Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . . . . 10
|
2 | | 2t0e0 11183 |
. . . . . . . . . 10
|
3 | 1, 2 | syl6eq 2672 |
. . . . . . . . 9
|
4 | 3 | oveq2d 6666 |
. . . . . . . 8
|
5 | 4 | fveq2d 6195 |
. . . . . . 7
|
6 | 5 | oveq2d 6666 |
. . . . . 6
|
7 | 6 | breq1d 4663 |
. . . . 5
|
8 | 7 | imbi2d 330 |
. . . 4
|
9 | | oveq2 6658 |
. . . . . . . . 9
|
10 | 9 | oveq2d 6666 |
. . . . . . . 8
|
11 | 10 | fveq2d 6195 |
. . . . . . 7
|
12 | 11 | oveq2d 6666 |
. . . . . 6
|
13 | 12 | breq1d 4663 |
. . . . 5
|
14 | 13 | imbi2d 330 |
. . . 4
|
15 | | oveq2 6658 |
. . . . . . . . 9
|
16 | 15 | oveq2d 6666 |
. . . . . . . 8
|
17 | 16 | fveq2d 6195 |
. . . . . . 7
|
18 | 17 | oveq2d 6666 |
. . . . . 6
|
19 | 18 | breq1d 4663 |
. . . . 5
|
20 | 19 | imbi2d 330 |
. . . 4
|
21 | | oveq2 6658 |
. . . . . . . . 9
|
22 | 21 | oveq2d 6666 |
. . . . . . . 8
|
23 | 22 | fveq2d 6195 |
. . . . . . 7
|
24 | 23 | oveq2d 6666 |
. . . . . 6
|
25 | 24 | breq1d 4663 |
. . . . 5
|
26 | 25 | imbi2d 330 |
. . . 4
|
27 | | iseralt.1 |
. . . . . . . . . . . 12
|
28 | | uzssz 11707 |
. . . . . . . . . . . 12
|
29 | 27, 28 | eqsstri 3635 |
. . . . . . . . . . 11
|
30 | 29 | a1i 11 |
. . . . . . . . . 10
|
31 | 30 | sselda 3603 |
. . . . . . . . 9
|
32 | 31 | zcnd 11483 |
. . . . . . . 8
|
33 | 32 | addid1d 10236 |
. . . . . . 7
|
34 | 33 | fveq2d 6195 |
. . . . . 6
|
35 | 34 | oveq2d 6666 |
. . . . 5
|
36 | | neg1rr 11125 |
. . . . . . . . 9
|
37 | | neg1ne0 11126 |
. . . . . . . . 9
|
38 | | reexpclz 12880 |
. . . . . . . . 9
|
39 | 36, 37, 38 | mp3an12 1414 |
. . . . . . . 8
|
40 | 31, 39 | syl 17 |
. . . . . . 7
|
41 | | iseralt.2 |
. . . . . . . . 9
|
42 | | iseralt.6 |
. . . . . . . . . 10
|
43 | 30 | sselda 3603 |
. . . . . . . . . . . 12
|
44 | | reexpclz 12880 |
. . . . . . . . . . . . 13
|
45 | 36, 37, 44 | mp3an12 1414 |
. . . . . . . . . . . 12
|
46 | 43, 45 | syl 17 |
. . . . . . . . . . 11
|
47 | | iseralt.3 |
. . . . . . . . . . . 12
|
48 | 47 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
49 | 46, 48 | remulcld 10070 |
. . . . . . . . . 10
|
50 | 42, 49 | eqeltrd 2701 |
. . . . . . . . 9
|
51 | 27, 41, 50 | serfre 12830 |
. . . . . . . 8
|
52 | 51 | ffvelrnda 6359 |
. . . . . . 7
|
53 | 40, 52 | remulcld 10070 |
. . . . . 6
|
54 | 53 | leidd 10594 |
. . . . 5
|
55 | 35, 54 | eqbrtrd 4675 |
. . . 4
|
56 | 47 | ad2antrr 762 |
. . . . . . . . . . 11
|
57 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | 2timesi 11147 |
. . . . . . . . . . . . . . 15
|
59 | 58 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
60 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 60, 27 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
|
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
63 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . 17
|
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
66 | | 2cn 11091 |
. . . . . . . . . . . . . . . 16
|
67 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . 17
|
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
69 | | mulcl 10020 |
. . . . . . . . . . . . . . . 16
|
70 | 66, 68, 69 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
71 | 66, 57 | mulcli 10045 |
. . . . . . . . . . . . . . . 16
|
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . 15
|
73 | 65, 70, 72 | addassd 10062 |
. . . . . . . . . . . . . 14
|
74 | 59, 73 | syl5eqr 2670 |
. . . . . . . . . . . . 13
|
75 | | 2nn0 11309 |
. . . . . . . . . . . . . . . . . 18
|
76 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
77 | | nn0mulcl 11329 |
. . . . . . . . . . . . . . . . . 18
|
78 | 75, 76, 77 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
79 | | uzaddcl 11744 |
. . . . . . . . . . . . . . . . 17
|
80 | 62, 78, 79 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
81 | 28, 80 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
82 | 81 | zcnd 11483 |
. . . . . . . . . . . . . 14
|
83 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
84 | 82, 83, 83 | addassd 10062 |
. . . . . . . . . . . . 13
|
85 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
86 | 85, 68, 83 | adddid 10064 |
. . . . . . . . . . . . . 14
|
87 | 86 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
88 | 74, 84, 87 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
|
89 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . 16
|
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . 15
|
91 | | nn0mulcl 11329 |
. . . . . . . . . . . . . . 15
|
92 | 75, 90, 91 | sylancr 695 |
. . . . . . . . . . . . . 14
|
93 | | uzaddcl 11744 |
. . . . . . . . . . . . . 14
|
94 | 62, 92, 93 | syl2anc 693 |
. . . . . . . . . . . . 13
|
95 | 94, 27 | syl6eleqr 2712 |
. . . . . . . . . . . 12
|
96 | 88, 95 | eqeltrd 2701 |
. . . . . . . . . . 11
|
97 | 56, 96 | ffvelrnd 6360 |
. . . . . . . . . 10
|
98 | | peano2uz 11741 |
. . . . . . . . . . . . 13
|
99 | 80, 98 | syl 17 |
. . . . . . . . . . . 12
|
100 | 99, 27 | syl6eleqr 2712 |
. . . . . . . . . . 11
|
101 | 56, 100 | ffvelrnd 6360 |
. . . . . . . . . 10
|
102 | 97, 101 | resubcld 10458 |
. . . . . . . . 9
|
103 | | 0red 10041 |
. . . . . . . . 9
|
104 | 40 | adantr 481 |
. . . . . . . . . 10
|
105 | 51 | ad2antrr 762 |
. . . . . . . . . . 11
|
106 | 80, 27 | syl6eleqr 2712 |
. . . . . . . . . . 11
|
107 | 105, 106 | ffvelrnd 6360 |
. . . . . . . . . 10
|
108 | 104, 107 | remulcld 10070 |
. . . . . . . . 9
|
109 | | iseralt.4 |
. . . . . . . . . . . . 13
|
110 | 109 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
111 | 110 | ad2antrr 762 |
. . . . . . . . . . 11
|
112 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
113 | 112 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
114 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
115 | 113, 114 | breq12d 4666 |
. . . . . . . . . . . 12
|
116 | 115 | rspcv 3305 |
. . . . . . . . . . 11
|
117 | 100, 111,
116 | sylc 65 |
. . . . . . . . . 10
|
118 | 97, 101 | suble0d 10618 |
. . . . . . . . . 10
|
119 | 117, 118 | mpbird 247 |
. . . . . . . . 9
|
120 | 102, 103,
108, 119 | leadd2dd 10642 |
. . . . . . . 8
|
121 | | seqp1 12816 |
. . . . . . . . . . . . 13
|
122 | 99, 121 | syl 17 |
. . . . . . . . . . . 12
|
123 | | seqp1 12816 |
. . . . . . . . . . . . . 14
|
124 | 80, 123 | syl 17 |
. . . . . . . . . . . . 13
|
125 | 124 | oveq1d 6665 |
. . . . . . . . . . . 12
|
126 | 122, 125 | eqtrd 2656 |
. . . . . . . . . . 11
|
127 | 88 | fveq2d 6195 |
. . . . . . . . . . 11
|
128 | 107 | recnd 10068 |
. . . . . . . . . . . 12
|
129 | 42 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
|
130 | 129 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
131 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
132 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
133 | 132, 114 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
134 | 131, 133 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
|
135 | 134 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
|
136 | 100, 130,
135 | sylc 65 |
. . . . . . . . . . . . . . 15
|
137 | | neg1cn 11124 |
. . . . . . . . . . . . . . . . . . 19
|
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
139 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
140 | 138, 139,
81 | expp1zd 13017 |
. . . . . . . . . . . . . . . . 17
|
141 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
142 | 141, 139,
81 | reexpclzd 13034 |
. . . . . . . . . . . . . . . . . . 19
|
143 | 142 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
144 | | mulcom 10022 |
. . . . . . . . . . . . . . . . . 18
|
145 | 143, 137,
144 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
146 | 143 | mulm1d 10482 |
. . . . . . . . . . . . . . . . 17
|
147 | 140, 145,
146 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
148 | 147 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
149 | 101 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
150 | | mulneg12 10468 |
. . . . . . . . . . . . . . . 16
|
151 | 143, 149,
150 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
152 | 136, 148,
151 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
153 | 101 | renegcld 10457 |
. . . . . . . . . . . . . . 15
|
154 | 142, 153 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
155 | 152, 154 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
156 | 155 | recnd 10068 |
. . . . . . . . . . . 12
|
157 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
158 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
159 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
160 | 158, 159 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
161 | 157, 160 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
|
162 | 161 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
|
163 | 96, 130, 162 | sylc 65 |
. . . . . . . . . . . . . . 15
|
164 | 81 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . 18
|
165 | 138, 139,
164 | expp1zd 13017 |
. . . . . . . . . . . . . . . . 17
|
166 | 147 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
167 | | mul2neg 10469 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 143, 57, 167 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
169 | 143 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . 18
|
170 | 168, 169 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
171 | 165, 166,
170 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
172 | 171 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
173 | 163, 172 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
174 | 142, 97 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
175 | 173, 174 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
176 | 175 | recnd 10068 |
. . . . . . . . . . . 12
|
177 | 128, 156,
176 | addassd 10062 |
. . . . . . . . . . 11
|
178 | 126, 127,
177 | 3eqtr3d 2664 |
. . . . . . . . . 10
|
179 | 178 | oveq2d 6666 |
. . . . . . . . 9
|
180 | 104 | recnd 10068 |
. . . . . . . . . 10
|
181 | 155, 175 | readdcld 10069 |
. . . . . . . . . . 11
|
182 | 181 | recnd 10068 |
. . . . . . . . . 10
|
183 | 180, 128,
182 | adddid 10064 |
. . . . . . . . 9
|
184 | 180, 156,
176 | adddid 10064 |
. . . . . . . . . . 11
|
185 | 152 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
186 | 153 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
187 | 180, 143,
186 | mulassd 10063 |
. . . . . . . . . . . . . 14
|
188 | 185, 187 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
189 | 85, 65, 68 | adddid 10064 |
. . . . . . . . . . . . . . . . 17
|
190 | 65 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . 18
|
191 | 190 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
192 | 65, 65, 70 | addassd 10062 |
. . . . . . . . . . . . . . . . 17
|
193 | 189, 191,
192 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . 16
|
194 | 193 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
195 | | expaddz 12904 |
. . . . . . . . . . . . . . . 16
|
196 | 138, 139,
64, 81, 195 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
|
197 | | 2z 11409 |
. . . . . . . . . . . . . . . . . 18
|
198 | 197 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
199 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . 18
|
200 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . 18
|
201 | 31, 199, 200 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
202 | | expmulz 12906 |
. . . . . . . . . . . . . . . . 17
|
203 | 138, 139,
198, 201, 202 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
|
204 | | neg1sqe1 12959 |
. . . . . . . . . . . . . . . . . 18
|
205 | 204 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
|
206 | | 1exp 12889 |
. . . . . . . . . . . . . . . . . 18
|
207 | 201, 206 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
208 | 205, 207 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
|
209 | 203, 208 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
210 | 194, 196,
209 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
|
211 | 210 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
212 | 186 | mulid2d 10058 |
. . . . . . . . . . . . 13
|
213 | 188, 211,
212 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
214 | 173 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
215 | 97 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
216 | 180, 143,
215 | mulassd 10063 |
. . . . . . . . . . . . . 14
|
217 | 214, 216 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
218 | 210 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
219 | 215 | mulid2d 10058 |
. . . . . . . . . . . . 13
|
220 | 217, 218,
219 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
221 | 213, 220 | oveq12d 6668 |
. . . . . . . . . . 11
|
222 | 149 | negcld 10379 |
. . . . . . . . . . . . 13
|
223 | 222, 215 | addcomd 10238 |
. . . . . . . . . . . 12
|
224 | 215, 149 | negsubd 10398 |
. . . . . . . . . . . 12
|
225 | 223, 224 | eqtrd 2656 |
. . . . . . . . . . 11
|
226 | 184, 221,
225 | 3eqtrd 2660 |
. . . . . . . . . 10
|
227 | 226 | oveq2d 6666 |
. . . . . . . . 9
|
228 | 179, 183,
227 | 3eqtrrd 2661 |
. . . . . . . 8
|
229 | 108 | recnd 10068 |
. . . . . . . . 9
|
230 | 229 | addid1d 10236 |
. . . . . . . 8
|
231 | 120, 228,
230 | 3brtr3d 4684 |
. . . . . . 7
|
232 | 105, 95 | ffvelrnd 6360 |
. . . . . . . . 9
|
233 | 104, 232 | remulcld 10070 |
. . . . . . . 8
|
234 | 53 | adantr 481 |
. . . . . . . 8
|
235 | | letr 10131 |
. . . . . . . 8
|
236 | 233, 108,
234, 235 | syl3anc 1326 |
. . . . . . 7
|
237 | 231, 236 | mpand 711 |
. . . . . 6
|
238 | 237 | expcom 451 |
. . . . 5
|
239 | 238 | a2d 29 |
. . . 4
|
240 | 8, 14, 20, 26, 55, 239 | nn0ind 11472 |
. . 3
|
241 | 240 | com12 32 |
. 2
|
242 | 241 | 3impia 1261 |
1
|