Step | Hyp | Ref
| Expression |
1 | | lenco 13578 |
. . . . . . 7
Word
|
2 | 1 | 3adant2 1080 |
. . . . . 6
Word
Word |
3 | | lenco 13578 |
. . . . . . 7
Word
|
4 | 3 | 3adant1 1079 |
. . . . . 6
Word
Word |
5 | 2, 4 | oveq12d 6668 |
. . . . 5
Word
Word
|
6 | 5 | oveq2d 6666 |
. . . 4
Word
Word ..^
..^ |
7 | 6 | mpteq1d 4738 |
. . 3
Word
Word ..^ ..^
..^ ..^ |
8 | 2 | oveq2d 6666 |
. . . . . . . 8
Word
Word ..^ ..^ |
9 | 8 | adantr 481 |
. . . . . . 7
Word
Word ..^ ..^ ..^ |
10 | 9 | eleq2d 2687 |
. . . . . 6
Word
Word ..^ ..^
..^ |
11 | 10 | ifbid 4108 |
. . . . 5
Word
Word ..^ ..^
..^
|
12 | | wrdf 13310 |
. . . . . . . . . . 11
Word ..^ |
13 | 12 | 3ad2ant1 1082 |
. . . . . . . . . 10
Word
Word ..^ |
14 | 13 | adantr 481 |
. . . . . . . . 9
Word
Word ..^ ..^ |
15 | | ffn 6045 |
. . . . . . . . 9
..^ ..^ |
16 | 14, 15 | syl 17 |
. . . . . . . 8
Word
Word ..^
..^ |
17 | | fvco2 6273 |
. . . . . . . 8
..^ ..^ |
18 | 16, 17 | sylan 488 |
. . . . . . 7
Word Word ..^
..^ |
19 | | iftrue 4092 |
. . . . . . . 8
..^
..^ |
20 | 19 | adantl 482 |
. . . . . . 7
Word Word ..^
..^ ..^ |
21 | 18, 20 | eqtr4d 2659 |
. . . . . 6
Word Word ..^
..^ ..^ |
22 | | wrdf 13310 |
. . . . . . . . . . 11
Word ..^ |
23 | 22 | 3ad2ant2 1083 |
. . . . . . . . . 10
Word
Word ..^ |
24 | 23 | ad2antrr 762 |
. . . . . . . . 9
Word Word ..^
..^ ..^ |
25 | | ffn 6045 |
. . . . . . . . 9
..^ ..^ |
26 | 24, 25 | syl 17 |
. . . . . . . 8
Word Word ..^
..^
..^ |
27 | | lencl 13324 |
. . . . . . . . . . . . 13
Word |
28 | 27 | nn0zd 11480 |
. . . . . . . . . . . 12
Word |
29 | 28 | 3ad2ant1 1082 |
. . . . . . . . . . 11
Word
Word |
30 | | fzospliti 12500 |
. . . . . . . . . . . 12
..^ ..^ ..^ |
31 | 30 | ancoms 469 |
. . . . . . . . . . 11
..^
..^ ..^ |
32 | 29, 31 | sylan 488 |
. . . . . . . . . 10
Word
Word ..^ ..^ ..^ |
33 | 32 | orcanai 952 |
. . . . . . . . 9
Word Word ..^
..^
..^ |
34 | | lencl 13324 |
. . . . . . . . . . . 12
Word |
35 | 34 | nn0zd 11480 |
. . . . . . . . . . 11
Word |
36 | 35 | 3ad2ant2 1083 |
. . . . . . . . . 10
Word
Word |
37 | 36 | ad2antrr 762 |
. . . . . . . . 9
Word Word ..^
..^ |
38 | | fzosubel3 12528 |
. . . . . . . . 9
..^ ..^ |
39 | 33, 37, 38 | syl2anc 693 |
. . . . . . . 8
Word Word ..^
..^ ..^ |
40 | | fvco2 6273 |
. . . . . . . 8
..^ ..^
|
41 | 26, 39, 40 | syl2anc 693 |
. . . . . . 7
Word Word ..^
..^ |
42 | 2 | oveq2d 6666 |
. . . . . . . . 9
Word
Word |
43 | 42 | fveq2d 6195 |
. . . . . . . 8
Word
Word
|
44 | 43 | ad2antrr 762 |
. . . . . . 7
Word Word ..^
..^
|
45 | | iffalse 4095 |
. . . . . . . 8
..^
..^
|
46 | 45 | adantl 482 |
. . . . . . 7
Word Word ..^
..^ ..^
|
47 | 41, 44, 46 | 3eqtr4d 2666 |
. . . . . 6
Word Word ..^
..^ ..^ |
48 | 21, 47 | ifeqda 4121 |
. . . . 5
Word
Word ..^ ..^
..^ |
49 | 11, 48 | eqtrd 2656 |
. . . 4
Word
Word ..^ ..^
..^ |
50 | 49 | mpteq2dva 4744 |
. . 3
Word
Word ..^ ..^
..^ ..^ |
51 | 7, 50 | eqtr2d 2657 |
. 2
Word
Word ..^ ..^ ..^
..^ |
52 | 14 | ffvelrnda 6359 |
. . . 4
Word Word ..^
..^ |
53 | 24, 39 | ffvelrnd 6360 |
. . . 4
Word Word ..^
..^ |
54 | 52, 53 | ifclda 4120 |
. . 3
Word
Word ..^ ..^
|
55 | | ccatfval 13358 |
. . . 4
Word
Word ++ ..^ ..^
|
56 | 55 | 3adant3 1081 |
. . 3
Word
Word ++ ..^ ..^
|
57 | | simp3 1063 |
. . . 4
Word
Word |
58 | 57 | feqmptd 6249 |
. . 3
Word
Word
|
59 | | fveq2 6191 |
. . . 4
..^
..^
|
60 | | fvif 6204 |
. . . 4
..^ ..^ |
61 | 59, 60 | syl6eq 2672 |
. . 3
..^
..^ |
62 | 54, 56, 58, 61 | fmptco 6396 |
. 2
Word
Word ++ ..^ ..^ |
63 | | ffun 6048 |
. . . . 5
|
64 | 63 | 3ad2ant3 1084 |
. . . 4
Word
Word |
65 | | simp1 1061 |
. . . 4
Word
Word
Word |
66 | | cofunexg 7130 |
. . . 4
Word
|
67 | 64, 65, 66 | syl2anc 693 |
. . 3
Word
Word |
68 | | simp2 1062 |
. . . 4
Word
Word
Word |
69 | | cofunexg 7130 |
. . . 4
Word
|
70 | 64, 68, 69 | syl2anc 693 |
. . 3
Word
Word |
71 | | ccatfval 13358 |
. . 3
++
..^ ..^
|
72 | 67, 70, 71 | syl2anc 693 |
. 2
Word
Word ++
..^ ..^
|
73 | 51, 62, 72 | 3eqtr4d 2666 |
1
Word
Word ++ ++
|