Step | Hyp | Ref
| Expression |
1 | | ostth3.5 |
. . . 4
                |
2 | | ostth.1 |
. . . . . . . . 9
   |
3 | | ostth3.3 |
. . . . . . . . . . . . 13
   |
4 | | prmuz2 14642 |
. . . . . . . . . . . . 13

      |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
       |
6 | | eluz2b2 11231 |
. . . . . . . . . . . 12
         |
7 | 5, 6 | sylib 200 |
. . . . . . . . . . 11
     |
8 | 7 | simpld 461 |
. . . . . . . . . 10
   |
9 | | nnq 11277 |
. . . . . . . . . 10
   |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
   |
11 | | qabsabv.a |
. . . . . . . . . 10
AbsVal   |
12 | | qrng.q |
. . . . . . . . . . 11
ℂfld ↾s   |
13 | 12 | qrngbas 24457 |
. . . . . . . . . 10
     |
14 | 11, 13 | abvcl 18052 |
. . . . . . . . 9
 
       |
15 | 2, 10, 14 | syl2anc 667 |
. . . . . . . 8
       |
16 | 8 | nnne0d 10654 |
. . . . . . . . 9
   |
17 | 12 | qrng0 24459 |
. . . . . . . . . 10
     |
18 | 11, 13, 17 | abvgt0 18056 |
. . . . . . . . 9
 
       |
19 | 2, 10, 16, 18 | syl3anc 1268 |
. . . . . . . 8
       |
20 | 15, 19 | elrpd 11338 |
. . . . . . 7
       |
21 | 20 | relogcld 23572 |
. . . . . 6
           |
22 | 8 | nnred 10624 |
. . . . . . 7
   |
23 | 7 | simprd 465 |
. . . . . . 7
   |
24 | 22, 23 | rplogcld 23578 |
. . . . . 6
       |
25 | 21, 24 | rerpdivcld 11369 |
. . . . 5
                 |
26 | 25 | renegcld 10046 |
. . . 4
                  |
27 | 1, 26 | syl5eqel 2533 |
. . 3
   |
28 | | ostth3.4 |
. . . . . . . . 9
    
  |
29 | | 1rp 11306 |
. . . . . . . . . 10
 |
30 | | logltb 23549 |
. . . . . . . . . 10
           
               |
31 | 20, 29, 30 | sylancl 668 |
. . . . . . . . 9
                     |
32 | 28, 31 | mpbid 214 |
. . . . . . . 8
        
      |
33 | | log1 23535 |
. . . . . . . 8
     |
34 | 32, 33 | syl6breq 4442 |
. . . . . . 7
        
  |
35 | 24 | rpcnd 11343 |
. . . . . . . 8
       |
36 | 35 | mul01d 9832 |
. . . . . . 7
         |
37 | 34, 36 | breqtrrd 4429 |
. . . . . 6
        
        |
38 | | 0red 9644 |
. . . . . . 7
   |
39 | 21, 38, 24 | ltdivmuld 11389 |
. . . . . 6
               
                 |
40 | 37, 39 | mpbird 236 |
. . . . 5
                 |
41 | 25 | lt0neg1d 10183 |
. . . . 5
               
                  |
42 | 40, 41 | mpbid 214 |
. . . 4
                  |
43 | 42, 1 | syl6breqr 4443 |
. . 3
   |
44 | 27, 43 | elrpd 11338 |
. 2
   |
45 | | padic.j |
. . . . 5
 
        
      |
46 | 12, 11, 45 | padicabvcxp 24470 |
. . . 4
                  |
47 | 3, 44, 46 | syl2anc 667 |
. . 3
                |
48 | | fveq2 5865 |
. . . . . . . . . 10
                   |
49 | 48 | oveq1d 6305 |
. . . . . . . . 9
                     
   |
50 | | eqid 2451 |
. . . . . . . . 9
          
            
   |
51 | | ovex 6318 |
. . . . . . . . 9
         
  |
52 | 49, 50, 51 | fvmpt 5948 |
. . . . . . . 8
                               |
53 | 10, 52 | syl 17 |
. . . . . . 7
                               |
54 | 45 | padicval 24455 |
. . . . . . . . . 10
                         |
55 | 3, 10, 54 | syl2anc 667 |
. . . . . . . . 9
                       |
56 | 16 | neneqd 2629 |
. . . . . . . . . 10
   |
57 | 56 | iffalsed 3892 |
. . . . . . . . 9
                      |
58 | 8 | nncnd 10625 |
. . . . . . . . . . . . . . 15
   |
59 | 58 | exp1d 12411 |
. . . . . . . . . . . . . 14
       |
60 | 59 | oveq2d 6306 |
. . . . . . . . . . . . 13
           |
61 | | 1z 10967 |
. . . . . . . . . . . . . 14
 |
62 | | pcid 14822 |
. . . . . . . . . . . . . 14
           |
63 | 3, 61, 62 | sylancl 668 |
. . . . . . . . . . . . 13
         |
64 | 60, 63 | eqtr3d 2487 |
. . . . . . . . . . . 12
     |
65 | 64 | negeqd 9869 |
. . . . . . . . . . 11
       |
66 | 65 | oveq2d 6306 |
. . . . . . . . . 10
               |
67 | | neg1z 10973 |
. . . . . . . . . . . 12
  |
68 | 67 | a1i 11 |
. . . . . . . . . . 11
    |
69 | 58, 16, 68 | cxpexpzd 23656 |
. . . . . . . . . 10
            |
70 | 66, 69 | eqtr4d 2488 |
. . . . . . . . 9
              |
71 | 55, 57, 70 | 3eqtrd 2489 |
. . . . . . . 8
               |
72 | 71 | oveq1d 6305 |
. . . . . . 7
                     |
73 | 27 | recnd 9669 |
. . . . . . . . . . 11
   |
74 | 73 | mulm1d 10070 |
. . . . . . . . . 10
       |
75 | 1 | negeqi 9868 |
. . . . . . . . . . 11
                  |
76 | 25 | recnd 9669 |
. . . . . . . . . . . 12
                 |
77 | 76 | negnegd 9977 |
. . . . . . . . . . 11
                                 |
78 | 75, 77 | syl5eq 2497 |
. . . . . . . . . 10
                  |
79 | 74, 78 | eqtrd 2485 |
. . . . . . . . 9
                    |
80 | 79 | oveq2d 6306 |
. . . . . . . 8
                          |
81 | 8 | nnrpd 11339 |
. . . . . . . . 9
   |
82 | | neg1rr 10714 |
. . . . . . . . . 10
  |
83 | 82 | a1i 11 |
. . . . . . . . 9
    |
84 | 81, 83, 73 | cxpmuld 23679 |
. . . . . . . 8
                |
85 | 58, 16, 76 | cxpefd 23657 |
. . . . . . . . 9
                                            |
86 | 21 | recnd 9669 |
. . . . . . . . . . 11
           |
87 | 24 | rpne0d 11346 |
. . . . . . . . . . 11
       |
88 | 86, 35, 87 | divcan1d 10384 |
. . . . . . . . . 10
                               |
89 | 88 | fveq2d 5869 |
. . . . . . . . 9
                                       |
90 | 20 | reeflogd 23573 |
. . . . . . . . 9
                   |
91 | 85, 89, 90 | 3eqtrd 2489 |
. . . . . . . 8
                        |
92 | 80, 84, 91 | 3eqtr3d 2493 |
. . . . . . 7
              |
93 | 53, 72, 92 | 3eqtrrd 2490 |
. . . . . 6
                        |
94 | | fveq2 5865 |
. . . . . . 7
           |
95 | | fveq2 5865 |
. . . . . . 7
                                     |
96 | 94, 95 | eqeq12d 2466 |
. . . . . 6
                                               |
97 | 93, 96 | syl5ibcom 224 |
. . . . 5
                          |
98 | 97 | adantr 467 |
. . . 4
 


                        |
99 | | prmnn 14625 |
. . . . . . . . 9

  |
100 | 99 | ad2antlr 733 |
. . . . . . . 8
       |
101 | | nnq 11277 |
. . . . . . . 8
   |
102 | 100, 101 | syl 17 |
. . . . . . 7
       |
103 | | fveq2 5865 |
. . . . . . . . 9
                   |
104 | 103 | oveq1d 6305 |
. . . . . . . 8
                     
   |
105 | | ovex 6318 |
. . . . . . . 8
         
  |
106 | 104, 50, 105 | fvmpt 5948 |
. . . . . . 7
                               |
107 | 102, 106 | syl 17 |
. . . . . 6
                                   |
108 | 73 | ad2antrr 732 |
. . . . . . . 8
       |
109 | 108 | 1cxpd 23652 |
. . . . . . 7
          |
110 | 3 | ad2antrr 732 |
. . . . . . . . . 10
       |
111 | 45 | padicval 24455 |
. . . . . . . . . 10
                         |
112 | 110, 102,
111 | syl2anc 667 |
. . . . . . . . 9
                           |
113 | 100 | nnne0d 10654 |
. . . . . . . . . . 11
       |
114 | 113 | neneqd 2629 |
. . . . . . . . . 10
    
  |
115 | 114 | iffalsed 3892 |
. . . . . . . . 9
      
                   |
116 | | pceq0 14820 |
. . . . . . . . . . . . . . . 16
         |
117 | 3, 99, 116 | syl2an 480 |
. . . . . . . . . . . . . . 15
 

  
   |
118 | | dvdsprm 14647 |
. . . . . . . . . . . . . . . . 17
       
   |
119 | 5, 118 | sylan 474 |
. . . . . . . . . . . . . . . 16
 


   |
120 | 119 | necon3bbid 2661 |
. . . . . . . . . . . . . . 15
 


   |
121 | 117, 120 | bitrd 257 |
. . . . . . . . . . . . . 14
 

  
   |
122 | 121 | biimpar 488 |
. . . . . . . . . . . . 13
         |
123 | 122 | negeqd 9869 |
. . . . . . . . . . . 12
           |
124 | | neg0 9920 |
. . . . . . . . . . . 12
  |
125 | 123, 124 | syl6eq 2501 |
. . . . . . . . . . 11
          |
126 | 125 | oveq2d 6306 |
. . . . . . . . . 10
                  |
127 | 58 | ad2antrr 732 |
. . . . . . . . . . 11
       |
128 | 127 | exp0d 12410 |
. . . . . . . . . 10
           |
129 | 126, 128 | eqtrd 2485 |
. . . . . . . . 9
              |
130 | 112, 115,
129 | 3eqtrd 2489 |
. . . . . . . 8
               |
131 | 130 | oveq1d 6305 |
. . . . . . 7
                     |
132 | | 2re 10679 |
. . . . . . . . . . . . 13
 |
133 | 132 | a1i 11 |
. . . . . . . . . . . 12
             |
134 | | ostth3.6 |
. . . . . . . . . . . . . 14
                      |
135 | 2 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
       |
136 | 11, 13 | abvcl 18052 |
. . . . . . . . . . . . . . . . . 18
 
       |
137 | 135, 102,
136 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
           |
138 | 11, 13, 17 | abvgt0 18056 |
. . . . . . . . . . . . . . . . . 18
 
       |
139 | 135, 102,
113, 138 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
           |
140 | 137, 139 | elrpd 11338 |
. . . . . . . . . . . . . . . 16
           |
141 | 140 | adantrr 723 |
. . . . . . . . . . . . . . 15
                 |
142 | 20 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                 |
143 | 141, 142 | ifcld 3924 |
. . . . . . . . . . . . . 14
                                  |
144 | 134, 143 | syl5eqel 2533 |
. . . . . . . . . . . . 13
          
  |
145 | 144 | rprecred 11352 |
. . . . . . . . . . . 12
               |
146 | | simprr 766 |
. . . . . . . . . . . . . . 15
              
  |
147 | 28 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
              
  |
148 | | breq1 4405 |
. . . . . . . . . . . . . . . 16
                                                       |
149 | | breq1 4405 |
. . . . . . . . . . . . . . . 16
                                                       |
150 | 148, 149 | ifboth 3917 |
. . . . . . . . . . . . . . 15
     
                            |
151 | 146, 147,
150 | syl2anc 667 |
. . . . . . . . . . . . . 14
                                  |
152 | 134, 151 | syl5eqbr 4436 |
. . . . . . . . . . . . 13
             |
153 | 144 | reclt1d 11354 |
. . . . . . . . . . . . 13
                 |
154 | 152, 153 | mpbid 214 |
. . . . . . . . . . . 12
          
    |
155 | | expnbnd 12401 |
. . . . . . . . . . . 12
       
        |
156 | 133, 145,
154, 155 | syl3anc 1268 |
. . . . . . . . . . 11
           
        |
157 | 144 | rpcnd 11343 |
. . . . . . . . . . . . . . . . 17
          
  |
158 | 157 | adantr 467 |
. . . . . . . . . . . . . . . 16
   
 
   
     |
159 | 144 | rpne0d 11346 |
. . . . . . . . . . . . . . . . 17
             |
160 | 159 | adantr 467 |
. . . . . . . . . . . . . . . 16
   
 
   
     |
161 | | nnz 10959 |
. . . . . . . . . . . . . . . . 17
   |
162 | 161 | adantl 468 |
. . . . . . . . . . . . . . . 16
   
 
   
     |
163 | 158, 160,
162 | exprecd 12424 |
. . . . . . . . . . . . . . 15
   
 
   
                 |
164 | 2 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . 18
   
 
   
     |
165 | | ax-1ne0 9608 |
. . . . . . . . . . . . . . . . . 18
 |
166 | 12 | qrng1 24460 |
. . . . . . . . . . . . . . . . . . 19
     |
167 | 11, 166, 17 | abv1z 18060 |
. . . . . . . . . . . . . . . . . 18
         |
168 | 164, 165,
167 | sylancl 668 |
. . . . . . . . . . . . . . . . 17
   
 
   
         |
169 | 8 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . 21
          
  |
170 | | nnnn0 10876 |
. . . . . . . . . . . . . . . . . . . . 21
   |
171 | | nnexpcl 12285 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
172 | 169, 170,
171 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . 20
   
 
   
         |
173 | 172 | nnzd 11039 |
. . . . . . . . . . . . . . . . . . 19
   
 
   
         |
174 | 99 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . 21
          
  |
175 | | nnexpcl 12285 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
176 | 174, 170,
175 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . 20
   
 
   
         |
177 | 176 | nnzd 11039 |
. . . . . . . . . . . . . . . . . . 19
   
 
   
         |
178 | | bezout 14510 |
. . . . . . . . . . . . . . . . . . 19
                 
                     |
179 | 173, 177,
178 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
   
 
   
                               |
180 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
181 | 3 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          
  |
182 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          
  |
183 | | prmrp 14658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
184 | 181, 182,
183 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
185 | 180, 184 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
186 | 185 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
       |
187 | 169 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
     |
188 | 174 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
     |
189 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
     |
190 | | rppwr 14525 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                 |
191 | 187, 188,
189, 190 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
                   |
192 | 186, 191 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
   
       
       |
193 | 192 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
   
 
   
   
       
       |
194 | 193 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
   
   
                           
                 |
195 | 2 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
   
     |
196 | 172 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
         |
197 | | nnq 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
         |
199 | | simprrl 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
     |
200 | | zq 11270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
     |
202 | | qmulcl 11282 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
         |
203 | 198, 201,
202 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
   
           |
204 | 176 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
         |
205 | | nnq 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
         |
207 | | simprrr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
     |
208 | | zq 11270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
209 | 207, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
     |
210 | | qmulcl 11282 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
         |
211 | 206, 209,
210 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
   
           |
212 | | qaddcl 11280 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                               |
213 | 203, 211,
212 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
   
                   |
214 | 11, 13 | abvcl 18052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                     |
215 | 195, 213,
214 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
   
   
                       |
216 | 11, 13 | abvcl 18052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     |
217 | 195, 203,
216 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
   
               |
218 | 11, 13 | abvcl 18052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     |
219 | 195, 211,
218 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
   
               |
220 | 217, 219 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
   
   
                           |
221 | | rpexpcl 12291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
222 | 144, 161,
221 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
         |
223 | 222 | rpred 11341 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
         |
224 | 223 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
   
         |
225 | | remulcl 9624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
226 | 132, 224,
225 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
   
   
           |
227 | | qex 11276 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
228 | | cnfldadd 18975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 ℂfld |
229 | 12, 228 | ressplusg 15239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      |
230 | 227, 229 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    |
231 | 11, 13, 230 | abvtri 18058 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                         |
232 | 195, 203,
211, 231 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
   
   
                                             |
233 | | cnfldmul 18976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  ℂfld |
234 | 12, 233 | ressmulr 15250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
235 | 227, 234 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
236 | 11, 13, 235 | abvmul 18057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                 |
237 | 195, 198,
201, 236 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                             |
238 | 10 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
     |
239 | 170 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
     |
240 | 12, 11 | qabvexp 24464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
                   |
241 | 195, 238,
239, 240 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
                     |
242 | 241 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                                 |
243 | 237, 242 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
                             |
244 | 195, 238,
14 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
         |
245 | 244, 239 | reexpcld 12433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
             |
246 | 11, 13 | abvcl 18052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
247 | 195, 201,
246 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
         |
248 | 245, 247 | remulcld 9671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                   |
249 | | elz 10939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

       |
250 | 249 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      |
251 | 250 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 

     |
252 | 11, 17 | abv0 18059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
253 | 2, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       |
254 | | 0le1 10137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 |
255 | 253, 254 | syl6eqbr 4440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
  |
256 | 255 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

      |
257 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           |
258 | 257 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
       |
259 | 256, 258 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 

        |
260 | | ostth3.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
      |
261 | | nnq 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   |
262 | 11, 13 | abvcl 18052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
       |
263 | 2, 261, 262 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 

      |
264 | | 1re 9642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 |
265 | | lenlt 9712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
             |
266 | 263, 264,
265 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 

    
       |
267 | 266 | ralbidva 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
               |
268 | 260, 267 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
        |
269 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
           |
270 | 269 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     
       |
271 | 270 | rspccv 3147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
   

       |
272 | 268, 271 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
   |
273 | 272 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 

        |
274 | 2 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   
  |
275 | 200 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
      |
276 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
           |
277 | 11, 13, 276 | abvneg 18062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
                    |
278 | 274, 275,
277 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
                       |
279 | 12 | qrngneg 24461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
             |
280 | 275, 279 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
                |
281 | | simprr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
       |
282 | 280, 281 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
               |
283 | 268 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
    
      |
284 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                             |
285 | 284 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                           
   |
286 | 285 | rspcv 3146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                                |
287 | 282, 283,
286 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
                   |
288 | 278, 287 | eqbrtrrd 4425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
       
  |
289 | 288 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 

 
       |
290 | 259, 273,
289 | 3jaod 1332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 

           |
291 | 251, 290 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 

      |
292 | 291 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        |
293 | 292 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
   
          |
294 | | rsp 2754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   

       |
295 | 293, 199,
294 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
         |
296 | 264 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
   
     |
297 | 161 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 
   
   
     |
298 | 19 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 
   
   
         |
299 | | expgt0 12305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
               |
300 | 244, 297,
298, 299 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
   
             |
301 | | lemul2 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                                   |
302 | 247, 296,
245, 300, 301 | syl112anc 1272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
       
                           |
303 | 295, 302 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
                             |
304 | 245 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
             |
305 | 304 | mulid1d 9660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
                       |
306 | 303, 305 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                           |
307 | 144 | rpred 11341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
  |
308 | 307 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
     |
309 | 142 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
         |
310 | 309 | rpge0d 11345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
         |
311 | 174 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 
   
   
     |
312 | 311, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 
   
   
     |
313 | 195, 312,
136 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
   
         |
314 | | max1 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              
     
                 |
315 | 244, 313,
314 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
                              |
316 | 315, 134 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
         |
317 | | leexp1a 12331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
         
 
              |
318 | 244, 308,
239, 310, 316, 317 | syl32anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                 |
319 | 248, 245,
224, 306, 318 | letrd 9792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
                       |
320 | 243, 319 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
   
                   |
321 | 11, 13, 235 | abvmul 18057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                           |
322 | 195, 206,
209, 321 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                             |
323 | 12, 11 | qabvexp 24464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
                   |
324 | 195, 312,
239, 323 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
                     |
325 | 324 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                                 |
326 | 322, 325 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
                             |
327 | 313, 239 | reexpcld 12433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
             |
328 | 11, 13 | abvcl 18052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
329 | 195, 209,
328 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
         |
330 | 327, 329 | remulcld 9671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                   |
331 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
332 | 331 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
       |
333 | 332 | rspcv 3146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  
           |
334 | 207, 293,
333 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
         |
335 | 311 | nnne0d 10654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 
   
   
     |
336 | 195, 312,
335, 138 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
 
   
   
         |
337 | | expgt0 12305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
               |
338 | 313, 297,
336, 337 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
   
             |
339 | | lemul2 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                                   |
340 | 329, 296,
327, 338, 339 | syl112anc 1272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
       
                           |
341 | 334, 340 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
                             |
342 | 327 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
             |
343 | 342 | mulid1d 9660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
                       |
344 | 341, 343 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                           |
345 | 141 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
         |
346 | 345 | rpge0d 11345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
         |
347 | | max2 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              
     
                 |
348 | 244, 313,
347 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
   
                              |
349 | 348, 134 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 
   
   
         |
350 | | leexp1a 12331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
         
 
              |
351 | 313, 308,
239, 346, 349, 350 | syl32anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 
   
   
                 |
352 | 330, 327,
224, 344, 351 | letrd 9792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
   
                       |
353 | 326, 352 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
   
                   |
354 | 217, 219,
224, 224, 320, 353 | le2addd 10232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
   
                                     |
355 | 222 | rpcnd 11343 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
   
         |
356 | 355 | 2timesd 10855 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
   
                     |
357 | 356 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
   
   
                     |
358 | 354, 357 | breqtrrd 4429 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
   
   
                                 |
359 | 215, 220,
226, 232, 358 | letrd 9792 |
. . . . . . . . . . . . . . . . . . . . . 22
   
 
   
   
                             |
360 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                       |
361 | 360 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
     
                           |
362 | 359, 361 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
   
   
                     
         |
363 | 194, 362 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . 20
   
 
   
   
                               
         |
364 | 363 | anassrs 654 |
. . . . . . . . . . . . . . . . . . 19
          
   
 
     
                                |
365 | 364 | rexlimdvva 2886 |
. . . . . . . . . . . . . . . . . 18
   
 
   
    
     
                                |
366 | 179, 365 | mpd 15 |
. . . . . . . . . . . . . . . . 17
   
 
   
               |
367 | 168, 366 | eqbrtrrd 4425 |
. . . . . . . . . . . . . . . 16
   
 
   
           |
368 | 222 | rpregt0d 11347 |
. . . . . . . . . . . . . . . . 17
   
 
   
               |
369 | | ledivmul2 10484 |
. . . . . . . . . . . . . . . . . 18
 
                           |
370 | 264, 132,
369 | mp3an12 1354 |
. . . . . . . . . . . . . . . . 17
                           |
371 | 368, 370 | syl 17 |
. . . . . . . . . . . . . . . 16
   
 
   
         
         |
372 | 367, 371 | mpbird 236 |
. . . . . . . . . . . . . . 15
   
 
   
           |
373 | 163, 372 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
   
 
   
           |
374 | | reexpcl 12289 |
. . . . . . . . . . . . . . . 16
   
         |
375 | 145, 170,
374 | syl2an 480 |
. . . . . . . . . . . . . . 15
   
 
   
           |
376 | | lenlt 9712 |
. . . . . . . . . . . . . . 15
       
                 |
377 | 375, 132,
376 | sylancl 668 |
. . . . . . . . . . . . . 14
   
 
   
         
         |
378 | 373, 377 | mpbid 214 |
. . . . . . . . . . . . 13
   
 
   
           |
379 | 378 | pm2.21d 110 |
. . . . . . . . . . . 12
   
 
   
   
         
   |
380 | 379 | rexlimdva 2879 |
. . . . . . . . . . 11
                  
       |
381 | 156, 380 | mpd 15 |
. . . . . . . . . 10
              
  |
382 | 381 | expr 620 |
. . . . . . . . 9
         
   
   |
383 | 382 | pm2.01d 173 |
. . . . . . . 8
           |
384 | 260 | ad2antrr 732 |
. . . . . . . . 9
            |
385 | | fveq2 5865 |
. . . . . . . . . . . 12
           |
386 | 385 | breq2d 4414 |
. . . . . . . . . . 11
 
   
       |
387 | 386 | notbid 296 |
. . . . . . . . . 10
 
   
       |
388 | 387 | rspcv 3146 |
. . . . . . . . 9
  
   
       |
389 | 100, 384,
388 | sylc 62 |
. . . . . . . 8
           |
390 | | lttri3 9717 |
. . . . . . . . 9
     
                   |
391 | 137, 264,
390 | sylancl 668 |
. . . . . . . 8
              
        |
392 | 383, 389,
391 | mpbir2and 933 |
. . . . . . 7
           |
393 | 109, 131,
392 | 3eqtr4d 2495 |
. . . . . 6
                      |
394 | 107, 393 | eqtr2d 2486 |
. . . . 5
                    
       |
395 | 394 | ex 436 |
. . . 4
 


                        |
396 | 98, 395 | pm2.61dne 2710 |
. . 3
 

                       |
397 | 12, 11, 2, 47, 396 | ostthlem2 24466 |
. 2
           
    |
398 | | oveq2 6298 |
. . . . 5
                     
   |
399 | 398 | mpteq2dv 4490 |
. . . 4
                             |
400 | 399 | eqeq2d 2461 |
. . 3
 
                       
     |
401 | 400 | rspcev 3150 |
. 2
                                |
402 | 44, 397, 401 | syl2anc 667 |
1
                 |