Step | Hyp | Ref
| Expression |
1 | | bpos.3 |
. . . . . 6
       
          |
2 | | id 22 |
. . . . . . . 8

  |
3 | | 5nn 10770 |
. . . . . . . . . . 11
 |
4 | | bpos.1 |
. . . . . . . . . . 11
       |
5 | | eluznn 11229 |
. . . . . . . . . . 11
 
    
  |
6 | 3, 4, 5 | sylancr 669 |
. . . . . . . . . 10
   |
7 | 6 | nnnn0d 10925 |
. . . . . . . . 9
   |
8 | | fzctr 11903 |
. . . . . . . . 9

        |
9 | | bccl2 12508 |
. . . . . . . . 9
             |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . 8
       |
11 | | pccl 14799 |
. . . . . . . 8
               |
12 | 2, 10, 11 | syl2anr 481 |
. . . . . . 7
 

        |
13 | 12 | ralrimiva 2802 |
. . . . . 6
  
       |
14 | 1, 13 | pcmptcl 14836 |
. . . . 5
                |
15 | 14 | simprd 465 |
. . . 4
          |
16 | | 3nn 10768 |
. . . . 5
 |
17 | | bpos.5 |
. . . . . 6
           |
18 | | 2z 10969 |
. . . . . . . . . . 11
 |
19 | 6 | nnzd 11039 |
. . . . . . . . . . 11
   |
20 | | zmulcl 10985 |
. . . . . . . . . . 11
 
     |
21 | 18, 19, 20 | sylancr 669 |
. . . . . . . . . 10
     |
22 | 21 | zred 11040 |
. . . . . . . . 9
     |
23 | | 2nn 10767 |
. . . . . . . . . . . 12
 |
24 | | nnmulcl 10632 |
. . . . . . . . . . . 12
 
     |
25 | 23, 6, 24 | sylancr 669 |
. . . . . . . . . . 11
     |
26 | 25 | nnrpd 11339 |
. . . . . . . . . 10
     |
27 | 26 | rpge0d 11345 |
. . . . . . . . 9

    |
28 | 22, 27 | resqrtcld 13479 |
. . . . . . . 8
         |
29 | 28 | flcld 12034 |
. . . . . . 7
             |
30 | | sqrt9 13337 |
. . . . . . . . 9
     |
31 | | 9re 10696 |
. . . . . . . . . . . 12
 |
32 | 31 | a1i 11 |
. . . . . . . . . . 11
   |
33 | | 10re 10698 |
. . . . . . . . . . . 12
 |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
   |
35 | | lep1 10444 |
. . . . . . . . . . . . . 14
     |
36 | 31, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
   |
37 | | df-10 10676 |
. . . . . . . . . . . . 13
   |
38 | 36, 37 | breqtrri 4428 |
. . . . . . . . . . . 12
 |
39 | 38 | a1i 11 |
. . . . . . . . . . 11

  |
40 | | 5cn 10689 |
. . . . . . . . . . . . 13
 |
41 | | 2cn 10680 |
. . . . . . . . . . . . 13
 |
42 | | 5t2e10 10764 |
. . . . . . . . . . . . 13
   |
43 | 40, 41, 42 | mulcomli 9650 |
. . . . . . . . . . . 12
   |
44 | | eluzle 11171 |
. . . . . . . . . . . . . 14
    
  |
45 | 4, 44 | syl 17 |
. . . . . . . . . . . . 13

  |
46 | 6 | nnred 10624 |
. . . . . . . . . . . . . 14
   |
47 | | 5re 10688 |
. . . . . . . . . . . . . . 15
 |
48 | | 2re 10679 |
. . . . . . . . . . . . . . . 16
 |
49 | | 2pos 10701 |
. . . . . . . . . . . . . . . 16
 |
50 | 48, 49 | pm3.2i 457 |
. . . . . . . . . . . . . . 15
   |
51 | | lemul2 10458 |
. . . . . . . . . . . . . . 15
 
     
     |
52 | 47, 50, 51 | mp3an13 1355 |
. . . . . . . . . . . . . 14
 
       |
53 | 46, 52 | syl 17 |
. . . . . . . . . . . . 13
         |
54 | 45, 53 | mpbid 214 |
. . . . . . . . . . . 12
  
    |
55 | 43, 54 | syl5eqbrr 4437 |
. . . . . . . . . . 11

    |
56 | 32, 34, 22, 39, 55 | letrd 9792 |
. . . . . . . . . 10

    |
57 | | 0re 9643 |
. . . . . . . . . . . . 13
 |
58 | | 9pos 10711 |
. . . . . . . . . . . . 13
 |
59 | 57, 31, 58 | ltleii 9757 |
. . . . . . . . . . . 12
 |
60 | 31, 59 | pm3.2i 457 |
. . . . . . . . . . 11
   |
61 | 22, 27 | jca 535 |
. . . . . . . . . . 11
   
     |
62 | | sqrtle 13324 |
. . . . . . . . . . 11
  
              
         |
63 | 60, 61, 62 | sylancr 669 |
. . . . . . . . . 10
       
         |
64 | 56, 63 | mpbid 214 |
. . . . . . . . 9
    
        |
65 | 30, 64 | syl5eqbrr 4437 |
. . . . . . . 8

        |
66 | | 3z 10970 |
. . . . . . . . 9
 |
67 | | flge 12041 |
. . . . . . . . 9
       
       
             |
68 | 28, 66, 67 | sylancl 668 |
. . . . . . . 8
       
             |
69 | 65, 68 | mpbid 214 |
. . . . . . 7

            |
70 | 66 | eluz1i 11166 |
. . . . . . 7
                                       |
71 | 29, 69, 70 | sylanbrc 670 |
. . . . . 6
                 |
72 | 17, 71 | syl5eqel 2533 |
. . . . 5
       |
73 | | eluznn 11229 |
. . . . 5
 
    
  |
74 | 16, 72, 73 | sylancr 669 |
. . . 4
   |
75 | 15, 74 | ffvelrnd 6023 |
. . 3
         |
76 | 75 | nnred 10624 |
. 2
         |
77 | 74 | nnred 10624 |
. . . . 5
   |
78 | | ppicl 24058 |
. . . . 5
 π    |
79 | 77, 78 | syl 17 |
. . . 4
 π    |
80 | 25, 79 | nnexpcld 12437 |
. . 3
      π     |
81 | 80 | nnred 10624 |
. 2
      π     |
82 | | nndivre 10645 |
. . . . 5
       
           |
83 | 28, 16, 82 | sylancl 668 |
. . . 4
           |
84 | | readdcl 9622 |
. . . 4
                       |
85 | 83, 48, 84 | sylancl 668 |
. . 3
             |
86 | 22, 27, 85 | recxpcld 23668 |
. 2
                  |
87 | | fveq2 5865 |
. . . . . 6
               |
88 | | fveq2 5865 |
. . . . . . . 8
 π  π    |
89 | | ppi1 24091 |
. . . . . . . 8
π   |
90 | 88, 89 | syl6eq 2501 |
. . . . . . 7
 π    |
91 | 90 | oveq2d 6306 |
. . . . . 6
      π           |
92 | 87, 91 | breq12d 4415 |
. . . . 5
             π  
     
         |
93 | 92 | imbi2d 318 |
. . . 4
  
     
     π                     |
94 | | fveq2 5865 |
. . . . . 6
               |
95 | | fveq2 5865 |
. . . . . . 7
 π  π    |
96 | 95 | oveq2d 6306 |
. . . . . 6
      π        π     |
97 | 94, 96 | breq12d 4415 |
. . . . 5
             π  
     
     π      |
98 | 97 | imbi2d 318 |
. . . 4
  
     
     π                π       |
99 | | fveq2 5865 |
. . . . . 6
                   |
100 | | fveq2 5865 |
. . . . . . 7
   π  π      |
101 | 100 | oveq2d 6306 |
. . . . . 6
        π        π       |
102 | 99, 101 | breq12d 4415 |
. . . . 5
               π  
       
     π        |
103 | 102 | imbi2d 318 |
. . . 4
    
     
     π                  π         |
104 | | fveq2 5865 |
. . . . . 6
               |
105 | | fveq2 5865 |
. . . . . . 7
 π  π    |
106 | 105 | oveq2d 6306 |
. . . . . 6
      π        π     |
107 | 104, 106 | breq12d 4415 |
. . . . 5
             π  
     
     π      |
108 | 107 | imbi2d 318 |
. . . 4
  
     
     π                π       |
109 | | 1z 10967 |
. . . . . . . 8
 |
110 | | seq1 12226 |
. . . . . . . 8
             |
111 | 109, 110 | ax-mp 5 |
. . . . . . 7
           |
112 | | 1nn 10620 |
. . . . . . . 8
 |
113 | | 1nprm 14629 |
. . . . . . . . . . 11
 |
114 | | eleq1 2517 |
. . . . . . . . . . 11
 
   |
115 | 113, 114 | mtbiri 305 |
. . . . . . . . . 10

  |
116 | 115 | iffalsed 3892 |
. . . . . . . . 9
  
    
          |
117 | | 1ex 9638 |
. . . . . . . . 9
 |
118 | 116, 1, 117 | fvmpt 5948 |
. . . . . . . 8
       |
119 | 112, 118 | ax-mp 5 |
. . . . . . 7
     |
120 | 111, 119 | eqtri 2473 |
. . . . . 6
       |
121 | | 1le1 10240 |
. . . . . 6
 |
122 | 120, 121 | eqbrtri 4422 |
. . . . 5
     
 |
123 | 21 | zcnd 11041 |
. . . . . 6
     |
124 | 123 | exp0d 12410 |
. . . . 5
         |
125 | 122, 124 | syl5breqr 4439 |
. . . 4
               |
126 | 15 | ffvelrnda 6022 |
. . . . . . . . . . . 12
 

        |
127 | 126 | nnred 10624 |
. . . . . . . . . . 11
 

        |
128 | 127 | adantr 467 |
. . . . . . . . . 10
               |
129 | 25 | ad2antrr 732 |
. . . . . . . . . . . 12
           |
130 | | nnre 10616 |
. . . . . . . . . . . . . 14
   |
131 | 130 | ad2antlr 733 |
. . . . . . . . . . . . 13
         |
132 | | ppicl 24058 |
. . . . . . . . . . . . 13
 π    |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . 12
       π    |
134 | 129, 133 | nnexpcld 12437 |
. . . . . . . . . . 11
            π     |
135 | 134 | nnred 10624 |
. . . . . . . . . 10
            π     |
136 | | nnre 10616 |
. . . . . . . . . . . . 13
       |
137 | | nngt0 10638 |
. . . . . . . . . . . . 13
       |
138 | 136, 137 | jca 535 |
. . . . . . . . . . . 12
           |
139 | 25, 138 | syl 17 |
. . . . . . . . . . 11
         |
140 | 139 | ad2antrr 732 |
. . . . . . . . . 10
               |
141 | | lemul1 10457 |
. . . . . . . . . 10
             π                
     π                   π         |
142 | 128, 135,
140, 141 | syl3anc 1268 |
. . . . . . . . 9
                   π  
                π         |
143 | | nnz 10959 |
. . . . . . . . . . . . . 14
   |
144 | 143 | adantl 468 |
. . . . . . . . . . . . 13
 

  |
145 | | ppiprm 24078 |
. . . . . . . . . . . . 13
     π     π     |
146 | 144, 145 | sylan 474 |
. . . . . . . . . . . 12
       π     π     |
147 | 146 | oveq2d 6306 |
. . . . . . . . . . 11
            π           π      |
148 | 123 | ad2antrr 732 |
. . . . . . . . . . . 12
           |
149 | 148, 133 | expp1d 12417 |
. . . . . . . . . . 11
             π          π        |
150 | 147, 149 | eqtrd 2485 |
. . . . . . . . . 10
            π           π        |
151 | 150 | breq2d 4414 |
. . . . . . . . 9
                       π    
                π         |
152 | 142, 151 | bitr4d 260 |
. . . . . . . 8
                   π  
               π        |
153 | | simpr 463 |
. . . . . . . . . . . . 13
 

  |
154 | | nnuz 11194 |
. . . . . . . . . . . . 13
     |
155 | 153, 154 | syl6eleq 2539 |
. . . . . . . . . . . 12
 

      |
156 | | seqp1 12228 |
. . . . . . . . . . . 12
    
                        |
157 | 155, 156 | syl 17 |
. . . . . . . . . . 11
 

                        |
158 | 157 | adantr 467 |
. . . . . . . . . 10
                               |
159 | | peano2nn 10621 |
. . . . . . . . . . . . . . 15
     |
160 | 159 | adantl 468 |
. . . . . . . . . . . . . 14
 

    |
161 | | eleq1 2517 |
. . . . . . . . . . . . . . . 16
   
     |
162 | | id 22 |
. . . . . . . . . . . . . . . . 17
       |
163 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
   
               |
164 | 162, 163 | oveq12d 6308 |
. . . . . . . . . . . . . . . 16
                             |
165 | 161, 164 | ifbieq1d 3904 |
. . . . . . . . . . . . . . 15
    
    
                               |
166 | | ovex 6318 |
. . . . . . . . . . . . . . . 16
               |
167 | 166, 117 | ifex 3949 |
. . . . . . . . . . . . . . 15
                      |
168 | 165, 1, 167 | fvmpt 5948 |
. . . . . . . . . . . . . 14
                                |
169 | 160, 168 | syl 17 |
. . . . . . . . . . . . 13
 

          
                  |
170 | | iftrue 3887 |
. . . . . . . . . . . . 13
  
                            
        |
171 | 169, 170 | sylan9eq 2505 |
. . . . . . . . . . . 12
                             |
172 | 6 | adantr 467 |
. . . . . . . . . . . . 13
 

  |
173 | | bposlem1 24212 |
. . . . . . . . . . . . 13
            
     
    |
174 | 172, 173 | sylan 474 |
. . . . . . . . . . . 12
                         |
175 | 171, 174 | eqbrtrd 4423 |
. . . . . . . . . . 11
                 |
176 | 14 | simpld 461 |
. . . . . . . . . . . . . . 15
       |
177 | | ffvelrn 6020 |
. . . . . . . . . . . . . . 15
                 |
178 | 176, 159,
177 | syl2an 480 |
. . . . . . . . . . . . . 14
 

        |
179 | 178 | nnred 10624 |
. . . . . . . . . . . . 13
 

        |
180 | 179 | adantr 467 |
. . . . . . . . . . . 12
               |
181 | 22 | ad2antrr 732 |
. . . . . . . . . . . 12
           |
182 | | nnre 10616 |
. . . . . . . . . . . . . . 15
               |
183 | | nngt0 10638 |
. . . . . . . . . . . . . . 15
               |
184 | 182, 183 | jca 535 |
. . . . . . . . . . . . . 14
                       |
185 | 126, 184 | syl 17 |
. . . . . . . . . . . . 13
 

                |
186 | 185 | adantr 467 |
. . . . . . . . . . . 12
                       |
187 | | lemul2 10458 |
. . . . . . . . . . . 12
                                                             |
188 | 180, 181,
186, 187 | syl3anc 1268 |
. . . . . . . . . . 11
             
 
                           |
189 | 175, 188 | mpbid 214 |
. . . . . . . . . 10
                    
            |
190 | 158, 189 | eqbrtrd 4423 |
. . . . . . . . 9
              
            |
191 | | ffvelrn 6020 |
. . . . . . . . . . . . 13
                     |
192 | 15, 159, 191 | syl2an 480 |
. . . . . . . . . . . 12
 

          |
193 | 192 | nnred 10624 |
. . . . . . . . . . 11
 

          |
194 | 25 | adantr 467 |
. . . . . . . . . . . . 13
 

    |
195 | 126, 194 | nnmulcld 10657 |
. . . . . . . . . . . 12
 

            |
196 | 195 | nnred 10624 |
. . . . . . . . . . 11
 

            |
197 | 160 | nnred 10624 |
. . . . . . . . . . . . . 14
 

    |
198 | | ppicl 24058 |
. . . . . . . . . . . . . 14
   π      |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . 13
 

π      |
200 | 194, 199 | nnexpcld 12437 |
. . . . . . . . . . . 12
 

     π       |
201 | 200 | nnred 10624 |
. . . . . . . . . . 11
 

     π       |
202 | | letr 9727 |
. . . . . . . . . . 11
                         π                                         π     
       
     π        |
203 | 193, 196,
201, 202 | syl3anc 1268 |
. . . . . . . . . 10
 

                             
     π     
       
     π        |
204 | 203 | adantr 467 |
. . . . . . . . 9
                                          π     
       
     π        |
205 | 190, 204 | mpand 681 |
. . . . . . . 8
                       π            
     π        |
206 | 152, 205 | sylbid 219 |
. . . . . . 7
                   π          
     π        |
207 | 157 | adantr 467 |
. . . . . . . . . 10
                               |
208 | | iffalse 3890 |
. . . . . . . . . . . 12
               
          |
209 | 169, 208 | sylan9eq 2505 |
. . . . . . . . . . 11
               |
210 | 209 | oveq2d 6306 |
. . . . . . . . . 10
                               |
211 | 126 | adantr 467 |
. . . . . . . . . . . 12
               |
212 | 211 | nncnd 10625 |
. . . . . . . . . . 11
               |
213 | 212 | mulid1d 9660 |
. . . . . . . . . 10
                       |
214 | 207, 210,
213 | 3eqtrd 2489 |
. . . . . . . . 9
                       |
215 | | ppinprm 24079 |
. . . . . . . . . . 11
     π    π    |
216 | 144, 215 | sylan 474 |
. . . . . . . . . 10
       π    π    |
217 | 216 | oveq2d 6306 |
. . . . . . . . 9
            π          π     |
218 | 214, 217 | breq12d 4415 |
. . . . . . . 8
                     π                π      |
219 | 218 | biimprd 227 |
. . . . . . 7
                   π                π        |
220 | 206, 219 | pm2.61dan 800 |
. . . . . 6
 

            π          
     π        |
221 | 220 | expcom 437 |
. . . . 5
        
     π                π         |
222 | 221 | a2d 29 |
. . . 4
  
     
     π   
              π         |
223 | 93, 98, 103, 108, 125, 222 | nnind 10627 |
. . 3
             π      |
224 | 74, 223 | mpcom 37 |
. 2
            π     |
225 | | cxpexp 23613 |
. . . 4
    π       π        π     |
226 | 123, 79, 225 | syl2anc 667 |
. . 3
     π        π     |
227 | 79 | nn0red 10926 |
. . . . 5
 π    |
228 | | nndivre 10645 |
. . . . . . 7
 
     |
229 | 77, 16, 228 | sylancl 668 |
. . . . . 6
     |
230 | | readdcl 9622 |
. . . . . 6
   
       |
231 | 229, 48, 230 | sylancl 668 |
. . . . 5
       |
232 | 74 | nnnn0d 10925 |
. . . . . . 7
   |
233 | 232 | nn0ge0d 10928 |
. . . . . 6

  |
234 | | ppiub 24132 |
. . . . . 6
   π        |
235 | 77, 233, 234 | syl2anc 667 |
. . . . 5
 π        |
236 | 48 | a1i 11 |
. . . . . 6
   |
237 | | flle 12035 |
. . . . . . . . 9
                         |
238 | 28, 237 | syl 17 |
. . . . . . . 8
                   |
239 | 17, 238 | syl5eqbr 4436 |
. . . . . . 7

        |
240 | | 3re 10683 |
. . . . . . . . . 10
 |
241 | | 3pos 10703 |
. . . . . . . . . 10
 |
242 | 240, 241 | pm3.2i 457 |
. . . . . . . . 9
   |
243 | 242 | a1i 11 |
. . . . . . . 8
     |
244 | | lediv1 10470 |
. . . . . . . 8
                               |
245 | 77, 28, 243, 244 | syl3anc 1268 |
. . . . . . 7
       
             |
246 | 239, 245 | mpbid 214 |
. . . . . 6
  
          |
247 | 229, 83, 236, 246 | leadd1dd 10227 |
. . . . 5
    
            |
248 | 227, 231,
85, 235, 247 | letrd 9792 |
. . . 4
 π              |
249 | | 2t1e2 10758 |
. . . . . . . 8
   |
250 | 6 | nnge1d 10652 |
. . . . . . . . 9

  |
251 | | 1re 9642 |
. . . . . . . . . . 11
 |
252 | | lemul2 10458 |
. . . . . . . . . . 11
 
     
     |
253 | 251, 50, 252 | mp3an13 1355 |
. . . . . . . . . 10
 
       |
254 | 46, 253 | syl 17 |
. . . . . . . . 9
         |
255 | 250, 254 | mpbid 214 |
. . . . . . . 8
  
    |
256 | 249, 255 | syl5eqbrr 4437 |
. . . . . . 7

    |
257 | 18 | eluz1i 11166 |
. . . . . . 7
               |
258 | 21, 256, 257 | sylanbrc 670 |
. . . . . 6
         |
259 | | eluz2b1 11230 |
. . . . . . 7
               |
260 | 259 | simprbi 466 |
. . . . . 6
      
    |
261 | 258, 260 | syl 17 |
. . . . 5
     |
262 | 22, 261, 227, 85 | cxpled 23665 |
. . . 4
  π                π                     |
263 | 248, 262 | mpbid 214 |
. . 3
     π                    |
264 | 226, 263 | eqbrtrrd 4425 |
. 2
      π                    |
265 | 76, 81, 86, 224, 264 | letrd 9792 |
1
                        |