Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . 4
Word |
2 | | efgval.r |
. . . 4
~FG |
3 | | efgval2.m |
. . . 4
|
4 | | efgval2.t |
. . . 4
splice |
5 | | efgred.d |
. . . 4
|
6 | | efgred.s |
. . . 4
Word ..^ |
7 | 1, 2, 3, 4, 5, 6 | efgsf 18142 |
. . 3
Word
..^ |
8 | 7 | fdmi 6052 |
. . . 4
Word
..^ |
9 | 8 | feq2i 6037 |
. . 3
Word
..^ |
10 | 7, 9 | mpbir 221 |
. 2
|
11 | | frn 6053 |
. . . 4
|
12 | 10, 11 | ax-mp 5 |
. . 3
|
13 | | fviss 6256 |
. . . . . . . . 9
Word Word |
14 | 1, 13 | eqsstri 3635 |
. . . . . . . 8
Word |
15 | 14 | sseli 3599 |
. . . . . . 7
Word |
16 | | lencl 13324 |
. . . . . . 7
Word
|
17 | 15, 16 | syl 17 |
. . . . . 6
|
18 | | peano2nn0 11333 |
. . . . . 6
|
19 | 14 | sseli 3599 |
. . . . . . . . . . . 12
Word |
20 | | lencl 13324 |
. . . . . . . . . . . 12
Word
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
|
22 | | nn0nlt0 11319 |
. . . . . . . . . . . 12
|
23 | | breq2 4657 |
. . . . . . . . . . . . 13
|
24 | 23 | notbid 308 |
. . . . . . . . . . . 12
|
25 | 22, 24 | syl5ibr 236 |
. . . . . . . . . . 11
|
26 | 21, 25 | syl5 34 |
. . . . . . . . . 10
|
27 | 26 | ralrimiv 2965 |
. . . . . . . . 9
|
28 | | rabeq0 3957 |
. . . . . . . . 9
|
29 | 27, 28 | sylibr 224 |
. . . . . . . 8
|
30 | 29 | sseq1d 3632 |
. . . . . . 7
|
31 | | breq2 4657 |
. . . . . . . . 9
|
32 | 31 | rabbidv 3189 |
. . . . . . . 8
|
33 | 32 | sseq1d 3632 |
. . . . . . 7
|
34 | | breq2 4657 |
. . . . . . . . 9
|
35 | 34 | rabbidv 3189 |
. . . . . . . 8
|
36 | 35 | sseq1d 3632 |
. . . . . . 7
|
37 | | breq2 4657 |
. . . . . . . . 9
|
38 | 37 | rabbidv 3189 |
. . . . . . . 8
|
39 | 38 | sseq1d 3632 |
. . . . . . 7
|
40 | | 0ss 3972 |
. . . . . . 7
|
41 | | simpr 477 |
. . . . . . . . . 10
|
42 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
43 | 42 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
44 | 43 | cbvrabv 3199 |
. . . . . . . . . . 11
|
45 | | eliun 4524 |
. . . . . . . . . . . . . . 15
|
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | rneqd 5353 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | cbvrexv 3172 |
. . . . . . . . . . . . . . 15
|
50 | 45, 49 | bitri 264 |
. . . . . . . . . . . . . 14
|
51 | | simpl1r 1113 |
. . . . . . . . . . . . . . . . . 18
|
52 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
|
53 | 14, 52 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word |
54 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | 55 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | | ltaddrp 11867 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | 56, 57, 58 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 1, 2, 3, 4 | efgtlen 18139 |
. . . . . . . . . . . . . . . . . . . . . 22
|
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . . 21
|
63 | 61, 62 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . 20
|
64 | 59, 63 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . 19
|
65 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
66 | 65 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | 66 | elrab 3363 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 52, 64, 67 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
|
69 | 51, 68 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
70 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 10, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
72 | | fvelrnb 6243 |
. . . . . . . . . . . . . . . . . 18
|
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
74 | 69, 73 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
75 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 1, 2, 3, 4, 5, 6 | efgsdm 18143 |
. . . . . . . . . . . . . . . . . . . . 21
Word
..^ |
77 | 76 | simp1bi 1076 |
. . . . . . . . . . . . . . . . . . . 20
Word |
78 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . 20
Word Word
|
79 | 75, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
Word |
80 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . 19
|
81 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 83 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | 81, 84 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 1, 2, 3, 4, 5, 6 | efgsp1 18150 |
. . . . . . . . . . . . . . . . . . . 20
++
|
87 | 75, 85, 86 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
++
|
88 | 1, 2, 3, 4, 5, 6 | efgsval2 18146 |
. . . . . . . . . . . . . . . . . . 19
Word
++
++ |
89 | 79, 80, 87, 88 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
++ |
90 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . 19
++
++ |
91 | 71, 87, 90 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
++ |
92 | 89, 91 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
|
93 | 92 | anassrs 680 |
. . . . . . . . . . . . . . . 16
|
94 | 74, 93 | rexlimddv 3035 |
. . . . . . . . . . . . . . 15
|
95 | 94 | rexlimdvaa 3032 |
. . . . . . . . . . . . . 14
|
96 | 50, 95 | syl5bi 232 |
. . . . . . . . . . . . 13
|
97 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 5 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . 20
|
99 | 1, 2, 3, 4, 5, 6 | efgs1 18148 |
. . . . . . . . . . . . . . . . . . . 20
|
100 | 98, 99 | sylbir 225 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 97, 100 | sylbir 225 |
. . . . . . . . . . . . . . . . . 18
|
102 | 1, 2, 3, 4, 5, 6 | efgsval 18144 |
. . . . . . . . . . . . . . . . . 18
|
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
104 | | s1len 13385 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 104 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | 105, 106 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . 19
|
108 | 107 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . 18
|
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
110 | | s1fv 13390 |
. . . . . . . . . . . . . . . . . 18
|
111 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
112 | 103, 109,
111 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
113 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . 17
|
114 | 71, 101, 113 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
115 | 112, 114 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
|
116 | 115 | ex 450 |
. . . . . . . . . . . . . 14
|
117 | 116 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
|
118 | 96, 117 | pm2.61d 170 |
. . . . . . . . . . . 12
|
119 | 118 | rabssdv 3682 |
. . . . . . . . . . 11
|
120 | 44, 119 | syl5eqss 3649 |
. . . . . . . . . 10
|
121 | 41, 120 | unssd 3789 |
. . . . . . . . 9
|
122 | 121 | ex 450 |
. . . . . . . 8
|
123 | | id 22 |
. . . . . . . . . . . . 13
|
124 | | nn0leltp1 11436 |
. . . . . . . . . . . . 13
|
125 | 21, 123, 124 | syl2anr 495 |
. . . . . . . . . . . 12
|
126 | 21 | nn0red 11352 |
. . . . . . . . . . . . 13
|
127 | | nn0re 11301 |
. . . . . . . . . . . . 13
|
128 | | leloe 10124 |
. . . . . . . . . . . . 13
|
129 | 126, 127,
128 | syl2anr 495 |
. . . . . . . . . . . 12
|
130 | 125, 129 | bitr3d 270 |
. . . . . . . . . . 11
|
131 | 130 | rabbidva 3188 |
. . . . . . . . . 10
|
132 | | unrab 3898 |
. . . . . . . . . 10
|
133 | 131, 132 | syl6eqr 2674 |
. . . . . . . . 9
|
134 | 133 | sseq1d 3632 |
. . . . . . . 8
|
135 | 122, 134 | sylibrd 249 |
. . . . . . 7
|
136 | 30, 33, 36, 39, 40, 135 | nn0ind 11472 |
. . . . . 6
|
137 | 17, 18, 136 | 3syl 18 |
. . . . 5
|
138 | | id 22 |
. . . . . 6
|
139 | 17 | nn0red 11352 |
. . . . . . 7
|
140 | 139 | ltp1d 10954 |
. . . . . 6
|
141 | 42 | breq1d 4663 |
. . . . . . 7
|
142 | 141 | elrab 3363 |
. . . . . 6
|
143 | 138, 140,
142 | sylanbrc 698 |
. . . . 5
|
144 | 137, 143 | sseldd 3604 |
. . . 4
|
145 | 144 | ssriv 3607 |
. . 3
|
146 | 12, 145 | eqssi 3619 |
. 2
|
147 | | dffo2 6119 |
. 2
|
148 | 10, 146, 147 | mpbir2an 955 |
1
|