Step | Hyp | Ref
| Expression |
1 | | ccatfval 13358 |
. . . 4
Word
Word ++ ..^ ..^
|
2 | 1 | eleq1d 2686 |
. . 3
Word
Word ++ Word
..^ ..^
Word |
3 | | wrdf 13310 |
. . . 4
..^ ..^ Word ..^ ..^ ..^ ..^ ..^
|
4 | | funmpt 5926 |
. . . . . . . . 9
..^ ..^ |
5 | | fzofi 12773 |
. . . . . . . . . . 11
..^ |
6 | | mptfi 8265 |
. . . . . . . . . . 11
..^ ..^ ..^
|
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . 10
..^ ..^ |
8 | | hashfun 13224 |
. . . . . . . . . 10
..^ ..^ ..^ ..^
..^ ..^ ..^ ..^
|
9 | 7, 8 | mp1i 13 |
. . . . . . . . 9
Word
Word
..^ ..^
..^ ..^ ..^ ..^
|
10 | 4, 9 | mpbii 223 |
. . . . . . . 8
Word
Word ..^ ..^ ..^ ..^
|
11 | | dmmptg 5632 |
. . . . . . . . . . 11
..^ ..^
..^ ..^
..^ |
12 | | fvex 6201 |
. . . . . . . . . . . . 13
|
13 | | fvex 6201 |
. . . . . . . . . . . . 13
|
14 | 12, 13 | ifex 4156 |
. . . . . . . . . . . 12
..^
|
15 | 14 | a1i 11 |
. . . . . . . . . . 11
..^ ..^ |
16 | 11, 15 | mprg 2926 |
. . . . . . . . . 10
..^ ..^ ..^ |
17 | 16 | fveq2i 6194 |
. . . . . . . . 9
..^ ..^
..^ |
18 | | lencl 13324 |
. . . . . . . . . . 11
Word
|
19 | | lencl 13324 |
. . . . . . . . . . 11
Word
|
20 | | nn0addcl 11328 |
. . . . . . . . . . 11
|
21 | 18, 19, 20 | syl2an 494 |
. . . . . . . . . 10
Word
Word |
22 | | hashfzo0 13217 |
. . . . . . . . . 10
..^ |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
Word
Word ..^ |
24 | 17, 23 | syl5eq 2668 |
. . . . . . . 8
Word
Word ..^ ..^ |
25 | 10, 24 | eqtrd 2656 |
. . . . . . 7
Word
Word ..^ ..^ |
26 | 25 | oveq2d 6666 |
. . . . . 6
Word
Word ..^ ..^ ..^
..^ |
27 | 26 | feq2d 6031 |
. . . . 5
Word
Word ..^ ..^
..^ ..^ ..^
..^ ..^
..^ |
28 | | eqid 2622 |
. . . . . . 7
..^ ..^ ..^ ..^
|
29 | 28 | fmpt 6381 |
. . . . . 6
..^ ..^ ..^ ..^
..^ |
30 | | simpl 473 |
. . . . . . . . 9
Word
Word
Word |
31 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . 19
|
33 | | addcom 10222 |
. . . . . . . . . . . . . . . . . . 19
|
34 | 31, 32, 33 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
|
35 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36 | ancomd 467 |
. . . . . . . . . . . . . . . . . . 19
|
38 | | nn0pzuz 11745 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
40 | 34, 39 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
41 | 18, 19, 40 | syl2an 494 |
. . . . . . . . . . . . . . . 16
Word
Word |
42 | | fzoss2 12496 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . 15
Word
Word ..^ ..^ |
44 | 43 | sselda 3603 |
. . . . . . . . . . . . . 14
Word Word
..^ ..^ |
45 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
47 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
49 | 45, 46, 48 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . 16
..^
..^ |
50 | 49 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
..^
..^ |
51 | 50 | rspcv 3305 |
. . . . . . . . . . . . . 14
..^ ..^ ..^
..^ |
52 | 44, 51 | syl 17 |
. . . . . . . . . . . . 13
Word Word
..^ ..^ ..^
..^ |
53 | | iftrue 4092 |
. . . . . . . . . . . . . . 15
..^
..^ |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . 14
Word Word
..^ ..^ |
55 | 54 | eleq1d 2686 |
. . . . . . . . . . . . 13
Word Word
..^ ..^
|
56 | 52, 55 | sylibd 229 |
. . . . . . . . . . . 12
Word Word
..^ ..^ ..^
|
57 | 56 | impancom 456 |
. . . . . . . . . . 11
Word Word ..^ ..^
..^ |
58 | 57 | imp 445 |
. . . . . . . . . 10
Word Word ..^ ..^
..^ |
59 | 58 | ralrimiva 2966 |
. . . . . . . . 9
Word Word ..^ ..^
..^ |
60 | | iswrdsymb 13322 |
. . . . . . . . 9
Word ..^ Word |
61 | 30, 59, 60 | syl2an2r 876 |
. . . . . . . 8
Word Word ..^ ..^
Word |
62 | | simpr 477 |
. . . . . . . . 9
Word
Word
Word |
63 | | simpr 477 |
. . . . . . . . . . . . . . . 16
Word Word
..^ ..^ |
64 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
Word |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word Word
..^ |
66 | | elincfzoext 12525 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
67 | 63, 65, 66 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Word Word
..^ ..^ |
68 | 18 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
Word
|
69 | 19 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
Word
|
70 | 68, 69, 33 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
Word
Word |
71 | 70 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
Word
Word ..^ ..^ |
72 | 71 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
Word
Word ..^
..^ |
73 | 72 | adantr 481 |
. . . . . . . . . . . . . . 15
Word Word
..^ ..^
..^ |
74 | 67, 73 | mpbird 247 |
. . . . . . . . . . . . . 14
Word Word
..^ ..^ |
75 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
76 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
77 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
79 | 75, 76, 78 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . 16
..^
..^ |
80 | 79 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
..^
..^ |
81 | 80 | rspcv 3305 |
. . . . . . . . . . . . . 14
..^ ..^ ..^
..^ |
82 | 74, 81 | syl 17 |
. . . . . . . . . . . . 13
Word Word
..^ ..^ ..^
..^ |
83 | 18 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . 21
Word
|
84 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word |
85 | 84 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Word Word
..^ |
86 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
87 | 86 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^
Word Word |
89 | 84 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
..^
Word Word |
90 | 88, 89 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . 20
..^
Word Word |
91 | 90 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
Word Word
..^ |
92 | | elfzole1 12478 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word Word
..^
|
94 | | addge02 10539 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 84, 87, 94 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
Word Word
..^ |
96 | 93, 95 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
Word Word
..^ |
97 | 85, 91, 96 | lensymd 10188 |
. . . . . . . . . . . . . . . . . 18
Word Word
..^
|
98 | 97 | intn3an3d 1444 |
. . . . . . . . . . . . . . . . 17
Word Word
..^
|
99 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . 17
..^
|
100 | 98, 99 | sylnibr 319 |
. . . . . . . . . . . . . . . 16
Word Word
..^ ..^ |
101 | 100 | iffalsed 4097 |
. . . . . . . . . . . . . . 15
Word Word
..^ ..^ |
102 | 101 | eleq1d 2686 |
. . . . . . . . . . . . . 14
Word Word
..^ ..^ |
103 | 86 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
..^
|
104 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Word
Word |
105 | | pncan 10287 |
. . . . . . . . . . . . . . . . . 18
|
106 | 103, 104,
105 | syl2anr 495 |
. . . . . . . . . . . . . . . . 17
Word Word
..^ |
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
Word Word
..^ |
108 | 107 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
Word Word
..^
|
109 | 108 | biimpd 219 |
. . . . . . . . . . . . . 14
Word Word
..^ |
110 | 102, 109 | sylbid 230 |
. . . . . . . . . . . . 13
Word Word
..^ ..^ |
111 | 82, 110 | syld 47 |
. . . . . . . . . . . 12
Word Word
..^ ..^ ..^
|
112 | 111 | impancom 456 |
. . . . . . . . . . 11
Word Word ..^ ..^
..^ |
113 | 112 | imp 445 |
. . . . . . . . . 10
Word Word ..^ ..^
..^ |
114 | 113 | ralrimiva 2966 |
. . . . . . . . 9
Word Word ..^ ..^
..^ |
115 | | iswrdsymb 13322 |
. . . . . . . . 9
Word ..^ Word |
116 | 62, 114, 115 | syl2an2r 876 |
. . . . . . . 8
Word Word ..^ ..^
Word |
117 | 61, 116 | jca 554 |
. . . . . . 7
Word Word ..^ ..^
Word Word |
118 | 117 | ex 450 |
. . . . . 6
Word
Word ..^ ..^
Word
Word |
119 | 29, 118 | syl5bir 233 |
. . . . 5
Word
Word ..^ ..^
..^ Word Word |
120 | 27, 119 | sylbid 230 |
. . . 4
Word
Word ..^ ..^
..^ ..^ ..^
Word Word |
121 | 3, 120 | syl5 34 |
. . 3
Word
Word ..^ ..^
Word Word Word |
122 | 2, 121 | sylbid 230 |
. 2
Word
Word ++ Word
Word
Word |
123 | | ccatcl 13359 |
. 2
Word
Word ++ Word |
124 | 122, 123 | impbid1 215 |
1
Word
Word ++ Word
Word Word |