Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . . . 10
Word |
2 | | fviss 6256 |
. . . . . . . . . 10
Word Word |
3 | 1, 2 | eqsstri 3635 |
. . . . . . . . 9
Word |
4 | | efgredlem.2 |
. . . . . . . . . . . . 13
|
5 | | efgval.r |
. . . . . . . . . . . . . . 15
~FG |
6 | | efgval2.m |
. . . . . . . . . . . . . . 15
|
7 | | efgval2.t |
. . . . . . . . . . . . . . 15
splice |
8 | | efgred.d |
. . . . . . . . . . . . . . 15
|
9 | | efgred.s |
. . . . . . . . . . . . . . 15
Word ..^ |
10 | 1, 5, 6, 7, 8, 9 | efgsdm 18143 |
. . . . . . . . . . . . . 14
Word
..^ |
11 | 10 | simp1bi 1076 |
. . . . . . . . . . . . 13
Word |
12 | 4, 11 | syl 17 |
. . . . . . . . . . . 12
Word |
13 | 12 | eldifad 3586 |
. . . . . . . . . . 11
Word |
14 | | wrdf 13310 |
. . . . . . . . . . 11
Word ..^ |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
..^ |
16 | | efgredlem.1 |
. . . . . . . . . . . . . . 15
|
17 | | efgredlem.3 |
. . . . . . . . . . . . . . 15
|
18 | | efgredlem.4 |
. . . . . . . . . . . . . . 15
|
19 | | efgredlem.5 |
. . . . . . . . . . . . . . 15
|
20 | 1, 5, 6, 7, 8, 9, 16, 4, 17, 18, 19 | efgredlema 18153 |
. . . . . . . . . . . . . 14
|
21 | 20 | simpld 475 |
. . . . . . . . . . . . 13
|
22 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
|
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
|
24 | 21 | nnred 11035 |
. . . . . . . . . . . . 13
|
25 | 24 | lem1d 10957 |
. . . . . . . . . . . 12
|
26 | | eldifsni 4320 |
. . . . . . . . . . . . . . 15
Word |
27 | 4, 11, 26 | 3syl 18 |
. . . . . . . . . . . . . 14
|
28 | | wrdfin 13323 |
. . . . . . . . . . . . . . 15
Word |
29 | | hashnncl 13157 |
. . . . . . . . . . . . . . 15
|
30 | 13, 28, 29 | 3syl 18 |
. . . . . . . . . . . . . 14
|
31 | 27, 30 | mpbird 247 |
. . . . . . . . . . . . 13
|
32 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
|
33 | | fznn0 12432 |
. . . . . . . . . . . . 13
|
34 | 31, 32, 33 | 3syl 18 |
. . . . . . . . . . . 12
|
35 | 23, 25, 34 | mpbir2and 957 |
. . . . . . . . . . 11
|
36 | | lencl 13324 |
. . . . . . . . . . . . . 14
Word |
37 | 13, 36 | syl 17 |
. . . . . . . . . . . . 13
|
38 | 37 | nn0zd 11480 |
. . . . . . . . . . . 12
|
39 | | fzoval 12471 |
. . . . . . . . . . . 12
..^ |
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
..^ |
41 | 35, 40 | eleqtrrd 2704 |
. . . . . . . . . 10
..^ |
42 | 15, 41 | ffvelrnd 6360 |
. . . . . . . . 9
|
43 | 3, 42 | sseldi 3601 |
. . . . . . . 8
Word |
44 | | lencl 13324 |
. . . . . . . 8
Word
|
45 | 43, 44 | syl 17 |
. . . . . . 7
|
46 | 45 | nn0red 11352 |
. . . . . 6
|
47 | | 2rp 11837 |
. . . . . 6
|
48 | | ltaddrp 11867 |
. . . . . 6
|
49 | 46, 47, 48 | sylancl 694 |
. . . . 5
|
50 | 37 | nn0red 11352 |
. . . . . . . . . . 11
|
51 | 50 | lem1d 10957 |
. . . . . . . . . 10
|
52 | | fznn 12408 |
. . . . . . . . . . 11
|
53 | 38, 52 | syl 17 |
. . . . . . . . . 10
|
54 | 21, 51, 53 | mpbir2and 957 |
. . . . . . . . 9
|
55 | 1, 5, 6, 7, 8, 9 | efgsres 18151 |
. . . . . . . . 9
..^ |
56 | 4, 54, 55 | syl2anc 693 |
. . . . . . . 8
..^ |
57 | 1, 5, 6, 7, 8, 9 | efgsval 18144 |
. . . . . . . 8
..^
..^ ..^ ..^ |
58 | 56, 57 | syl 17 |
. . . . . . 7
..^ ..^ ..^ |
59 | | 1eluzge0 11732 |
. . . . . . . . . . . . . 14
|
60 | | fzss1 12380 |
. . . . . . . . . . . . . 14
|
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . 13
|
62 | 61, 54 | sseldi 3601 |
. . . . . . . . . . . 12
|
63 | | swrd0val 13421 |
. . . . . . . . . . . 12
Word substr
..^ |
64 | 13, 62, 63 | syl2anc 693 |
. . . . . . . . . . 11
substr
..^ |
65 | 64 | fveq2d 6195 |
. . . . . . . . . 10
substr ..^ |
66 | | swrd0len 13422 |
. . . . . . . . . . 11
Word substr |
67 | 13, 62, 66 | syl2anc 693 |
. . . . . . . . . 10
substr |
68 | 65, 67 | eqtr3d 2658 |
. . . . . . . . 9
..^ |
69 | 68 | oveq1d 6665 |
. . . . . . . 8
..^ |
70 | 69 | fveq2d 6195 |
. . . . . . 7
..^ ..^ ..^ |
71 | | fzo0end 12560 |
. . . . . . . 8
..^ |
72 | | fvres 6207 |
. . . . . . . 8
..^ ..^ |
73 | 21, 71, 72 | 3syl 18 |
. . . . . . 7
..^ |
74 | 58, 70, 73 | 3eqtrd 2660 |
. . . . . 6
..^ |
75 | 74 | fveq2d 6195 |
. . . . 5
..^ |
76 | 1, 5, 6, 7, 8, 9 | efgsdmi 18145 |
. . . . . . 7
|
77 | 4, 21, 76 | syl2anc 693 |
. . . . . 6
|
78 | 1, 5, 6, 7 | efgtlen 18139 |
. . . . . 6
|
79 | 42, 77, 78 | syl2anc 693 |
. . . . 5
|
80 | 49, 75, 79 | 3brtr4d 4685 |
. . . 4
..^ |
81 | 1, 5, 6, 7 | efgtf 18135 |
. . . . . . . . . . . 12
splice |
82 | 42, 81 | syl 17 |
. . . . . . . . . . 11
splice |
83 | 82 | simprd 479 |
. . . . . . . . . 10
|
84 | | ffn 6045 |
. . . . . . . . . 10
|
85 | | ovelrn 6810 |
. . . . . . . . . 10
|
86 | 83, 84, 85 | 3syl 18 |
. . . . . . . . 9
|
87 | 77, 86 | mpbid 222 |
. . . . . . . 8
|
88 | 20 | simprd 479 |
. . . . . . . . . 10
|
89 | 1, 5, 6, 7, 8, 9 | efgsdmi 18145 |
. . . . . . . . . 10
|
90 | 17, 88, 89 | syl2anc 693 |
. . . . . . . . 9
|
91 | 1, 5, 6, 7, 8, 9 | efgsdm 18143 |
. . . . . . . . . . . . . . . . 17
Word
..^ |
92 | 91 | simp1bi 1076 |
. . . . . . . . . . . . . . . 16
Word |
93 | 17, 92 | syl 17 |
. . . . . . . . . . . . . . 15
Word |
94 | 93 | eldifad 3586 |
. . . . . . . . . . . . . 14
Word |
95 | | wrdf 13310 |
. . . . . . . . . . . . . 14
Word ..^ |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . 13
..^ |
97 | | fzo0end 12560 |
. . . . . . . . . . . . . . 15
..^ |
98 | | elfzofz 12485 |
. . . . . . . . . . . . . . 15
..^ |
99 | 88, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . 14
|
100 | | lencl 13324 |
. . . . . . . . . . . . . . . . 17
Word |
101 | 94, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
|
102 | 101 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
|
103 | | fzoval 12471 |
. . . . . . . . . . . . . . 15
..^ |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . 14
..^ |
105 | 99, 104 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
..^ |
106 | 96, 105 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
107 | 1, 5, 6, 7 | efgtf 18135 |
. . . . . . . . . . . 12
splice |
108 | 106, 107 | syl 17 |
. . . . . . . . . . 11
splice |
109 | 108 | simprd 479 |
. . . . . . . . . 10
|
110 | | ffn 6045 |
. . . . . . . . . 10
|
111 | | ovelrn 6810 |
. . . . . . . . . 10
|
112 | 109, 110,
111 | 3syl 18 |
. . . . . . . . 9
|
113 | 90, 112 | mpbid 222 |
. . . . . . . 8
|
114 | | reeanv 3107 |
. . . . . . . . 9
|
115 | | reeanv 3107 |
. . . . . . . . . . 11
|
116 | 16 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
117 | 4 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
118 | 17 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
119 | 18 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
120 | 19 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
121 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
122 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
123 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
|
124 | 123 | simpld 475 |
. . . . . . . . . . . . . . 15
|
125 | 123 | simprd 479 |
. . . . . . . . . . . . . . 15
|
126 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
|
127 | 126 | simpld 475 |
. . . . . . . . . . . . . . 15
|
128 | 126 | simprd 479 |
. . . . . . . . . . . . . . 15
|
129 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
|
130 | 129 | simpld 475 |
. . . . . . . . . . . . . . 15
|
131 | 129 | simprd 479 |
. . . . . . . . . . . . . . 15
|
132 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
133 | 1, 5, 6, 7, 8, 9, 116, 117, 118, 119, 120, 121, 122, 124, 125, 127, 128, 130, 131, 132 | efgredlemb 18159 |
. . . . . . . . . . . . . 14
|
134 | | iman 440 |
. . . . . . . . . . . . . 14
|
135 | 133, 134 | mpbir 221 |
. . . . . . . . . . . . 13
|
136 | 135 | expr 643 |
. . . . . . . . . . . 12
|
137 | 136 | rexlimdvva 3038 |
. . . . . . . . . . 11
|
138 | 115, 137 | syl5bir 233 |
. . . . . . . . . 10
|
139 | 138 | rexlimdvva 3038 |
. . . . . . . . 9
|
140 | 114, 139 | syl5bir 233 |
. . . . . . . 8
|
141 | 87, 113, 140 | mp2and 715 |
. . . . . . 7
|
142 | | fvres 6207 |
. . . . . . . 8
..^ ..^ |
143 | 88, 97, 142 | 3syl 18 |
. . . . . . 7
..^ |
144 | 141, 73, 143 | 3eqtr4d 2666 |
. . . . . 6
..^
..^ |
145 | | fzss1 12380 |
. . . . . . . . . . . . 13
|
146 | 59, 145 | ax-mp 5 |
. . . . . . . . . . . 12
|
147 | 101 | nn0red 11352 |
. . . . . . . . . . . . . 14
|
148 | 147 | lem1d 10957 |
. . . . . . . . . . . . 13
|
149 | | fznn 12408 |
. . . . . . . . . . . . . 14
|
150 | 102, 149 | syl 17 |
. . . . . . . . . . . . 13
|
151 | 88, 148, 150 | mpbir2and 957 |
. . . . . . . . . . . 12
|
152 | 146, 151 | sseldi 3601 |
. . . . . . . . . . 11
|
153 | | swrd0val 13421 |
. . . . . . . . . . 11
Word substr
..^ |
154 | 94, 152, 153 | syl2anc 693 |
. . . . . . . . . 10
substr
..^ |
155 | 154 | fveq2d 6195 |
. . . . . . . . 9
substr ..^ |
156 | | swrd0len 13422 |
. . . . . . . . . 10
Word substr |
157 | 94, 152, 156 | syl2anc 693 |
. . . . . . . . 9
substr |
158 | 155, 157 | eqtr3d 2658 |
. . . . . . . 8
..^ |
159 | 158 | oveq1d 6665 |
. . . . . . 7
..^ |
160 | 159 | fveq2d 6195 |
. . . . . 6
..^ ..^ ..^ |
161 | 144, 70, 160 | 3eqtr4d 2666 |
. . . . 5
..^ ..^ ..^ ..^ |
162 | 1, 5, 6, 7, 8, 9 | efgsres 18151 |
. . . . . . 7
..^ |
163 | 17, 151, 162 | syl2anc 693 |
. . . . . 6
..^ |
164 | 1, 5, 6, 7, 8, 9 | efgsval 18144 |
. . . . . 6
..^
..^ ..^ ..^ |
165 | 163, 164 | syl 17 |
. . . . 5
..^ ..^ ..^ |
166 | 161, 58, 165 | 3eqtr4d 2666 |
. . . 4
..^ ..^ |
167 | | fveq2 6191 |
. . . . . . . . 9
..^ ..^ |
168 | 167 | fveq2d 6195 |
. . . . . . . 8
..^ ..^ |
169 | 168 | breq1d 4663 |
. . . . . . 7
..^
..^ |
170 | 167 | eqeq1d 2624 |
. . . . . . . 8
..^ ..^ |
171 | | fveq1 6190 |
. . . . . . . . 9
..^
..^ |
172 | 171 | eqeq1d 2624 |
. . . . . . . 8
..^ ..^ |
173 | 170, 172 | imbi12d 334 |
. . . . . . 7
..^
..^ ..^ |
174 | 169, 173 | imbi12d 334 |
. . . . . 6
..^
..^
..^ ..^ |
175 | | fveq2 6191 |
. . . . . . . . 9
..^ ..^ |
176 | 175 | eqeq2d 2632 |
. . . . . . . 8
..^
..^
..^ ..^ |
177 | | fveq1 6190 |
. . . . . . . . 9
..^
..^ |
178 | 177 | eqeq2d 2632 |
. . . . . . . 8
..^ ..^
..^
..^ |
179 | 176, 178 | imbi12d 334 |
. . . . . . 7
..^ ..^ ..^ ..^
..^ ..^ ..^ |
180 | 179 | imbi2d 330 |
. . . . . 6
..^ ..^
..^ ..^ ..^ ..^
..^ ..^ ..^ |
181 | 174, 180 | rspc2va 3323 |
. . . . 5
..^
..^
..^
..^ ..^ ..^ ..^ |
182 | 56, 163, 16, 181 | syl21anc 1325 |
. . . 4
..^ ..^
..^ ..^ ..^ |
183 | 80, 166, 182 | mp2d 49 |
. . 3
..^ ..^ |
184 | | lbfzo0 12507 |
. . . . 5
..^ |
185 | 21, 184 | sylibr 224 |
. . . 4
..^ |
186 | | fvres 6207 |
. . . 4
..^
..^ |
187 | 185, 186 | syl 17 |
. . 3
..^ |
188 | | lbfzo0 12507 |
. . . . 5
..^ |
189 | 88, 188 | sylibr 224 |
. . . 4
..^ |
190 | | fvres 6207 |
. . . 4
..^
..^ |
191 | 189, 190 | syl 17 |
. . 3
..^ |
192 | 183, 187,
191 | 3eqtr3d 2664 |
. 2
|
193 | 192, 19 | pm2.65i 185 |
1
|