Step | Hyp | Ref
| Expression |
1 | | eluznn 11258 |
. . . . 5
 
    
  |
2 | | fveq2 5888 |
. . . . . . . 8
           |
3 | 2 | negeqd 9895 |
. . . . . . 7
             |
4 | 3 | oveq2d 6331 |
. . . . . 6
                     |
5 | | aaliou3lem.b |
. . . . . 6
            |
6 | | ovex 6343 |
. . . . . 6
          |
7 | 4, 5, 6 | fvmpt 5971 |
. . . . 5
                |
8 | 1, 7 | syl 17 |
. . . 4
 
                    |
9 | | 2rp 11336 |
. . . . 5
 |
10 | 1 | nnnn0d 10954 |
. . . . . . . 8
 
    
  |
11 | | faccl 12501 |
. . . . . . . 8

      |
12 | 10, 11 | syl 17 |
. . . . . . 7
 
           |
13 | 12 | nnzd 11068 |
. . . . . 6
 
           |
14 | 13 | znegcld 11071 |
. . . . 5
 
            |
15 | | rpexpcl 12323 |
. . . . 5
                   |
16 | 9, 14, 15 | sylancr 674 |
. . . 4
 
                |
17 | 8, 16 | eqeltrd 2540 |
. . 3
 
           |
18 | 17 | rpred 11370 |
. 2
 
           |
19 | 17 | rpgt0d 11373 |
. 2
 
    
      |
20 | | fveq2 5888 |
. . . . . 6
           |
21 | | fveq2 5888 |
. . . . . 6
           |
22 | 20, 21 | breq12d 4429 |
. . . . 5
     
   
           |
23 | 22 | imbi2d 322 |
. . . 4
      
    

            |
24 | | fveq2 5888 |
. . . . . 6
           |
25 | | fveq2 5888 |
. . . . . 6
           |
26 | 24, 25 | breq12d 4429 |
. . . . 5
     
   
           |
27 | 26 | imbi2d 322 |
. . . 4
      
    

            |
28 | | fveq2 5888 |
. . . . . 6
               |
29 | | fveq2 5888 |
. . . . . 6
               |
30 | 28, 29 | breq12d 4429 |
. . . . 5
       
   
               |
31 | 30 | imbi2d 322 |
. . . 4
        
    

                |
32 | | fveq2 5888 |
. . . . . 6
           |
33 | | fveq2 5888 |
. . . . . 6
           |
34 | 32, 33 | breq12d 4429 |
. . . . 5
     
   
           |
35 | 34 | imbi2d 322 |
. . . 4
      
    

            |
36 | | nnnn0 10905 |
. . . . . . . . . . . . 13
   |
37 | | faccl 12501 |
. . . . . . . . . . . . 13

      |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
       |
39 | 38 | nnzd 11068 |
. . . . . . . . . . 11
       |
40 | 39 | znegcld 11071 |
. . . . . . . . . 10
        |
41 | | rpexpcl 12323 |
. . . . . . . . . 10
                   |
42 | 9, 40, 41 | sylancr 674 |
. . . . . . . . 9
            |
43 | 42 | rpred 11370 |
. . . . . . . 8
            |
44 | 43 | leidd 10208 |
. . . . . . 7
         
           |
45 | | nncn 10645 |
. . . . . . . . . . . 12
   |
46 | 45 | subidd 10000 |
. . . . . . . . . . 11
 
   |
47 | 46 | oveq2d 6331 |
. . . . . . . . . 10
                 |
48 | | halfcn 10858 |
. . . . . . . . . . 11
   |
49 | | exp0 12308 |
. . . . . . . . . . 11
           |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . 10
       |
51 | 47, 50 | syl6eq 2512 |
. . . . . . . . 9
           |
52 | 51 | oveq2d 6331 |
. . . . . . . 8
                                 |
53 | 42 | rpcnd 11372 |
. . . . . . . . 9
            |
54 | 53 | mulid1d 9686 |
. . . . . . . 8
                       |
55 | 52, 54 | eqtrd 2496 |
. . . . . . 7
                               |
56 | 44, 55 | breqtrrd 4443 |
. . . . . 6
         
                     |
57 | | fveq2 5888 |
. . . . . . . . 9
           |
58 | 57 | negeqd 9895 |
. . . . . . . 8
             |
59 | 58 | oveq2d 6331 |
. . . . . . 7
                     |
60 | | ovex 6343 |
. . . . . . 7
          |
61 | 59, 5, 60 | fvmpt 5971 |
. . . . . 6
                |
62 | | nnz 10988 |
. . . . . . 7
   |
63 | | uzid 11202 |
. . . . . . 7
       |
64 | | oveq1 6322 |
. . . . . . . . . 10
       |
65 | 64 | oveq2d 6331 |
. . . . . . . . 9
                   |
66 | 65 | oveq2d 6331 |
. . . . . . . 8
                                         |
67 | | aaliou3lem.a |
. . . . . . . 8
                          |
68 | | ovex 6343 |
. . . . . . . 8
                    |
69 | 66, 67, 68 | fvmpt 5971 |
. . . . . . 7
    
                         |
70 | 62, 63, 69 | 3syl 18 |
. . . . . 6
                          |
71 | 56, 61, 70 | 3brtr4d 4447 |
. . . . 5
           |
72 | 71 | a1i 11 |
. . . 4
 
           |
73 | | eluznn 11258 |
. . . . . . . . . . . . . . . . . 18
 
       |
74 | 73 | nnnn0d 10954 |
. . . . . . . . . . . . . . . . 17
 
       |
75 | | faccl 12501 |
. . . . . . . . . . . . . . . . 17

      |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
 
           |
77 | 76 | nnzd 11068 |
. . . . . . . . . . . . . . 15
 
           |
78 | 77 | znegcld 11071 |
. . . . . . . . . . . . . 14
 
            |
79 | | rpexpcl 12323 |
. . . . . . . . . . . . . 14
                   |
80 | 9, 78, 79 | sylancr 674 |
. . . . . . . . . . . . 13
 
                |
81 | 80 | rpred 11370 |
. . . . . . . . . . . 12
 
                |
82 | 80 | rpge0d 11374 |
. . . . . . . . . . . 12
 
    
           |
83 | | simpl 463 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
84 | 83 | nnnn0d 10954 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
85 | 84, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
           |
86 | 85 | nnzd 11068 |
. . . . . . . . . . . . . . . 16
 
           |
87 | 86 | znegcld 11071 |
. . . . . . . . . . . . . . 15
 
            |
88 | 9, 87, 41 | sylancr 674 |
. . . . . . . . . . . . . 14
 
                |
89 | | halfre 10857 |
. . . . . . . . . . . . . . . 16
   |
90 | | halfgt0 10859 |
. . . . . . . . . . . . . . . 16
   |
91 | 89, 90 | elrpii 11334 |
. . . . . . . . . . . . . . 15
   |
92 | | eluzelz 11197 |
. . . . . . . . . . . . . . . 16
    
  |
93 | | zsubcl 11008 |
. . . . . . . . . . . . . . . 16
 
     |
94 | 92, 62, 93 | syl2anr 485 |
. . . . . . . . . . . . . . 15
 
         |
95 | | rpexpcl 12323 |
. . . . . . . . . . . . . . 15
                 |
96 | 91, 94, 95 | sylancr 674 |
. . . . . . . . . . . . . 14
 
               |
97 | 88, 96 | rpmulcld 11386 |
. . . . . . . . . . . . 13
 
                          |
98 | 97 | rpred 11370 |
. . . . . . . . . . . 12
 
                          |
99 | 81, 82, 98 | jca31 541 |
. . . . . . . . . . 11
 
                                                |
100 | 99 | adantr 471 |
. . . . . . . . . 10
                
                   
                                           |
101 | 92 | adantl 472 |
. . . . . . . . . . . . . . 15
 
       |
102 | 78, 101 | zmulcld 11075 |
. . . . . . . . . . . . . 14
 
              |
103 | | rpexpcl 12323 |
. . . . . . . . . . . . . 14
                       |
104 | 9, 102, 103 | sylancr 674 |
. . . . . . . . . . . . 13
 
                  |
105 | 104 | rpred 11370 |
. . . . . . . . . . . 12
 
                  |
106 | 104 | rpge0d 11374 |
. . . . . . . . . . . 12
 
    
             |
107 | 89 | a1i 11 |
. . . . . . . . . . . 12
 
         |
108 | 105, 106,
107 | jca31 541 |
. . . . . . . . . . 11
 
                                   |
109 | 108 | adantr 471 |
. . . . . . . . . 10
                
                   
                              |
110 | | simpr 467 |
. . . . . . . . . 10
                
                   
                              |
111 | 76 | nncnd 10653 |
. . . . . . . . . . . . . . . 16
 
           |
112 | 101 | zcnd 11070 |
. . . . . . . . . . . . . . . 16
 
       |
113 | 111, 112 | mulneg1d 10099 |
. . . . . . . . . . . . . . 15
 
                     |
114 | 76, 73 | nnmulcld 10685 |
. . . . . . . . . . . . . . . . 17
 
             |
115 | 114 | nnge1d 10680 |
. . . . . . . . . . . . . . . 16
 
    
        |
116 | | 1re 9668 |
. . . . . . . . . . . . . . . . 17
 |
117 | 114 | nnred 10652 |
. . . . . . . . . . . . . . . . 17
 
             |
118 | | leneg 10145 |
. . . . . . . . . . . . . . . . 17
                           |
119 | 116, 117,
118 | sylancr 674 |
. . . . . . . . . . . . . . . 16
 
                  
    |
120 | 115, 119 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
           
   |
121 | 113, 120 | eqbrtrd 4437 |
. . . . . . . . . . . . . 14
 
           
   |
122 | | neg1z 11002 |
. . . . . . . . . . . . . . 15
  |
123 | | eluz 11201 |
. . . . . . . . . . . . . . 15
         
             
           |
124 | 102, 122,
123 | sylancl 673 |
. . . . . . . . . . . . . 14
 
                 
           |
125 | 121, 124 | mpbird 240 |
. . . . . . . . . . . . 13
 
                   |
126 | | 2re 10707 |
. . . . . . . . . . . . . 14
 |
127 | | 1le2 10852 |
. . . . . . . . . . . . . 14
 |
128 | | leexp2a 12360 |
. . . . . . . . . . . . . 14
                                 |
129 | 126, 127,
128 | mp3an12 1363 |
. . . . . . . . . . . . 13
                               |
130 | 125, 129 | syl 17 |
. . . . . . . . . . . 12
 
               
       |
131 | | 2cn 10708 |
. . . . . . . . . . . . 13
 |
132 | | expn1 12314 |
. . . . . . . . . . . . 13
          |
133 | 131, 132 | ax-mp 5 |
. . . . . . . . . . . 12
        |
134 | 130, 133 | syl6breq 4456 |
. . . . . . . . . . 11
 
               
    |
135 | 134 | adantr 471 |
. . . . . . . . . 10
                
                   
               |
136 | | lemul12a 10491 |
. . . . . . . . . . 11
                                                                                  
                                                                                 |
137 | 136 | 3impia 1212 |
. . . . . . . . . 10
                                                                                                                                                                  |
138 | 100, 109,
110, 135, 137 | syl112anc 1280 |
. . . . . . . . 9
                
                   
                                               |
139 | 138 | ex 440 |
. . . . . . . 8
 
                                                                                  |
140 | | facp1 12496 |
. . . . . . . . . . . . . 14

                |
141 | 74, 140 | syl 17 |
. . . . . . . . . . . . 13
 
                     |
142 | 141 | negeqd 9895 |
. . . . . . . . . . . 12
 
                       |
143 | | ax-1cn 9623 |
. . . . . . . . . . . . . . 15
 |
144 | | addcom 9845 |
. . . . . . . . . . . . . . 15
 
       |
145 | 112, 143,
144 | sylancl 673 |
. . . . . . . . . . . . . 14
 
           |
146 | 145 | oveq2d 6331 |
. . . . . . . . . . . . 13
 
                         |
147 | | peano2cn 9831 |
. . . . . . . . . . . . . . 15
     |
148 | 112, 147 | syl 17 |
. . . . . . . . . . . . . 14
 
         |
149 | 111, 148 | mulneg1d 10099 |
. . . . . . . . . . . . 13
 
                         |
150 | 78 | zcnd 11070 |
. . . . . . . . . . . . . . 15
 
            |
151 | | 1cnd 9685 |
. . . . . . . . . . . . . . 15
 
       |
152 | 150, 151,
112 | adddid 9693 |
. . . . . . . . . . . . . 14
 
                                |
153 | 150 | mulid1d 9686 |
. . . . . . . . . . . . . . 15
 
                   |
154 | 153 | oveq1d 6330 |
. . . . . . . . . . . . . 14
 
                                     |
155 | 152, 154 | eqtrd 2496 |
. . . . . . . . . . . . 13
 
                              |
156 | 146, 149,
155 | 3eqtr3d 2504 |
. . . . . . . . . . . 12
 
                              |
157 | 142, 156 | eqtrd 2496 |
. . . . . . . . . . 11
 
                            |
158 | 157 | oveq2d 6331 |
. . . . . . . . . 10
 
                                    |
159 | | 2cnne0 10853 |
. . . . . . . . . . . 12
   |
160 | | expaddz 12348 |
. . . . . . . . . . . 12
                                                             |
161 | 159, 160 | mpan 681 |
. . . . . . . . . . 11
                                                         |
162 | 78, 102, 161 | syl2anc 671 |
. . . . . . . . . 10
 
                                               |
163 | 158, 162 | eqtrd 2496 |
. . . . . . . . 9
 
                                        |
164 | 45 | adantr 471 |
. . . . . . . . . . . . . 14
 
    
  |
165 | 112, 151,
164 | addsubd 10033 |
. . . . . . . . . . . . 13
 
               |
166 | 165 | oveq2d 6331 |
. . . . . . . . . . . 12
 
                           |
167 | | uznn0sub 11219 |
. . . . . . . . . . . . . 14
    
    |
168 | 167 | adantl 472 |
. . . . . . . . . . . . 13
 
         |
169 | | expp1 12311 |
. . . . . . . . . . . . 13
                               |
170 | 48, 168, 169 | sylancr 674 |
. . . . . . . . . . . 12
 
                             |
171 | 166, 170 | eqtrd 2496 |
. . . . . . . . . . 11
 
                             |
172 | 171 | oveq2d 6331 |
. . . . . . . . . 10
 
                                                   |
173 | 88 | rpcnd 11372 |
. . . . . . . . . . 11
 
                |
174 | 96 | rpcnd 11372 |
. . . . . . . . . . 11
 
               |
175 | 48 | a1i 11 |
. . . . . . . . . . 11
 
         |
176 | 173, 174,
175 | mulassd 9692 |
. . . . . . . . . 10
 
                                                     |
177 | 172, 176 | eqtr4d 2499 |
. . . . . . . . 9
 
                                                   |
178 | 163, 177 | breq12d 4429 |
. . . . . . . 8
 
                                     
                                                |
179 | 139, 178 | sylibrd 242 |
. . . . . . 7
 
                                            
                        |
180 | | fveq2 5888 |
. . . . . . . . . . . 12
           |
181 | 180 | negeqd 9895 |
. . . . . . . . . . 11
             |
182 | 181 | oveq2d 6331 |
. . . . . . . . . 10
                     |
183 | | ovex 6343 |
. . . . . . . . . 10
          |
184 | 182, 5, 183 | fvmpt 5971 |
. . . . . . . . 9
                |
185 | 73, 184 | syl 17 |
. . . . . . . 8
 
                    |
186 | | oveq1 6322 |
. . . . . . . . . . . 12
       |
187 | 186 | oveq2d 6331 |
. . . . . . . . . . 11
                   |
188 | 187 | oveq2d 6331 |
. . . . . . . . . 10
                                         |
189 | | ovex 6343 |
. . . . . . . . . 10
                    |
190 | 188, 67, 189 | fvmpt 5971 |
. . . . . . . . 9
    
                         |
191 | 190 | adantl 472 |
. . . . . . . 8
 
                              |
192 | 185, 191 | breq12d 4429 |
. . . . . . 7
 
                      
                      |
193 | 73 | peano2nnd 10654 |
. . . . . . . . 9
 
         |
194 | | fveq2 5888 |
. . . . . . . . . . . 12
               |
195 | 194 | negeqd 9895 |
. . . . . . . . . . 11
                 |
196 | 195 | oveq2d 6331 |
. . . . . . . . . 10
                         |
197 | | ovex 6343 |
. . . . . . . . . 10
            |
198 | 196, 5, 197 | fvmpt 5971 |
. . . . . . . . 9
                      |
199 | 193, 198 | syl 17 |
. . . . . . . 8
 
                        |
200 | | peano2uz 11241 |
. . . . . . . . . 10
    
        |
201 | | oveq1 6322 |
. . . . . . . . . . . . 13
           |
202 | 201 | oveq2d 6331 |
. . . . . . . . . . . 12
                       |
203 | 202 | oveq2d 6331 |
. . . . . . . . . . 11
                                             |
204 | | ovex 6343 |
. . . . . . . . . . 11
                      |
205 | 203, 67, 204 | fvmpt 5971 |
. . . . . . . . . 10
      
                             |
206 | 200, 205 | syl 17 |
. . . . . . . . 9
    
                             |
207 | 206 | adantl 472 |
. . . . . . . 8
 
                                  |
208 | 199, 207 | breq12d 4429 |
. . . . . . 7
 
                            
                        |
209 | 179, 192,
208 | 3imtr4d 276 |
. . . . . 6
 
                   
         |
210 | 209 | expcom 441 |
. . . . 5
    

        
                |
211 | 210 | a2d 29 |
. . . 4
    
 
               
          |
212 | 23, 27, 31, 35, 72, 211 | uzind4 11246 |
. . 3
    

           |
213 | 212 | impcom 436 |
. 2
 
        
      |
214 | | 0xr 9713 |
. . 3
 |
215 | 67 | aaliou3lem1 23347 |
. . 3
 
           |
216 | | elioc2 11726 |
. . 3
              ![(,] (,]](_ioc.gif)     
        
            |
217 | 214, 215,
216 | sylancr 674 |
. 2
 
            ![(,] (,]](_ioc.gif)                           |
218 | 18, 19, 213, 217 | mpbir3and 1197 |
1
 
           ![(,] (,]](_ioc.gif)        |