Step | Hyp | Ref
| Expression |
1 | | 4z 11411 |
. 2
|
2 | | oveq2 6658 |
. . . 4
|
3 | | id 22 |
. . . 4
|
4 | 2, 3 | oveq12d 6668 |
. . 3
|
5 | | oveq2 6658 |
. . . 4
|
6 | 5, 3 | oveq12d 6668 |
. . 3
|
7 | 4, 6 | breq12d 4666 |
. 2
|
8 | | oveq2 6658 |
. . . 4
|
9 | | id 22 |
. . . 4
|
10 | 8, 9 | oveq12d 6668 |
. . 3
|
11 | | oveq2 6658 |
. . . 4
|
12 | 11, 9 | oveq12d 6668 |
. . 3
|
13 | 10, 12 | breq12d 4666 |
. 2
|
14 | | oveq2 6658 |
. . . 4
|
15 | | id 22 |
. . . 4
|
16 | 14, 15 | oveq12d 6668 |
. . 3
|
17 | | oveq2 6658 |
. . . 4
|
18 | 17, 15 | oveq12d 6668 |
. . 3
|
19 | 16, 18 | breq12d 4666 |
. 2
|
20 | | oveq2 6658 |
. . . 4
|
21 | | id 22 |
. . . 4
|
22 | 20, 21 | oveq12d 6668 |
. . 3
|
23 | | oveq2 6658 |
. . . 4
|
24 | 23, 21 | oveq12d 6668 |
. . 3
|
25 | 22, 24 | breq12d 4666 |
. 2
|
26 | | 6nn0 11313 |
. . . 4
|
27 | | 7nn0 11314 |
. . . 4
|
28 | | 4nn0 11311 |
. . . 4
|
29 | | 0nn0 11307 |
. . . 4
|
30 | | 4lt10 11678 |
. . . 4
; |
31 | | 6lt7 11209 |
. . . 4
|
32 | 26, 27, 28, 29, 30, 31 | decltc 11532 |
. . 3
; ; |
33 | | 2cn 11091 |
. . . . . 6
|
34 | | 2nn0 11309 |
. . . . . 6
|
35 | | 3nn0 11310 |
. . . . . 6
|
36 | | expmul 12905 |
. . . . . 6
|
37 | 33, 34, 35, 36 | mp3an 1424 |
. . . . 5
|
38 | | sq2 12960 |
. . . . . . 7
|
39 | 38 | eqcomi 2631 |
. . . . . 6
|
40 | | 4m1e3 11138 |
. . . . . 6
|
41 | 39, 40 | oveq12i 6662 |
. . . . 5
|
42 | 37, 41 | eqtr4i 2647 |
. . . 4
|
43 | | 3cn 11095 |
. . . . . . 7
|
44 | | 3t2e6 11179 |
. . . . . . 7
|
45 | 43, 33, 44 | mulcomli 10047 |
. . . . . 6
|
46 | 45 | oveq2i 6661 |
. . . . 5
|
47 | | 2exp6 15795 |
. . . . 5
; |
48 | 46, 47 | eqtri 2644 |
. . . 4
; |
49 | | 4cn 11098 |
. . . . 5
|
50 | | 4ne0 11117 |
. . . . 5
|
51 | | expm1 12910 |
. . . . 5
|
52 | 49, 50, 1, 51 | mp3an 1424 |
. . . 4
|
53 | 42, 48, 52 | 3eqtr3ri 2653 |
. . 3
; |
54 | | df-4 11081 |
. . . . . . 7
|
55 | 54 | oveq2i 6661 |
. . . . . 6
|
56 | 55, 54 | oveq12i 6662 |
. . . . 5
|
57 | | bcp1ctr 25004 |
. . . . . 6
|
58 | 35, 57 | ax-mp 5 |
. . . . 5
|
59 | | df-3 11080 |
. . . . . . . . 9
|
60 | 59 | oveq2i 6661 |
. . . . . . . 8
|
61 | 60, 59 | oveq12i 6662 |
. . . . . . 7
|
62 | | bcp1ctr 25004 |
. . . . . . . . 9
|
63 | 34, 62 | ax-mp 5 |
. . . . . . . 8
|
64 | | df-2 11079 |
. . . . . . . . . . . 12
|
65 | 64 | oveq2i 6661 |
. . . . . . . . . . 11
|
66 | 65, 64 | oveq12i 6662 |
. . . . . . . . . 10
|
67 | | 1nn0 11308 |
. . . . . . . . . . 11
|
68 | | bcp1ctr 25004 |
. . . . . . . . . . 11
|
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . 10
|
70 | | 1e0p1 11552 |
. . . . . . . . . . . . . . 15
|
71 | 70 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
72 | 71, 70 | oveq12i 6662 |
. . . . . . . . . . . . 13
|
73 | | bcp1ctr 25004 |
. . . . . . . . . . . . . 14
|
74 | 29, 73 | ax-mp 5 |
. . . . . . . . . . . . 13
|
75 | 34, 29 | nn0mulcli 11331 |
. . . . . . . . . . . . . . . 16
|
76 | | bcn0 13097 |
. . . . . . . . . . . . . . . 16
|
77 | 75, 76 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
78 | | 2t0e0 11183 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | 78 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . 20
|
80 | 79, 70 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 70 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . 19
|
82 | 80, 81 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . 18
|
83 | | 1div1e1 10717 |
. . . . . . . . . . . . . . . . . 18
|
84 | 82, 83 | eqtri 2644 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
|
86 | | 2t1e2 11176 |
. . . . . . . . . . . . . . . 16
|
87 | 85, 86 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
88 | 77, 87 | oveq12i 6662 |
. . . . . . . . . . . . . 14
|
89 | 33 | mulid2i 10043 |
. . . . . . . . . . . . . 14
|
90 | 88, 89 | eqtri 2644 |
. . . . . . . . . . . . 13
|
91 | 72, 74, 90 | 3eqtri 2648 |
. . . . . . . . . . . 12
|
92 | 86 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
93 | 92, 59 | eqtr4i 2647 |
. . . . . . . . . . . . . . 15
|
94 | 64 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
|
95 | 93, 94 | oveq12i 6662 |
. . . . . . . . . . . . . 14
|
96 | 95 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
97 | | 2ne0 11113 |
. . . . . . . . . . . . . 14
|
98 | 43, 33, 97 | divcan2i 10768 |
. . . . . . . . . . . . 13
|
99 | 96, 98 | eqtri 2644 |
. . . . . . . . . . . 12
|
100 | 91, 99 | oveq12i 6662 |
. . . . . . . . . . 11
|
101 | 100, 45 | eqtri 2644 |
. . . . . . . . . 10
|
102 | 66, 69, 101 | 3eqtri 2648 |
. . . . . . . . 9
|
103 | | 2t2e4 11177 |
. . . . . . . . . . . . . 14
|
104 | 103 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
105 | | df-5 11082 |
. . . . . . . . . . . . 13
|
106 | 104, 105 | eqtr4i 2647 |
. . . . . . . . . . . 12
|
107 | 59 | eqcomi 2631 |
. . . . . . . . . . . 12
|
108 | 106, 107 | oveq12i 6662 |
. . . . . . . . . . 11
|
109 | 108 | oveq2i 6661 |
. . . . . . . . . 10
|
110 | | 5cn 11100 |
. . . . . . . . . . 11
|
111 | | 3ne0 11115 |
. . . . . . . . . . 11
|
112 | 33, 110, 43, 111 | divassi 10781 |
. . . . . . . . . 10
|
113 | 109, 112 | eqtr4i 2647 |
. . . . . . . . 9
|
114 | 102, 113 | oveq12i 6662 |
. . . . . . . 8
|
115 | 63, 114 | eqtri 2644 |
. . . . . . 7
|
116 | | 6cn 11102 |
. . . . . . . . 9
|
117 | | 2nn 11185 |
. . . . . . . . . . 11
|
118 | | 5nn 11188 |
. . . . . . . . . . 11
|
119 | 117, 118 | nnmulcli 11044 |
. . . . . . . . . 10
|
120 | 119 | nncni 11030 |
. . . . . . . . 9
|
121 | 43, 111 | pm3.2i 471 |
. . . . . . . . 9
|
122 | | div12 10707 |
. . . . . . . . 9
|
123 | 116, 120,
121, 122 | mp3an 1424 |
. . . . . . . 8
|
124 | | 5t2e10 11634 |
. . . . . . . . . 10
; |
125 | 110, 33, 124 | mulcomli 10047 |
. . . . . . . . 9
; |
126 | 116, 43, 33, 111 | divmuli 10779 |
. . . . . . . . . 10
|
127 | 44, 126 | mpbir 221 |
. . . . . . . . 9
|
128 | 125, 127 | oveq12i 6662 |
. . . . . . . 8
; |
129 | 123, 128 | eqtri 2644 |
. . . . . . 7
; |
130 | 61, 115, 129 | 3eqtri 2648 |
. . . . . 6
; |
131 | 45 | oveq1i 6660 |
. . . . . . . . 9
|
132 | | df-7 11084 |
. . . . . . . . 9
|
133 | 131, 132 | eqtr4i 2647 |
. . . . . . . 8
|
134 | | 3p1e4 11153 |
. . . . . . . 8
|
135 | 133, 134 | oveq12i 6662 |
. . . . . . 7
|
136 | 135 | oveq2i 6661 |
. . . . . 6
|
137 | 130, 136 | oveq12i 6662 |
. . . . 5
; |
138 | 56, 58, 137 | 3eqtri 2648 |
. . . 4
; |
139 | | 10nn 11514 |
. . . . . . 7
; |
140 | 139 | nncni 11030 |
. . . . . 6
; |
141 | | 7cn 11104 |
. . . . . . . 8
|
142 | 141, 49, 50 | divcli 10767 |
. . . . . . 7
|
143 | 33, 142 | mulcli 10045 |
. . . . . 6
|
144 | 140, 33, 143 | mulassi 10049 |
. . . . 5
; ; |
145 | 103 | oveq1i 6660 |
. . . . . . 7
|
146 | 33, 33, 142 | mulassi 10049 |
. . . . . . 7
|
147 | 141, 49, 50 | divcan2i 10768 |
. . . . . . 7
|
148 | 145, 146,
147 | 3eqtr3i 2652 |
. . . . . 6
|
149 | 148 | oveq2i 6661 |
. . . . 5
; ; |
150 | 144, 149 | eqtri 2644 |
. . . 4
; ; |
151 | 27 | dec0u 11520 |
. . . 4
; ; |
152 | 138, 150,
151 | 3eqtri 2648 |
. . 3
; |
153 | 32, 53, 152 | 3brtr4i 4683 |
. 2
|
154 | | 4nn 11187 |
. . . 4
|
155 | | eluznn 11758 |
. . . 4
|
156 | 154, 155 | mpan 706 |
. . 3
|
157 | | nnnn0 11299 |
. . . . . . . . . 10
|
158 | | nnexpcl 12873 |
. . . . . . . . . 10
|
159 | 154, 157,
158 | sylancr 695 |
. . . . . . . . 9
|
160 | 159 | nnrpd 11870 |
. . . . . . . 8
|
161 | | nnrp 11842 |
. . . . . . . 8
|
162 | 160, 161 | rpdivcld 11889 |
. . . . . . 7
|
163 | 162 | rpred 11872 |
. . . . . 6
|
164 | | nnmulcl 11043 |
. . . . . . . . . 10
|
165 | 117, 164 | mpan 706 |
. . . . . . . . 9
|
166 | 165 | nnnn0d 11351 |
. . . . . . . 8
|
167 | | nnz 11399 |
. . . . . . . 8
|
168 | | bccl 13109 |
. . . . . . . 8
|
169 | 166, 167,
168 | syl2anc 693 |
. . . . . . 7
|
170 | 169 | nn0red 11352 |
. . . . . 6
|
171 | | 2rp 11837 |
. . . . . . 7
|
172 | 165 | peano2nnd 11037 |
. . . . . . . . 9
|
173 | 172 | nnrpd 11870 |
. . . . . . . 8
|
174 | | peano2nn 11032 |
. . . . . . . . 9
|
175 | 174 | nnrpd 11870 |
. . . . . . . 8
|
176 | 173, 175 | rpdivcld 11889 |
. . . . . . 7
|
177 | | rpmulcl 11855 |
. . . . . . 7
|
178 | 171, 176,
177 | sylancr 695 |
. . . . . 6
|
179 | 163, 170,
178 | ltmul1d 11913 |
. . . . 5
|
180 | | bcp1ctr 25004 |
. . . . . . 7
|
181 | 157, 180 | syl 17 |
. . . . . 6
|
182 | 181 | breq2d 4665 |
. . . . 5
|
183 | 179, 182 | bitr4d 271 |
. . . 4
|
184 | | 2re 11090 |
. . . . . . . 8
|
185 | 184 | a1i 11 |
. . . . . . 7
|
186 | 173, 161 | rpdivcld 11889 |
. . . . . . . 8
|
187 | 186 | rpred 11872 |
. . . . . . 7
|
188 | | nnmulcl 11043 |
. . . . . . . . . 10
|
189 | 159, 117,
188 | sylancl 694 |
. . . . . . . . 9
|
190 | 189 | nnrpd 11870 |
. . . . . . . 8
|
191 | 190, 175 | rpdivcld 11889 |
. . . . . . 7
|
192 | 161 | rpreccld 11882 |
. . . . . . . . 9
|
193 | | ltaddrp 11867 |
. . . . . . . . 9
|
194 | 184, 192,
193 | sylancr 695 |
. . . . . . . 8
|
195 | 165 | nncnd 11036 |
. . . . . . . . . 10
|
196 | | 1cnd 10056 |
. . . . . . . . . 10
|
197 | | nncn 11028 |
. . . . . . . . . 10
|
198 | | nnne0 11053 |
. . . . . . . . . 10
|
199 | 195, 196,
197, 198 | divdird 10839 |
. . . . . . . . 9
|
200 | 33 | a1i 11 |
. . . . . . . . . . 11
|
201 | 200, 197,
198 | divcan4d 10807 |
. . . . . . . . . 10
|
202 | 201 | oveq1d 6665 |
. . . . . . . . 9
|
203 | 199, 202 | eqtr2d 2657 |
. . . . . . . 8
|
204 | 194, 203 | breqtrd 4679 |
. . . . . . 7
|
205 | 185, 187,
191, 204 | ltmul2dd 11928 |
. . . . . 6
|
206 | | expp1 12867 |
. . . . . . . . . 10
|
207 | 49, 157, 206 | sylancr 695 |
. . . . . . . . 9
|
208 | 159 | nncnd 11036 |
. . . . . . . . . . 11
|
209 | 208, 200,
200 | mulassd 10063 |
. . . . . . . . . 10
|
210 | 103 | oveq2i 6661 |
. . . . . . . . . 10
|
211 | 209, 210 | syl6eq 2672 |
. . . . . . . . 9
|
212 | 207, 211 | eqtr4d 2659 |
. . . . . . . 8
|
213 | 212 | oveq1d 6665 |
. . . . . . 7
|
214 | 189 | nncnd 11036 |
. . . . . . . 8
|
215 | 174 | nncnd 11036 |
. . . . . . . 8
|
216 | 174 | nnne0d 11065 |
. . . . . . . 8
|
217 | 214, 200,
215, 216 | div23d 10838 |
. . . . . . 7
|
218 | 213, 217 | eqtrd 2656 |
. . . . . 6
|
219 | 208, 200,
197, 198 | div23d 10838 |
. . . . . . . 8
|
220 | 219 | oveq1d 6665 |
. . . . . . 7
|
221 | 172 | nncnd 11036 |
. . . . . . . 8
|
222 | 214, 197,
221, 215, 198, 216 | divmul24d 10844 |
. . . . . . 7
|
223 | 162 | rpcnd 11874 |
. . . . . . . 8
|
224 | 176 | rpcnd 11874 |
. . . . . . . 8
|
225 | 223, 200,
224 | mulassd 10063 |
. . . . . . 7
|
226 | 220, 222,
225 | 3eqtr3rd 2665 |
. . . . . 6
|
227 | 205, 218,
226 | 3brtr4d 4685 |
. . . . 5
|
228 | 174 | nnnn0d 11351 |
. . . . . . . . . 10
|
229 | | nnexpcl 12873 |
. . . . . . . . . 10
|
230 | 154, 228,
229 | sylancr 695 |
. . . . . . . . 9
|
231 | 230 | nnrpd 11870 |
. . . . . . . 8
|
232 | 231, 175 | rpdivcld 11889 |
. . . . . . 7
|
233 | 232 | rpred 11872 |
. . . . . 6
|
234 | 178 | rpred 11872 |
. . . . . . 7
|
235 | 163, 234 | remulcld 10070 |
. . . . . 6
|
236 | | nn0mulcl 11329 |
. . . . . . . . 9
|
237 | 34, 228, 236 | sylancr 695 |
. . . . . . . 8
|
238 | 174 | nnzd 11481 |
. . . . . . . 8
|
239 | | bccl 13109 |
. . . . . . . 8
|
240 | 237, 238,
239 | syl2anc 693 |
. . . . . . 7
|
241 | 240 | nn0red 11352 |
. . . . . 6
|
242 | | lttr 10114 |
. . . . . 6
|
243 | 233, 235,
241, 242 | syl3anc 1326 |
. . . . 5
|
244 | 227, 243 | mpand 711 |
. . . 4
|
245 | 183, 244 | sylbid 230 |
. . 3
|
246 | 156, 245 | syl 17 |
. 2
|
247 | 1, 7, 13, 19, 25, 153, 246 | uzind4i 11750 |
1
|