Step | Hyp | Ref
| Expression |
1 | | fveq2 5879 |
. . 3
           |
2 | | fveq2 5879 |
. . 3
           |
3 | | fveq2 5879 |
. . 3
           |
4 | | zssre 10968 |
. . 3
 |
5 | | eleq1 2537 |
. . . . . 6
 
   |
6 | 5 | anbi2d 718 |
. . . . 5
  

     |
7 | | fveq2 5879 |
. . . . . 6
           |
8 | 7 | eleq1d 2533 |
. . . . 5
     
       |
9 | 6, 8 | imbi12d 327 |
. . . 4
   
       
         |
10 | | monotoddzzfi.1 |
. . . 4
 

      |
11 | 9, 10 | chvarv 2120 |
. . 3
 

      |
12 | | elznn 10977 |
. . . . . . 7

       |
13 | 12 | simprbi 471 |
. . . . . 6
      |
14 | | elznn 10977 |
. . . . . . 7

       |
15 | 14 | simprbi 471 |
. . . . . 6
      |
16 | 13, 15 | anim12i 576 |
. . . . 5
 
           |
17 | 16 | adantl 473 |
. . . 4
 
             |
18 | | simpll 768 |
. . . . . . 7
   
 
     |
19 | | nnnn0 10900 |
. . . . . . . 8
   |
20 | 19 | ad2antrl 742 |
. . . . . . 7
   
 
     |
21 | | nnnn0 10900 |
. . . . . . . 8
   |
22 | 21 | ad2antll 743 |
. . . . . . 7
   
 
     |
23 | | vex 3034 |
. . . . . . . 8
 |
24 | | vex 3034 |
. . . . . . . 8
 |
25 | | simpl 464 |
. . . . . . . . . . 11
 
   |
26 | 25 | eleq1d 2533 |
. . . . . . . . . 10
 
     |
27 | | simpr 468 |
. . . . . . . . . . 11
 
   |
28 | 27 | eleq1d 2533 |
. . . . . . . . . 10
 
     |
29 | 26, 28 | 3anbi23d 1368 |
. . . . . . . . 9
 
  


    |
30 | | breq12 4400 |
. . . . . . . . . 10
 
     |
31 | | fveq2 5879 |
. . . . . . . . . . 11
           |
32 | 7, 31 | breqan12d 4411 |
. . . . . . . . . 10
 
                     |
33 | 30, 32 | imbi12d 327 |
. . . . . . . . 9
 
  
         
            |
34 | 29, 33 | imbi12d 327 |
. . . . . . . 8
 
   
     
       
 
             |
35 | | monotoddzzfi.3 |
. . . . . . . 8
 
 
           |
36 | 23, 24, 34, 35 | vtocl2 3088 |
. . . . . . 7
 
 
           |
37 | 18, 20, 22, 36 | syl3anc 1292 |
. . . . . 6
   
 
       
       |
38 | 37 | ex 441 |
. . . . 5
 
      
            |
39 | 11 | adantrr 731 |
. . . . . . . . 9
 
         |
40 | 39 | adantr 472 |
. . . . . . . 8
   
 
          |
41 | | 0red 9662 |
. . . . . . . 8
   
 
      |
42 | | eleq1 2537 |
. . . . . . . . . . . . 13
 
   |
43 | 42 | anbi2d 718 |
. . . . . . . . . . . 12
  

     |
44 | | fveq2 5879 |
. . . . . . . . . . . . 13
           |
45 | 44 | eleq1d 2533 |
. . . . . . . . . . . 12
     
       |
46 | 43, 45 | imbi12d 327 |
. . . . . . . . . . 11
   
       
         |
47 | 46, 10 | chvarv 2120 |
. . . . . . . . . 10
 

      |
48 | 47 | adantrl 730 |
. . . . . . . . 9
 
         |
49 | 48 | adantr 472 |
. . . . . . . 8
   
 
          |
50 | | 0red 9662 |
. . . . . . . . . . . 12
        
      |
51 | | znegcl 10996 |
. . . . . . . . . . . . . . 15
    |
52 | 51 | ad2antrl 742 |
. . . . . . . . . . . . . 14
 
      |
53 | | negex 9893 |
. . . . . . . . . . . . . . 15
  |
54 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
  
    |
55 | 54 | anbi2d 718 |
. . . . . . . . . . . . . . . 16
   

 
    |
56 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
             |
57 | 56 | eleq1d 2533 |
. . . . . . . . . . . . . . . 16
      
        |
58 | 55, 57 | imbi12d 327 |
. . . . . . . . . . . . . . 15
    
                   |
59 | 53, 58, 10 | vtocl 3086 |
. . . . . . . . . . . . . 14
 
         |
60 | 52, 59 | syldan 478 |
. . . . . . . . . . . . 13
 
          |
61 | 60 | ad2antrr 740 |
. . . . . . . . . . . 12
        
           |
62 | | 0z 10972 |
. . . . . . . . . . . . . . . . . 18
 |
63 | | c0ex 9655 |
. . . . . . . . . . . . . . . . . . 19
 |
64 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
65 | 64 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . 20
  

     |
66 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
67 | 66 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
68 | 65, 67 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . 19
   
       
         |
69 | 63, 68, 10 | vtocl 3086 |
. . . . . . . . . . . . . . . . . 18
 

      |
70 | 62, 69 | mpan2 685 |
. . . . . . . . . . . . . . . . 17
       |
71 | 70 | recnd 9687 |
. . . . . . . . . . . . . . . 16
       |
72 | | neg0 9940 |
. . . . . . . . . . . . . . . . . 18
  |
73 | 72 | fveq2i 5882 |
. . . . . . . . . . . . . . . . 17
          |
74 | | negeq 9887 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
75 | 74 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
             |
76 | 66 | negeqd 9889 |
. . . . . . . . . . . . . . . . . . . . 21
             |
77 | 75, 76 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . . . 20
                         |
78 | 65, 77 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . 19
   
                             |
79 | | monotoddzzfi.2 |
. . . . . . . . . . . . . . . . . . 19
 

            |
80 | 63, 78, 79 | vtocl 3086 |
. . . . . . . . . . . . . . . . . 18
 

            |
81 | 62, 80 | mpan2 685 |
. . . . . . . . . . . . . . . . 17
             |
82 | 73, 81 | syl5eqr 2519 |
. . . . . . . . . . . . . . . 16
            |
83 | 71, 82 | eqnegad 10351 |
. . . . . . . . . . . . . . 15
       |
84 | 83 | adantr 472 |
. . . . . . . . . . . . . 14
 
         |
85 | 84 | ad2antrr 740 |
. . . . . . . . . . . . 13
        
          |
86 | | nngt0 10660 |
. . . . . . . . . . . . . . 15
 
   |
87 | 86 | adantl 473 |
. . . . . . . . . . . . . 14
        
       |
88 | | simplll 776 |
. . . . . . . . . . . . . . 15
        
      |
89 | | 0nn0 10908 |
. . . . . . . . . . . . . . . 16
 |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . 15
        
      |
91 | | simplrl 778 |
. . . . . . . . . . . . . . 15
        
       |
92 | | simpl 464 |
. . . . . . . . . . . . . . . . . . 19
   
  |
93 | 92 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
   
    |
94 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
   
   |
95 | 94 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
   
     |
96 | 93, 95 | 3anbi23d 1368 |
. . . . . . . . . . . . . . . . 17
   
   
     |
97 | | breq12 4400 |
. . . . . . . . . . . . . . . . . 18
   
     |
98 | 92 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
   
          |
99 | 94 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
   
           |
100 | 98, 99 | breq12d 4408 |
. . . . . . . . . . . . . . . . . 18
   
                     |
101 | 97, 100 | imbi12d 327 |
. . . . . . . . . . . . . . . . 17
   
 
        
               |
102 | 96, 101 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
   
  
 
           
  
    
          |
103 | 63, 53, 102, 35 | vtocl2 3088 |
. . . . . . . . . . . . . . 15
 
   
            |
104 | 88, 90, 91, 103 | syl3anc 1292 |
. . . . . . . . . . . . . 14
        
     
            |
105 | 87, 104 | mpd 15 |
. . . . . . . . . . . . 13
        
               |
106 | 85, 105 | eqbrtrrd 4418 |
. . . . . . . . . . . 12
        
           |
107 | 50, 61, 106 | ltled 9800 |
. . . . . . . . . . 11
        
           |
108 | | 0le0 10721 |
. . . . . . . . . . . . 13
 |
109 | 84 | ad2antrr 740 |
. . . . . . . . . . . . 13
        
          |
110 | 108, 109 | syl5breqr 4432 |
. . . . . . . . . . . 12
        
          |
111 | | fveq2 5879 |
. . . . . . . . . . . . . 14
 
           |
112 | 111 | breq2d 4407 |
. . . . . . . . . . . . 13
 

    
       |
113 | 112 | adantl 473 |
. . . . . . . . . . . 12
        
                 |
114 | 110, 113 | mpbird 240 |
. . . . . . . . . . 11
        
           |
115 | | elnn0 10895 |
. . . . . . . . . . . . 13
 
      |
116 | 115 | biimpi 199 |
. . . . . . . . . . . 12
 
      |
117 | 116 | ad2antrl 742 |
. . . . . . . . . . 11
   
 
          |
118 | 107, 114,
117 | mpjaodan 803 |
. . . . . . . . . 10
   
 
   
       |
119 | | negeq 9887 |
. . . . . . . . . . . . . . . 16
     |
120 | 119 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
             |
121 | 7 | negeqd 9889 |
. . . . . . . . . . . . . . 15
             |
122 | 120, 121 | eqeq12d 2486 |
. . . . . . . . . . . . . 14
                         |
123 | 6, 122 | imbi12d 327 |
. . . . . . . . . . . . 13
   
                             |
124 | 123, 79 | chvarv 2120 |
. . . . . . . . . . . 12
 

            |
125 | 124 | adantrr 731 |
. . . . . . . . . . 11
 
               |
126 | 125 | adantr 472 |
. . . . . . . . . 10
   
 
                |
127 | 118, 126 | breqtrd 4420 |
. . . . . . . . 9
   
 
   
       |
128 | 40 | le0neg1d 10206 |
. . . . . . . . 9
   
 
                 |
129 | 127, 128 | mpbird 240 |
. . . . . . . 8
   
 
       
  |
130 | 84 | adantr 472 |
. . . . . . . . 9
   
 
          |
131 | | nngt0 10660 |
. . . . . . . . . . 11
   |
132 | 131 | ad2antll 743 |
. . . . . . . . . 10
   
 
   
  |
133 | | simpll 768 |
. . . . . . . . . . 11
   
 
      |
134 | 89 | a1i 11 |
. . . . . . . . . . 11
   
 
      |
135 | 21 | ad2antll 743 |
. . . . . . . . . . 11
   
 
      |
136 | | simpl 464 |
. . . . . . . . . . . . . . 15
     |
137 | 136 | eleq1d 2533 |
. . . . . . . . . . . . . 14
       |
138 | | simpr 468 |
. . . . . . . . . . . . . . 15
     |
139 | 138 | eleq1d 2533 |
. . . . . . . . . . . . . 14
       |
140 | 137, 139 | 3anbi23d 1368 |
. . . . . . . . . . . . 13
    


    |
141 | | breq12 4400 |
. . . . . . . . . . . . . 14
       |
142 | 66, 31 | breqan12d 4411 |
. . . . . . . . . . . . . 14
                       |
143 | 141, 142 | imbi12d 327 |
. . . . . . . . . . . . 13
             
             |
144 | 140, 143 | imbi12d 327 |
. . . . . . . . . . . 12
     
 
         
       
         |
145 | 63, 24, 144, 35 | vtocl2 3088 |
. . . . . . . . . . 11
 
 
           |
146 | 133, 134,
135, 145 | syl3anc 1292 |
. . . . . . . . . 10
   
 
        
       |
147 | 132, 146 | mpd 15 |
. . . . . . . . 9
   
 
       
      |
148 | 130, 147 | eqbrtrrd 4418 |
. . . . . . . 8
   
 
   
      |
149 | 40, 41, 49, 129, 148 | lelttrd 9810 |
. . . . . . 7
   
 
       
      |
150 | 149 | a1d 25 |
. . . . . 6
   
 
        
       |
151 | 150 | ex 441 |
. . . . 5
 
       
            |
152 | | simp3 1032 |
. . . . . . 7
   
 
      |
153 | | zre 10965 |
. . . . . . . . . . . 12
   |
154 | 153 | adantl 473 |
. . . . . . . . . . 11
 
   |
155 | 154 | ad2antlr 741 |
. . . . . . . . . 10
   
 
      |
156 | | 1red 9676 |
. . . . . . . . . 10
   
 
      |
157 | | nnre 10638 |
. . . . . . . . . . 11
   |
158 | 157 | ad2antrl 742 |
. . . . . . . . . 10
   
 
      |
159 | | 0red 9662 |
. . . . . . . . . . 11
   
 
      |
160 | | nn0ge0 10919 |
. . . . . . . . . . . . 13
 
   |
161 | 160 | ad2antll 743 |
. . . . . . . . . . . 12
   
 
   
   |
162 | 155 | le0neg1d 10206 |
. . . . . . . . . . . 12
   
 
         |
163 | 161, 162 | mpbird 240 |
. . . . . . . . . . 11
   
 
   
  |
164 | | 0le1 10158 |
. . . . . . . . . . . 12
 |
165 | 164 | a1i 11 |
. . . . . . . . . . 11
   
 
   
  |
166 | 155, 159,
156, 163, 165 | letrd 9809 |
. . . . . . . . . 10
   
 
   
  |
167 | | nnge1 10657 |
. . . . . . . . . . 11
   |
168 | 167 | ad2antrl 742 |
. . . . . . . . . 10
   
 
   
  |
169 | 155, 156,
158, 166, 168 | letrd 9809 |
. . . . . . . . 9
   
 
   
  |
170 | 155, 158 | lenltd 9798 |
. . . . . . . . 9
   
 
        |
171 | 169, 170 | mpbid 215 |
. . . . . . . 8
   
 
   
  |
172 | 171 | 3adant3 1050 |
. . . . . . 7
   
 
      |
173 | 152, 172 | pm2.21dd 179 |
. . . . . 6
   
 
              |
174 | 173 | 3exp 1230 |
. . . . 5
 
       
            |
175 | | negex 9893 |
. . . . . . . . . . . 12
  |
176 | | simpl 464 |
. . . . . . . . . . . . . . 15
  
 
   |
177 | 176 | eleq1d 2533 |
. . . . . . . . . . . . . 14
  
 
     |
178 | | simpr 468 |
. . . . . . . . . . . . . . 15
  
 
   |
179 | 178 | eleq1d 2533 |
. . . . . . . . . . . . . 14
  
 
     |
180 | 177, 179 | 3anbi23d 1368 |
. . . . . . . . . . . . 13
  
 
   

     |
181 | | breq12 4400 |
. . . . . . . . . . . . . 14
  
 
      |
182 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
             |
183 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
             |
184 | 182, 183 | breqan12d 4411 |
. . . . . . . . . . . . . 14
  
 
                      |
185 | 181, 184 | imbi12d 327 |
. . . . . . . . . . . . 13
  
 
 
        
                 |
186 | 180, 185 | imbi12d 327 |
. . . . . . . . . . . 12
  
 
  
 
                 
               |
187 | 175, 53, 186, 35 | vtocl2 3088 |
. . . . . . . . . . 11
 

         
        |
188 | 187 | 3com23 1237 |
. . . . . . . . . 10
 

         
        |
189 | 188 | 3expb 1232 |
. . . . . . . . 9
 
            
        |
190 | 189 | adantlr 729 |
. . . . . . . 8
   
 
            
        |
191 | | negeq 9887 |
. . . . . . . . . . . . . . 15
     |
192 | 191 | fveq2d 5883 |
. . . . . . . . . . . . . 14
             |
193 | 44 | negeqd 9889 |
. . . . . . . . . . . . . 14
             |
194 | 192, 193 | eqeq12d 2486 |
. . . . . . . . . . . . 13
                         |
195 | 43, 194 | imbi12d 327 |
. . . . . . . . . . . 12
   
                             |
196 | 195, 79 | chvarv 2120 |
. . . . . . . . . . 11
 

            |
197 | 196 | adantrl 730 |
. . . . . . . . . 10
 
               |
198 | 197 | adantr 472 |
. . . . . . . . 9
   
 
                 |
199 | 125 | adantr 472 |
. . . . . . . . 9
   
 
                 |
200 | 198, 199 | breq12d 4408 |
. . . . . . . 8
   
 
                    
        |
201 | 190, 200 | sylibd 222 |
. . . . . . 7
   
 
                     |
202 | | zre 10965 |
. . . . . . . . . 10
   |
203 | 202 | ad2antrl 742 |
. . . . . . . . 9
 
     |
204 | 203 | adantr 472 |
. . . . . . . 8
   
 
       |
205 | 154 | ad2antlr 741 |
. . . . . . . 8
   
 
       |
206 | 204, 205 | ltnegd 10212 |
. . . . . . 7
   
 
           |
207 | 39 | adantr 472 |
. . . . . . . 8
   
 
           |
208 | 48 | adantr 472 |
. . . . . . . 8
   
 
           |
209 | 207, 208 | ltnegd 10212 |
. . . . . . 7
   
 
                  
        |
210 | 201, 206,
209 | 3imtr4d 276 |
. . . . . 6
   
 
         
       |
211 | 210 | ex 441 |
. . . . 5
 
        
            |
212 | 38, 151, 174, 211 | ccased 962 |
. . . 4
 
           

            |
213 | 17, 212 | mpd 15 |
. . 3
 
       
       |
214 | 1, 2, 3, 4, 11, 213 | ltord1 10161 |
. 2
 
               |
215 | 214 | 3impb 1227 |
1
 
             |