Step | Hyp | Ref
| Expression |
1 | | oveq2 6303 |
. . . . . . . . 9
           |
2 | 1 | oveq1d 6310 |
. . . . . . . 8
               |
3 | 2 | oveq2d 6311 |
. . . . . . 7
                       |
4 | | oveq2 6303 |
. . . . . . . . 9
 
     |
5 | | oveq2 6303 |
. . . . . . . . 9
           |
6 | 4, 5 | oveq12d 6313 |
. . . . . . . 8
                   |
7 | 6 | breq2d 4417 |
. . . . . . 7
     
 
     
               |
8 | 3, 7 | raleqbidv 3003 |
. . . . . 6
  
                      
                           |
9 | 8 | imbi2d 318 |
. . . . 5
  
                                                      |
10 | | oveq2 6303 |
. . . . . . . . 9
           |
11 | 10 | oveq1d 6310 |
. . . . . . . 8
               |
12 | 11 | oveq2d 6311 |
. . . . . . 7
                       |
13 | | oveq2 6303 |
. . . . . . . . 9
 
     |
14 | | oveq2 6303 |
. . . . . . . . 9
           |
15 | 13, 14 | oveq12d 6313 |
. . . . . . . 8
                   |
16 | 15 | breq2d 4417 |
. . . . . . 7
     
 
     
               |
17 | 12, 16 | raleqbidv 3003 |
. . . . . 6
  
                      
                           |
18 | 17 | imbi2d 318 |
. . . . 5
  
                                                      |
19 | | oveq2 6303 |
. . . . . . . . 9
               |
20 | 19 | oveq1d 6310 |
. . . . . . . 8
                   |
21 | 20 | oveq2d 6311 |
. . . . . . 7
                           |
22 | | oveq2 6303 |
. . . . . . . . 9
   
  
    |
23 | | oveq2 6303 |
. . . . . . . . 9
               |
24 | 22, 23 | oveq12d 6313 |
. . . . . . . 8
                         |
25 | 24 | breq2d 4417 |
. . . . . . 7
       
 
     
                   |
26 | 21, 25 | raleqbidv 3003 |
. . . . . 6
    
                      
                                 |
27 | 26 | imbi2d 318 |
. . . . 5
    
                                                            |
28 | | oveq2 6303 |
. . . . . . . . 9
           |
29 | 28 | oveq1d 6310 |
. . . . . . . 8
               |
30 | 29 | oveq2d 6311 |
. . . . . . 7
                       |
31 | | oveq2 6303 |
. . . . . . . . 9
 
     |
32 | | oveq2 6303 |
. . . . . . . . 9
           |
33 | 31, 32 | oveq12d 6313 |
. . . . . . . 8
                   |
34 | 33 | breq2d 4417 |
. . . . . . 7
     
 
     
               |
35 | 30, 34 | raleqbidv 3003 |
. . . . . 6
  
                      
                           |
36 | 35 | imbi2d 318 |
. . . . 5
  
                                                      |
37 | | ostth2.5 |
. . . . . . . . . . . . . 14
       |
38 | | eluz2nn 11204 |
. . . . . . . . . . . . . 14
    
  |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
   |
40 | 39 | nncnd 10632 |
. . . . . . . . . . . 12
   |
41 | 40 | exp0d 12417 |
. . . . . . . . . . 11
       |
42 | 41 | oveq1d 6310 |
. . . . . . . . . 10
           |
43 | | 1m1e0 10685 |
. . . . . . . . . 10
   |
44 | 42, 43 | syl6eq 2503 |
. . . . . . . . 9
         |
45 | 44 | oveq2d 6311 |
. . . . . . . 8
                 |
46 | 45 | eleq2d 2516 |
. . . . . . 7
                   |
47 | | 0le0 10706 |
. . . . . . . . . 10
 |
48 | 47 | a1i 11 |
. . . . . . . . 9

  |
49 | | ostth.1 |
. . . . . . . . . 10
   |
50 | | qabsabv.a |
. . . . . . . . . . 11
AbsVal   |
51 | | qrng.q |
. . . . . . . . . . . 12
ℂfld ↾s   |
52 | 51 | qrng0 24471 |
. . . . . . . . . . 11
     |
53 | 50, 52 | abv0 18071 |
. . . . . . . . . 10
       |
54 | 49, 53 | syl 17 |
. . . . . . . . 9
       |
55 | 40 | mul01d 9837 |
. . . . . . . . . . 11
     |
56 | 55 | oveq1d 6310 |
. . . . . . . . . 10
                 |
57 | | ostth2.7 |
. . . . . . . . . . . . . 14
              |
58 | | 1re 9647 |
. . . . . . . . . . . . . . 15
 |
59 | | nnq 11284 |
. . . . . . . . . . . . . . . . 17
   |
60 | 39, 59 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
61 | 51 | qrngbas 24469 |
. . . . . . . . . . . . . . . . 17
     |
62 | 50, 61 | abvcl 18064 |
. . . . . . . . . . . . . . . 16
 
       |
63 | 49, 60, 62 | syl2anc 667 |
. . . . . . . . . . . . . . 15
       |
64 | | ifcl 3925 |
. . . . . . . . . . . . . . 15
                      |
65 | 58, 63, 64 | sylancr 670 |
. . . . . . . . . . . . . 14
                |
66 | 57, 65 | syl5eqel 2535 |
. . . . . . . . . . . . 13
   |
67 | 66 | recnd 9674 |
. . . . . . . . . . . 12
   |
68 | | 0nn0 10891 |
. . . . . . . . . . . 12
 |
69 | | expcl 12297 |
. . . . . . . . . . . 12
 
       |
70 | 67, 68, 69 | sylancl 669 |
. . . . . . . . . . 11
       |
71 | 70 | mul02d 9836 |
. . . . . . . . . 10
         |
72 | 56, 71 | eqtrd 2487 |
. . . . . . . . 9
           |
73 | 48, 54, 72 | 3brtr4d 4436 |
. . . . . . . 8
    
 
        |
74 | | elfz1eq 11817 |
. . . . . . . . . 10
       |
75 | 74 | fveq2d 5874 |
. . . . . . . . 9
               |
76 | 75 | breq1d 4415 |
. . . . . . . 8
         
 
     
               |
77 | 73, 76 | syl5ibrcom 226 |
. . . . . . 7
                     |
78 | 46, 77 | sylbid 219 |
. . . . . 6
                           |
79 | 78 | ralrimiv 2802 |
. . . . 5
                
 
        |
80 | | fveq2 5870 |
. . . . . . . . . 10
           |
81 | 80 | breq1d 4415 |
. . . . . . . . 9
     
 
     
               |
82 | 81 | cbvralv 3021 |
. . . . . . . 8
 
                      
                          |
83 | 49 | ad2antrr 733 |
. . . . . . . . . . . 12
                                             |
84 | | elfzelz 11807 |
. . . . . . . . . . . . . 14
               |
85 | 84 | ad2antrl 735 |
. . . . . . . . . . . . 13
                                             |
86 | | zq 11277 |
. . . . . . . . . . . . 13
   |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . 12
                                             |
88 | 50, 61 | abvcl 18064 |
. . . . . . . . . . . 12
 
       |
89 | 83, 87, 88 | syl2anc 667 |
. . . . . . . . . . 11
                                                 |
90 | 39 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
                                             |
91 | | simplr 763 |
. . . . . . . . . . . . . . . . 17
                                             |
92 | 90, 91 | nnexpcld 12444 |
. . . . . . . . . . . . . . . 16
                                                 |
93 | 85, 92 | zmodcld 12124 |
. . . . . . . . . . . . . . 15
                                                   |
94 | 93 | nn0zd 11045 |
. . . . . . . . . . . . . 14
                                                   |
95 | | zq 11277 |
. . . . . . . . . . . . . 14
       
       |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . 13
                                                   |
97 | 50, 61 | abvcl 18064 |
. . . . . . . . . . . . 13
            
        |
98 | 83, 96, 97 | syl2anc 667 |
. . . . . . . . . . . 12
                                                       |
99 | 90, 59 | syl 17 |
. . . . . . . . . . . . . . 15
                                             |
100 | 83, 99, 62 | syl2anc 667 |
. . . . . . . . . . . . . 14
                                                 |
101 | 100, 91 | reexpcld 12440 |
. . . . . . . . . . . . 13
                                                     |
102 | 85 | zred 11047 |
. . . . . . . . . . . . . . . . 17
                                             |
103 | 102, 92 | nndivred 10665 |
. . . . . . . . . . . . . . . 16
                                                   |
104 | 103 | flcld 12041 |
. . . . . . . . . . . . . . 15
                                                       |
105 | | zq 11277 |
. . . . . . . . . . . . . . 15
                       |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
                                                       |
107 | 50, 61 | abvcl 18064 |
. . . . . . . . . . . . . 14
                             |
108 | 83, 106, 107 | syl2anc 667 |
. . . . . . . . . . . . 13
                                                           |
109 | 101, 108 | remulcld 9676 |
. . . . . . . . . . . 12
                                                                     |
110 | 98, 109 | readdcld 9675 |
. . . . . . . . . . 11
                                                                                 |
111 | 90 | nnred 10631 |
. . . . . . . . . . . . 13
                                             |
112 | | nn0p1nn 10916 |
. . . . . . . . . . . . . . 15

    |
113 | 112 | ad2antlr 734 |
. . . . . . . . . . . . . 14
                                               |
114 | 113 | nnred 10631 |
. . . . . . . . . . . . 13
                                               |
115 | 111, 114 | remulcld 9676 |
. . . . . . . . . . . 12
                                            
    |
116 | 66 | ad2antrr 733 |
. . . . . . . . . . . . 13
                                             |
117 | | peano2nn0 10917 |
. . . . . . . . . . . . . 14

    |
118 | 117 | ad2antlr 734 |
. . . . . . . . . . . . 13
                                               |
119 | 116, 118 | reexpcld 12440 |
. . . . . . . . . . . 12
                                                   |
120 | 115, 119 | remulcld 9676 |
. . . . . . . . . . 11
                                                         |
121 | | nnq 11284 |
. . . . . . . . . . . . . . 15
           |
122 | 92, 121 | syl 17 |
. . . . . . . . . . . . . 14
                                                 |
123 | | qmulcl 11289 |
. . . . . . . . . . . . . 14
                                   |
124 | 122, 106,
123 | syl2anc 667 |
. . . . . . . . . . . . 13
                                                             |
125 | | qex 11283 |
. . . . . . . . . . . . . . 15
 |
126 | | cnfldadd 18987 |
. . . . . . . . . . . . . . . 16
 ℂfld |
127 | 51, 126 | ressplusg 15251 |
. . . . . . . . . . . . . . 15
      |
128 | 125, 127 | ax-mp 5 |
. . . . . . . . . . . . . 14
    |
129 | 50, 61, 128 | abvtri 18070 |
. . . . . . . . . . . . 13
                                                                                       |
130 | 83, 96, 124, 129 | syl3anc 1269 |
. . . . . . . . . . . 12
                                                                           
                             |
131 | 92 | nnrpd 11346 |
. . . . . . . . . . . . . . . 16
                                                 |
132 | | modval 12105 |
. . . . . . . . . . . . . . . 16
       
                         |
133 | 102, 131,
132 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                                                                     |
134 | 133 | oveq1d 6310 |
. . . . . . . . . . . . . 14
                                                                                                         |
135 | 102 | recnd 9674 |
. . . . . . . . . . . . . . 15
                                             |
136 | | qcn 11285 |
. . . . . . . . . . . . . . . 16
                                   |
137 | 124, 136 | syl 17 |
. . . . . . . . . . . . . . 15
                                                             |
138 | 135, 137 | npcand 9995 |
. . . . . . . . . . . . . 14
                                                                                 |
139 | 134, 138 | eqtrd 2487 |
. . . . . . . . . . . . 13
                                                                     |
140 | 139 | fveq2d 5874 |
. . . . . . . . . . . 12
                                                                             |
141 | | cnfldmul 18988 |
. . . . . . . . . . . . . . . . . 18
  ℂfld |
142 | 51, 141 | ressmulr 15262 |
. . . . . . . . . . . . . . . . 17
       |
143 | 125, 142 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     |
144 | 50, 61, 143 | abvmul 18069 |
. . . . . . . . . . . . . . 15
                                                               |
145 | 83, 122, 106, 144 | syl3anc 1269 |
. . . . . . . . . . . . . 14
                                                                                         |
146 | 51, 50 | qabvexp 24476 |
. . . . . . . . . . . . . . . 16
 
                   |
147 | 83, 99, 91, 146 | syl3anc 1269 |
. . . . . . . . . . . . . . 15
                                                             |
148 | 147 | oveq1d 6310 |
. . . . . . . . . . . . . 14
                                                                                             |
149 | 145, 148 | eqtrd 2487 |
. . . . . . . . . . . . 13
                                                                                         |
150 | 149 | oveq2d 6311 |
. . . . . . . . . . . 12
                                                                               
                                 |
151 | 130, 140,
150 | 3brtr3d 4435 |
. . . . . . . . . . 11
                                                   
                                 |
152 | 116, 91 | reexpcld 12440 |
. . . . . . . . . . . . 13
                                                 |
153 | 115, 152 | remulcld 9676 |
. . . . . . . . . . . 12
                                                       |
154 | | nn0re 10885 |
. . . . . . . . . . . . . . . . 17

  |
155 | 154 | ad2antlr 734 |
. . . . . . . . . . . . . . . 16
                                             |
156 | 111, 155 | remulcld 9676 |
. . . . . . . . . . . . . . 15
                                               |
157 | 156, 152 | remulcld 9676 |
. . . . . . . . . . . . . 14
                                                     |
158 | 111, 152 | remulcld 9676 |
. . . . . . . . . . . . . 14
                                                   |
159 | | zmodfz 12125 |
. . . . . . . . . . . . . . . 16
                         |
160 | 85, 92, 159 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                                                             |
161 | | simprr 767 |
. . . . . . . . . . . . . . 15
                                                          
 
        |
162 | | fveq2 5870 |
. . . . . . . . . . . . . . . . 17
                       |
163 | 162 | breq1d 4415 |
. . . . . . . . . . . . . . . 16
           
 
     
         
 
         |
164 | 163 | rspcv 3148 |
. . . . . . . . . . . . . . 15
                  
                                            |
165 | 160, 161,
164 | sylc 62 |
. . . . . . . . . . . . . 14
                                                    
 
        |
166 | 111, 101 | remulcld 9676 |
. . . . . . . . . . . . . . 15
                                                       |
167 | 101 | recnd 9674 |
. . . . . . . . . . . . . . . . 17
                                                     |
168 | 108 | recnd 9674 |
. . . . . . . . . . . . . . . . 17
                                                           |
169 | 167, 168 | mulcomd 9669 |
. . . . . . . . . . . . . . . 16
                                                                                             |
170 | 50, 61 | abvge0 18065 |
. . . . . . . . . . . . . . . . . . 19
 

      |
171 | 83, 99, 170 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                                                 |
172 | 100, 91, 171 | expge0d 12441 |
. . . . . . . . . . . . . . . . 17
                                                     |
173 | 104 | zred 11047 |
. . . . . . . . . . . . . . . . . 18
                                                       |
174 | | elfzle1 11809 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
175 | 174 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . . . . 21
                                             |
176 | 92 | nnred 10631 |
. . . . . . . . . . . . . . . . . . . . 21
                                                 |
177 | 92 | nngt0d 10660 |
. . . . . . . . . . . . . . . . . . . . 21
                                                 |
178 | | divge0 10481 |
. . . . . . . . . . . . . . . . . . . . 21
  
           
        |
179 | 102, 175,
176, 177, 178 | syl22anc 1270 |
. . . . . . . . . . . . . . . . . . . 20
                                                   |
180 | | flge0nn0 12061 |
. . . . . . . . . . . . . . . . . . . 20
              
            |
181 | 103, 179,
180 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
                                                       |
182 | 51, 50 | qabvle 24475 |
. . . . . . . . . . . . . . . . . . 19
                                       |
183 | 83, 181, 182 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                                                        
            |
184 | | simprl 765 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                         |
185 | | 0z 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
186 | 90, 118 | nnexpcld 12444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                   |
187 | 186 | nnzd 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                   |
188 | | elfzm11 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      
          |
189 | 185, 187,
188 | sylancr 670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                        
          |
190 | 184, 189 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                           
         |
191 | 190 | simp3d 1023 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                   |
192 | 90 | nncnd 10632 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                             |
193 | 192, 91 | expp1d 12424 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                         |
194 | 191, 193 | breqtrd 4430 |
. . . . . . . . . . . . . . . . . . . . 21
                                                   |
195 | | ltdivmul 10487 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                           |
196 | 102, 111,
176, 177, 195 | syl112anc 1273 |
. . . . . . . . . . . . . . . . . . . . 21
                                                           |
197 | 194, 196 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . 20
                                                   |
198 | 90 | nnzd 11046 |
. . . . . . . . . . . . . . . . . . . . 21
                                             |
199 | | fllt 12049 |
. . . . . . . . . . . . . . . . . . . . 21
               
             |
200 | 103, 198,
199 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
                                                               |
201 | 197, 200 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
                                                       |
202 | 173, 111,
201 | ltled 9788 |
. . . . . . . . . . . . . . . . . 18
                                                    
  |
203 | 108, 173,
111, 183, 202 | letrd 9797 |
. . . . . . . . . . . . . . . . 17
                                                        
  |
204 | 108, 111,
101, 172, 203 | lemul1ad 10553 |
. . . . . . . . . . . . . . . 16
                                                                  
            |
205 | 169, 204 | eqbrtrd 4426 |
. . . . . . . . . . . . . . 15
                                                                  
            |
206 | 90 | nnnn0d 10932 |
. . . . . . . . . . . . . . . . 17
                                             |
207 | 206 | nn0ge0d 10935 |
. . . . . . . . . . . . . . . 16
                                             |
208 | | max1 11487 |
. . . . . . . . . . . . . . . . . . 19
     
    
     
         |
209 | 100, 58, 208 | sylancl 669 |
. . . . . . . . . . . . . . . . . 18
                                                              |
210 | 209, 57 | syl6breqr 4446 |
. . . . . . . . . . . . . . . . 17
                                                 |
211 | | leexp1a 12338 |
. . . . . . . . . . . . . . . . 17
      
         
 
              |
212 | 100, 116,
91, 171, 210, 211 | syl32anc 1277 |
. . . . . . . . . . . . . . . 16
                                                         |
213 | 101, 152,
111, 207, 212 | lemul2ad 10554 |
. . . . . . . . . . . . . . 15
                                                     
       |
214 | 109, 166,
158, 205, 213 | letrd 9797 |
. . . . . . . . . . . . . 14
                                                                  
        |
215 | 98, 109, 157, 158, 165, 214 | le2addd 10239 |
. . . . . . . . . . . . 13
                                                                                                 |
216 | | nn0cn 10886 |
. . . . . . . . . . . . . . . . . 18

  |
217 | 216 | ad2antlr 734 |
. . . . . . . . . . . . . . . . 17
                                             |
218 | | 1cnd 9664 |
. . . . . . . . . . . . . . . . 17
                                             |
219 | 192, 217,
218 | adddid 9672 |
. . . . . . . . . . . . . . . 16
                                            
          |
220 | 192 | mulid1d 9665 |
. . . . . . . . . . . . . . . . 17
                                               |
221 | 220 | oveq2d 6311 |
. . . . . . . . . . . . . . . 16
                                                       |
222 | 219, 221 | eqtrd 2487 |
. . . . . . . . . . . . . . 15
                                            
        |
223 | 222 | oveq1d 6310 |
. . . . . . . . . . . . . 14
                                                                 |
224 | 192, 217 | mulcld 9668 |
. . . . . . . . . . . . . . 15
                                               |
225 | 152 | recnd 9674 |
. . . . . . . . . . . . . . 15
                                                 |
226 | 224, 192,
225 | adddird 9673 |
. . . . . . . . . . . . . 14
                                                                       |
227 | 223, 226 | eqtrd 2487 |
. . . . . . . . . . . . 13
                                                                       |
228 | 215, 227 | breqtrrd 4432 |
. . . . . . . . . . . 12
                                                                                           |
229 | | max2 11489 |
. . . . . . . . . . . . . . . 16
     

     
         |
230 | 100, 58, 229 | sylancl 669 |
. . . . . . . . . . . . . . 15
                                                          |
231 | 230, 57 | syl6breqr 4446 |
. . . . . . . . . . . . . 14
                                             |
232 | | nn0z 10967 |
. . . . . . . . . . . . . . . . 17

  |
233 | 232 | ad2antlr 734 |
. . . . . . . . . . . . . . . 16
                                             |
234 | | uzid 11180 |
. . . . . . . . . . . . . . . 16
       |
235 | 233, 234 | syl 17 |
. . . . . . . . . . . . . . 15
                                                 |
236 | | peano2uz 11219 |
. . . . . . . . . . . . . . 15
    
        |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . 14
                                                   |
238 | 116, 231,
237 | leexp2ad 12455 |
. . . . . . . . . . . . 13
                                                       |
239 | 90, 113 | nnmulcld 10664 |
. . . . . . . . . . . . . . 15
                                            
    |
240 | 239 | nngt0d 10660 |
. . . . . . . . . . . . . 14
                                           
     |
241 | | lemul2 10465 |
. . . . . . . . . . . . . 14
                  
                                        |
242 | 152, 119,
115, 240, 241 | syl112anc 1273 |
. . . . . . . . . . . . 13
                                                                               |
243 | 238, 242 | mpbid 214 |
. . . . . . . . . . . 12
                                                                   |
244 | 110, 153,
120, 228, 243 | letrd 9797 |
. . . . . . . . . . 11
                                                                                             |
245 | 89, 110, 120, 151, 244 | letrd 9797 |
. . . . . . . . . 10
                                                             |
246 | 245 | expr 620 |
. . . . . . . . 9
                  
                             
            |
247 | 246 | ralrimdva 2808 |
. . . . . . . 8
 

 
                                                        |
248 | 82, 247 | syl5bi 221 |
. . . . . . 7
 

 
                                                        |
249 | 248 | expcom 437 |
. . . . . 6

                                           
 
              |
250 | 249 | a2d 29 |
. . . . 5

                 
 
       
                                  |
251 | 9, 18, 27, 36, 79, 250 | nn0ind 11037 |
. . . 4

                
 
         |
252 | 251 | impcom 432 |
. . 3
 

                          |
253 | | fveq2 5870 |
. . . . 5
           |
254 | 253 | breq1d 4415 |
. . . 4
     
 
     
               |
255 | 254 | rspccv 3149 |
. . 3
 
                       
             
 
         |
256 | 252, 255 | syl 17 |
. 2
 

          
               |
257 | 256 | 3impia 1206 |
1
 
          
              |