Step | Hyp | Ref
| Expression |
1 | | bpos.3 |
. . . . . 6
|
2 | | id 22 |
. . . . . . . 8
|
3 | | 5nn 11188 |
. . . . . . . . . . 11
|
4 | | bpos.1 |
. . . . . . . . . . 11
|
5 | | eluznn 11758 |
. . . . . . . . . . 11
|
6 | 3, 4, 5 | sylancr 695 |
. . . . . . . . . 10
|
7 | 6 | nnnn0d 11351 |
. . . . . . . . 9
|
8 | | fzctr 12451 |
. . . . . . . . 9
|
9 | | bccl2 13110 |
. . . . . . . . 9
|
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . 8
|
11 | | pccl 15554 |
. . . . . . . 8
|
12 | 2, 10, 11 | syl2anr 495 |
. . . . . . 7
|
13 | 12 | ralrimiva 2966 |
. . . . . 6
|
14 | 1, 13 | pcmptcl 15595 |
. . . . 5
|
15 | 14 | simprd 479 |
. . . 4
|
16 | | 3nn 11186 |
. . . . 5
|
17 | | bpos.5 |
. . . . . 6
|
18 | | 2z 11409 |
. . . . . . . . . . 11
|
19 | 6 | nnzd 11481 |
. . . . . . . . . . 11
|
20 | | zmulcl 11426 |
. . . . . . . . . . 11
|
21 | 18, 19, 20 | sylancr 695 |
. . . . . . . . . 10
|
22 | 21 | zred 11482 |
. . . . . . . . 9
|
23 | | 2nn 11185 |
. . . . . . . . . . . 12
|
24 | | nnmulcl 11043 |
. . . . . . . . . . . 12
|
25 | 23, 6, 24 | sylancr 695 |
. . . . . . . . . . 11
|
26 | 25 | nnrpd 11870 |
. . . . . . . . . 10
|
27 | 26 | rpge0d 11876 |
. . . . . . . . 9
|
28 | 22, 27 | resqrtcld 14156 |
. . . . . . . 8
|
29 | 28 | flcld 12599 |
. . . . . . 7
|
30 | | sqrt9 14014 |
. . . . . . . . 9
|
31 | | 9re 11107 |
. . . . . . . . . . . 12
|
32 | 31 | a1i 11 |
. . . . . . . . . . 11
|
33 | | 10re 11517 |
. . . . . . . . . . . 12
; |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
; |
35 | | lep1 10862 |
. . . . . . . . . . . . . 14
|
36 | 31, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
|
37 | | 9p1e10 11496 |
. . . . . . . . . . . . 13
; |
38 | 36, 37 | breqtri 4678 |
. . . . . . . . . . . 12
; |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
; |
40 | | 5cn 11100 |
. . . . . . . . . . . . 13
|
41 | | 2cn 11091 |
. . . . . . . . . . . . 13
|
42 | | 5t2e10 11634 |
. . . . . . . . . . . . 13
; |
43 | 40, 41, 42 | mulcomli 10047 |
. . . . . . . . . . . 12
; |
44 | | eluzle 11700 |
. . . . . . . . . . . . . 14
|
45 | 4, 44 | syl 17 |
. . . . . . . . . . . . 13
|
46 | 6 | nnred 11035 |
. . . . . . . . . . . . . 14
|
47 | | 5re 11099 |
. . . . . . . . . . . . . . 15
|
48 | | 2re 11090 |
. . . . . . . . . . . . . . . 16
|
49 | | 2pos 11112 |
. . . . . . . . . . . . . . . 16
|
50 | 48, 49 | pm3.2i 471 |
. . . . . . . . . . . . . . 15
|
51 | | lemul2 10876 |
. . . . . . . . . . . . . . 15
|
52 | 47, 50, 51 | mp3an13 1415 |
. . . . . . . . . . . . . 14
|
53 | 46, 52 | syl 17 |
. . . . . . . . . . . . 13
|
54 | 45, 53 | mpbid 222 |
. . . . . . . . . . . 12
|
55 | 43, 54 | syl5eqbrr 4689 |
. . . . . . . . . . 11
;
|
56 | 32, 34, 22, 39, 55 | letrd 10194 |
. . . . . . . . . 10
|
57 | | 0re 10040 |
. . . . . . . . . . . . 13
|
58 | | 9pos 11122 |
. . . . . . . . . . . . 13
|
59 | 57, 31, 58 | ltleii 10160 |
. . . . . . . . . . . 12
|
60 | 31, 59 | pm3.2i 471 |
. . . . . . . . . . 11
|
61 | 22, 27 | jca 554 |
. . . . . . . . . . 11
|
62 | | sqrtle 14001 |
. . . . . . . . . . 11
|
63 | 60, 61, 62 | sylancr 695 |
. . . . . . . . . 10
|
64 | 56, 63 | mpbid 222 |
. . . . . . . . 9
|
65 | 30, 64 | syl5eqbrr 4689 |
. . . . . . . 8
|
66 | | 3z 11410 |
. . . . . . . . 9
|
67 | | flge 12606 |
. . . . . . . . 9
|
68 | 28, 66, 67 | sylancl 694 |
. . . . . . . 8
|
69 | 65, 68 | mpbid 222 |
. . . . . . 7
|
70 | 66 | eluz1i 11695 |
. . . . . . 7
|
71 | 29, 69, 70 | sylanbrc 698 |
. . . . . 6
|
72 | 17, 71 | syl5eqel 2705 |
. . . . 5
|
73 | | eluznn 11758 |
. . . . 5
|
74 | 16, 72, 73 | sylancr 695 |
. . . 4
|
75 | 15, 74 | ffvelrnd 6360 |
. . 3
|
76 | 75 | nnred 11035 |
. 2
|
77 | 74 | nnred 11035 |
. . . . 5
|
78 | | ppicl 24857 |
. . . . 5
π |
79 | 77, 78 | syl 17 |
. . . 4
π |
80 | 25, 79 | nnexpcld 13030 |
. . 3
π |
81 | 80 | nnred 11035 |
. 2
π |
82 | | nndivre 11056 |
. . . . 5
|
83 | 28, 16, 82 | sylancl 694 |
. . . 4
|
84 | | readdcl 10019 |
. . . 4
|
85 | 83, 48, 84 | sylancl 694 |
. . 3
|
86 | 22, 27, 85 | recxpcld 24469 |
. 2
|
87 | | fveq2 6191 |
. . . . . 6
|
88 | | fveq2 6191 |
. . . . . . . 8
π π |
89 | | ppi1 24890 |
. . . . . . . 8
π |
90 | 88, 89 | syl6eq 2672 |
. . . . . . 7
π |
91 | 90 | oveq2d 6666 |
. . . . . 6
π |
92 | 87, 91 | breq12d 4666 |
. . . . 5
π
|
93 | 92 | imbi2d 330 |
. . . 4
π |
94 | | fveq2 6191 |
. . . . . 6
|
95 | | fveq2 6191 |
. . . . . . 7
π π |
96 | 95 | oveq2d 6666 |
. . . . . 6
π π |
97 | 94, 96 | breq12d 4666 |
. . . . 5
π
π |
98 | 97 | imbi2d 330 |
. . . 4
π π |
99 | | fveq2 6191 |
. . . . . 6
|
100 | | fveq2 6191 |
. . . . . . 7
π π |
101 | 100 | oveq2d 6666 |
. . . . . 6
π π |
102 | 99, 101 | breq12d 4666 |
. . . . 5
π
π |
103 | 102 | imbi2d 330 |
. . . 4
π π |
104 | | fveq2 6191 |
. . . . . 6
|
105 | | fveq2 6191 |
. . . . . . 7
π π |
106 | 105 | oveq2d 6666 |
. . . . . 6
π π |
107 | 104, 106 | breq12d 4666 |
. . . . 5
π
π |
108 | 107 | imbi2d 330 |
. . . 4
π π |
109 | | 1z 11407 |
. . . . . . . 8
|
110 | | seq1 12814 |
. . . . . . . 8
|
111 | 109, 110 | ax-mp 5 |
. . . . . . 7
|
112 | | 1nn 11031 |
. . . . . . . 8
|
113 | | 1nprm 15392 |
. . . . . . . . . . 11
|
114 | | eleq1 2689 |
. . . . . . . . . . 11
|
115 | 113, 114 | mtbiri 317 |
. . . . . . . . . 10
|
116 | 115 | iffalsed 4097 |
. . . . . . . . 9
|
117 | | 1ex 10035 |
. . . . . . . . 9
|
118 | 116, 1, 117 | fvmpt 6282 |
. . . . . . . 8
|
119 | 112, 118 | ax-mp 5 |
. . . . . . 7
|
120 | 111, 119 | eqtri 2644 |
. . . . . 6
|
121 | | 1le1 10655 |
. . . . . 6
|
122 | 120, 121 | eqbrtri 4674 |
. . . . 5
|
123 | 21 | zcnd 11483 |
. . . . . 6
|
124 | 123 | exp0d 13002 |
. . . . 5
|
125 | 122, 124 | syl5breqr 4691 |
. . . 4
|
126 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
127 | 126 | nnred 11035 |
. . . . . . . . . . 11
|
128 | 127 | adantr 481 |
. . . . . . . . . 10
|
129 | 25 | ad2antrr 762 |
. . . . . . . . . . . 12
|
130 | | nnre 11027 |
. . . . . . . . . . . . . 14
|
131 | 130 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
132 | | ppicl 24857 |
. . . . . . . . . . . . 13
π |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . 12
π |
134 | 129, 133 | nnexpcld 13030 |
. . . . . . . . . . 11
π |
135 | 134 | nnred 11035 |
. . . . . . . . . 10
π |
136 | | nnre 11027 |
. . . . . . . . . . . . 13
|
137 | | nngt0 11049 |
. . . . . . . . . . . . 13
|
138 | 136, 137 | jca 554 |
. . . . . . . . . . . 12
|
139 | 25, 138 | syl 17 |
. . . . . . . . . . 11
|
140 | 139 | ad2antrr 762 |
. . . . . . . . . 10
|
141 | | lemul1 10875 |
. . . . . . . . . 10
π
π π |
142 | 128, 135,
140, 141 | syl3anc 1326 |
. . . . . . . . 9
π
π |
143 | | nnz 11399 |
. . . . . . . . . . . . . 14
|
144 | 143 | adantl 482 |
. . . . . . . . . . . . 13
|
145 | | ppiprm 24877 |
. . . . . . . . . . . . 13
π π |
146 | 144, 145 | sylan 488 |
. . . . . . . . . . . 12
π π |
147 | 146 | oveq2d 6666 |
. . . . . . . . . . 11
π π |
148 | 123 | ad2antrr 762 |
. . . . . . . . . . . 12
|
149 | 148, 133 | expp1d 13009 |
. . . . . . . . . . 11
π π |
150 | 147, 149 | eqtrd 2656 |
. . . . . . . . . 10
π π |
151 | 150 | breq2d 4665 |
. . . . . . . . 9
π
π |
152 | 142, 151 | bitr4d 271 |
. . . . . . . 8
π
π |
153 | | simpr 477 |
. . . . . . . . . . . . 13
|
154 | | nnuz 11723 |
. . . . . . . . . . . . 13
|
155 | 153, 154 | syl6eleq 2711 |
. . . . . . . . . . . 12
|
156 | | seqp1 12816 |
. . . . . . . . . . . 12
|
157 | 155, 156 | syl 17 |
. . . . . . . . . . 11
|
158 | 157 | adantr 481 |
. . . . . . . . . 10
|
159 | | peano2nn 11032 |
. . . . . . . . . . . . . . 15
|
160 | 159 | adantl 482 |
. . . . . . . . . . . . . 14
|
161 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
162 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
163 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
164 | 162, 163 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
165 | 161, 164 | ifbieq1d 4109 |
. . . . . . . . . . . . . . 15
|
166 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
167 | 166, 117 | ifex 4156 |
. . . . . . . . . . . . . . 15
|
168 | 165, 1, 167 | fvmpt 6282 |
. . . . . . . . . . . . . 14
|
169 | 160, 168 | syl 17 |
. . . . . . . . . . . . 13
|
170 | | iftrue 4092 |
. . . . . . . . . . . . 13
|
171 | 169, 170 | sylan9eq 2676 |
. . . . . . . . . . . 12
|
172 | 6 | adantr 481 |
. . . . . . . . . . . . 13
|
173 | | bposlem1 25009 |
. . . . . . . . . . . . 13
|
174 | 172, 173 | sylan 488 |
. . . . . . . . . . . 12
|
175 | 171, 174 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
176 | 14 | simpld 475 |
. . . . . . . . . . . . . . 15
|
177 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
|
178 | 176, 159,
177 | syl2an 494 |
. . . . . . . . . . . . . 14
|
179 | 178 | nnred 11035 |
. . . . . . . . . . . . 13
|
180 | 179 | adantr 481 |
. . . . . . . . . . . 12
|
181 | 22 | ad2antrr 762 |
. . . . . . . . . . . 12
|
182 | | nnre 11027 |
. . . . . . . . . . . . . . 15
|
183 | | nngt0 11049 |
. . . . . . . . . . . . . . 15
|
184 | 182, 183 | jca 554 |
. . . . . . . . . . . . . 14
|
185 | 126, 184 | syl 17 |
. . . . . . . . . . . . 13
|
186 | 185 | adantr 481 |
. . . . . . . . . . . 12
|
187 | | lemul2 10876 |
. . . . . . . . . . . 12
|
188 | 180, 181,
186, 187 | syl3anc 1326 |
. . . . . . . . . . 11
|
189 | 175, 188 | mpbid 222 |
. . . . . . . . . 10
|
190 | 158, 189 | eqbrtrd 4675 |
. . . . . . . . 9
|
191 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
|
192 | 15, 159, 191 | syl2an 494 |
. . . . . . . . . . . 12
|
193 | 192 | nnred 11035 |
. . . . . . . . . . 11
|
194 | 25 | adantr 481 |
. . . . . . . . . . . . 13
|
195 | 126, 194 | nnmulcld 11068 |
. . . . . . . . . . . 12
|
196 | 195 | nnred 11035 |
. . . . . . . . . . 11
|
197 | 160 | nnred 11035 |
. . . . . . . . . . . . . 14
|
198 | | ppicl 24857 |
. . . . . . . . . . . . . 14
π |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . 13
π |
200 | 194, 199 | nnexpcld 13030 |
. . . . . . . . . . . 12
π |
201 | 200 | nnred 11035 |
. . . . . . . . . . 11
π |
202 | | letr 10131 |
. . . . . . . . . . 11
π π
π |
203 | 193, 196,
201, 202 | syl3anc 1326 |
. . . . . . . . . 10
π
π |
204 | 203 | adantr 481 |
. . . . . . . . 9
π
π |
205 | 190, 204 | mpand 711 |
. . . . . . . 8
π
π |
206 | 152, 205 | sylbid 230 |
. . . . . . 7
π
π |
207 | 157 | adantr 481 |
. . . . . . . . . 10
|
208 | | iffalse 4095 |
. . . . . . . . . . . 12
|
209 | 169, 208 | sylan9eq 2676 |
. . . . . . . . . . 11
|
210 | 209 | oveq2d 6666 |
. . . . . . . . . 10
|
211 | 126 | adantr 481 |
. . . . . . . . . . . 12
|
212 | 211 | nncnd 11036 |
. . . . . . . . . . 11
|
213 | 212 | mulid1d 10057 |
. . . . . . . . . 10
|
214 | 207, 210,
213 | 3eqtrd 2660 |
. . . . . . . . 9
|
215 | | ppinprm 24878 |
. . . . . . . . . . 11
π π |
216 | 144, 215 | sylan 488 |
. . . . . . . . . 10
π π |
217 | 216 | oveq2d 6666 |
. . . . . . . . 9
π π |
218 | 214, 217 | breq12d 4666 |
. . . . . . . 8
π π |
219 | 218 | biimprd 238 |
. . . . . . 7
π π |
220 | 206, 219 | pm2.61dan 832 |
. . . . . 6
π
π |
221 | 220 | expcom 451 |
. . . . 5
π π |
222 | 221 | a2d 29 |
. . . 4
π
π |
223 | 93, 98, 103, 108, 125, 222 | nnind 11038 |
. . 3
π |
224 | 74, 223 | mpcom 38 |
. 2
π |
225 | | cxpexp 24414 |
. . . 4
π π π |
226 | 123, 79, 225 | syl2anc 693 |
. . 3
π π |
227 | 79 | nn0red 11352 |
. . . . 5
π |
228 | | nndivre 11056 |
. . . . . . 7
|
229 | 77, 16, 228 | sylancl 694 |
. . . . . 6
|
230 | | readdcl 10019 |
. . . . . 6
|
231 | 229, 48, 230 | sylancl 694 |
. . . . 5
|
232 | 74 | nnnn0d 11351 |
. . . . . . 7
|
233 | 232 | nn0ge0d 11354 |
. . . . . 6
|
234 | | ppiub 24929 |
. . . . . 6
π |
235 | 77, 233, 234 | syl2anc 693 |
. . . . 5
π |
236 | 48 | a1i 11 |
. . . . . 6
|
237 | | flle 12600 |
. . . . . . . . 9
|
238 | 28, 237 | syl 17 |
. . . . . . . 8
|
239 | 17, 238 | syl5eqbr 4688 |
. . . . . . 7
|
240 | | 3re 11094 |
. . . . . . . . . 10
|
241 | | 3pos 11114 |
. . . . . . . . . 10
|
242 | 240, 241 | pm3.2i 471 |
. . . . . . . . 9
|
243 | 242 | a1i 11 |
. . . . . . . 8
|
244 | | lediv1 10888 |
. . . . . . . 8
|
245 | 77, 28, 243, 244 | syl3anc 1326 |
. . . . . . 7
|
246 | 239, 245 | mpbid 222 |
. . . . . 6
|
247 | 229, 83, 236, 246 | leadd1dd 10641 |
. . . . 5
|
248 | 227, 231,
85, 235, 247 | letrd 10194 |
. . . 4
π |
249 | | 2t1e2 11176 |
. . . . . . . 8
|
250 | 6 | nnge1d 11063 |
. . . . . . . . 9
|
251 | | 1re 10039 |
. . . . . . . . . . 11
|
252 | | lemul2 10876 |
. . . . . . . . . . 11
|
253 | 251, 50, 252 | mp3an13 1415 |
. . . . . . . . . 10
|
254 | 46, 253 | syl 17 |
. . . . . . . . 9
|
255 | 250, 254 | mpbid 222 |
. . . . . . . 8
|
256 | 249, 255 | syl5eqbrr 4689 |
. . . . . . 7
|
257 | 18 | eluz1i 11695 |
. . . . . . 7
|
258 | 21, 256, 257 | sylanbrc 698 |
. . . . . 6
|
259 | | eluz2gt1 11760 |
. . . . . 6
|
260 | 258, 259 | syl 17 |
. . . . 5
|
261 | 22, 260, 227, 85 | cxpled 24466 |
. . . 4
π π |
262 | 248, 261 | mpbid 222 |
. . 3
π |
263 | 226, 262 | eqbrtrrd 4677 |
. 2
π |
264 | 76, 81, 86, 224, 263 | letrd 10194 |
1
|