Step | Hyp | Ref
| Expression |
1 | | simp3 999 |
. . . 4
 
   |
2 | 1 | lt0ne0d 8447 |
. . 3
 
   |
3 | | divalglemex 11897 |
. . 3
 
   
           |
4 | 2, 3 | syld3an3 1283 |
. 2
 
   
           |
5 | | nfv 1528 |
. . . . . 6
     
   |
6 | | nfre1 2520 |
. . . . . . 7
   
          |
7 | | nfv 1528 |
. . . . . . 7
  |
8 | 6, 7 | nfim 1572 |
. . . . . 6
    
        
  |
9 | | oveq1 5875 |
. . . . . . . . . . . 12
       |
10 | 9 | oveq1d 5883 |
. . . . . . . . . . 11
           |
11 | 10 | eqeq2d 2189 |
. . . . . . . . . 10
 
   
       |
12 | 11 | 3anbi3d 1318 |
. . . . . . . . 9
  
        
    
        |
13 | 12 | cbvrexv 2704 |
. . . . . . . 8
  
   
    
 
           |
14 | | simpr 110 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
15 | | simp2 998 |
. . . . . . . . . . . . . . . . . 18
 
   |
16 | 15 | znegcld 9353 |
. . . . . . . . . . . . . . . . 17
 
    |
17 | 15 | zred 9351 |
. . . . . . . . . . . . . . . . . . 19
 
   |
18 | 17 | lt0neg1d 8449 |
. . . . . . . . . . . . . . . . . 18
 
 
    |
19 | 1, 18 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
 
    |
20 | | elnnz 9239 |
. . . . . . . . . . . . . . . . 17
 
      |
21 | 16, 19, 20 | sylanbrc 417 |
. . . . . . . . . . . . . . . 16
 
    |
22 | 21 | ad5antr 496 |
. . . . . . . . . . . . . . 15
            
   
     
 
             |
23 | | simplrr 536 |
. . . . . . . . . . . . . . . 16
     
 

  |
24 | 23 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
            
   
     
 
            |
25 | | simplrl 535 |
. . . . . . . . . . . . . . . 16
     
 

  |
26 | 25 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
            
   
     
 
            |
27 | | simplr 528 |
. . . . . . . . . . . . . . . 16
            
   
     
 
            |
28 | 27 | znegcld 9353 |
. . . . . . . . . . . . . . 15
            
   
     
 
             |
29 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
     
 

  |
30 | 29 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
            
   
     
 
            |
31 | 30 | znegcld 9353 |
. . . . . . . . . . . . . . 15
            
   
     
 
             |
32 | | simpr1 1003 |
. . . . . . . . . . . . . . . 16
      
 


   
     
  |
33 | 32 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
            
   
     
 
            |
34 | | simpr2 1004 |
. . . . . . . . . . . . . . . 16
            
   
     
 
                |
35 | | simpll2 1037 |
. . . . . . . . . . . . . . . . . . 19
     
 

  |
36 | 35 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . 18
            
   
     
 
            |
37 | 36 | zred 9351 |
. . . . . . . . . . . . . . . . 17
            
   
     
 
            |
38 | | 0red 7936 |
. . . . . . . . . . . . . . . . . 18
            
   
     
 
            |
39 | | simpll3 1038 |
. . . . . . . . . . . . . . . . . . 19
     
 

  |
40 | 39 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . 18
            
   
     
 
            |
41 | 37, 38, 40 | ltled 8053 |
. . . . . . . . . . . . . . . . 17
            
   
     
 
            |
42 | 37, 41 | absnidd 11140 |
. . . . . . . . . . . . . . . 16
            
   
     
 
                 |
43 | 34, 42 | breqtrd 4026 |
. . . . . . . . . . . . . . 15
            
   
     
 
             |
44 | | simpr3 1005 |
. . . . . . . . . . . . . . . . 17
            
   
     
 
                |
45 | 27 | zcnd 9352 |
. . . . . . . . . . . . . . . . . . 19
            
   
     
 
            |
46 | 36 | zcnd 9352 |
. . . . . . . . . . . . . . . . . . 19
            
   
     
 
            |
47 | 45, 46 | mul2negd 8347 |
. . . . . . . . . . . . . . . . . 18
            
   
     
 
                  |
48 | 47 | oveq1d 5883 |
. . . . . . . . . . . . . . . . 17
            
   
     
 
            
         |
49 | 44, 48 | eqtr4d 2213 |
. . . . . . . . . . . . . . . 16
            
   
     
 
                  |
50 | | simpr3 1005 |
. . . . . . . . . . . . . . . . . 18
      
 


   
     
      |
51 | 50 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
            
   
     
 
                |
52 | 30 | zcnd 9352 |
. . . . . . . . . . . . . . . . . . 19
            
   
     
 
            |
53 | 52, 46 | mul2negd 8347 |
. . . . . . . . . . . . . . . . . 18
            
   
     
 
                  |
54 | 53 | oveq1d 5883 |
. . . . . . . . . . . . . . . . 17
            
   
     
 
            
         |
55 | 51, 54 | eqtr4d 2213 |
. . . . . . . . . . . . . . . 16
            
   
     
 
                  |
56 | 49, 55 | eqtr3d 2212 |
. . . . . . . . . . . . . . 15
            
   
     
 
            
           |
57 | 22, 24, 26, 28, 31, 33, 43, 56 | divalglemnqt 11895 |
. . . . . . . . . . . . . 14
            
   
     
 
         
    |
58 | 30 | zred 9351 |
. . . . . . . . . . . . . . 15
            
   
     
 
            |
59 | 27 | zred 9351 |
. . . . . . . . . . . . . . 15
            
   
     
 
            |
60 | 58, 59 | ltnegd 8457 |
. . . . . . . . . . . . . 14
            
   
     
 
                |
61 | 57, 60 | mtbird 673 |
. . . . . . . . . . . . 13
            
   
     
 
         
  |
62 | 61 | adantr 276 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
63 | 14, 62 | pm2.21dd 620 |
. . . . . . . . . . 11
         
 


   
     
 
          
  |
64 | 36 | adantr 276 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
65 | 26 | adantr 276 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
66 | 24 | adantr 276 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
67 | 30 | adantr 276 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
68 | 27 | adantr 276 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
69 | | simpr 110 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
70 | 51 | adantr 276 |
. . . . . . . . . . . . 13
         
 


   
     
 
          
      |
71 | 44 | adantr 276 |
. . . . . . . . . . . . 13
         
 


   
     
 
          
      |
72 | 70, 71 | eqtr3d 2212 |
. . . . . . . . . . . 12
         
 


   
     
 
          
          |
73 | 64, 65, 66, 67, 68, 69, 72 | divalglemqt 11894 |
. . . . . . . . . . 11
         
 


   
     
 
          
  |
74 | | simpr 110 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
75 | | simpr1 1003 |
. . . . . . . . . . . . . . 15
            
   
     
 
            |
76 | | simpr2 1004 |
. . . . . . . . . . . . . . . . 17
      
 


   
     
      |
77 | 76 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
            
   
     
 
                |
78 | 77, 42 | breqtrd 4026 |
. . . . . . . . . . . . . . 15
            
   
     
 
             |
79 | 55, 49 | eqtr3d 2212 |
. . . . . . . . . . . . . . 15
            
   
     
 
            
           |
80 | 22, 26, 24, 31, 28, 75, 78, 79 | divalglemnqt 11895 |
. . . . . . . . . . . . . 14
            
   
     
 
         
    |
81 | 59, 58 | ltnegd 8457 |
. . . . . . . . . . . . . 14
            
   
     
 
                |
82 | 80, 81 | mtbird 673 |
. . . . . . . . . . . . 13
            
   
     
 
         
  |
83 | 82 | adantr 276 |
. . . . . . . . . . . 12
         
 


   
     
 
          
  |
84 | 74, 83 | pm2.21dd 620 |
. . . . . . . . . . 11
         
 


   
     
 
          
  |
85 | | simplr 528 |
. . . . . . . . . . . . 13
      
 


   
        |
86 | 85 | ad2antrr 488 |
. . . . . . . . . . . 12
            
   
     
 
            |
87 | | ztri3or 9272 |
. . . . . . . . . . . 12
 
 
   |
88 | 86, 27, 87 | syl2anc 411 |
. . . . . . . . . . 11
            
   
     
 
              |
89 | 63, 73, 84, 88 | mpjao3dan 1307 |
. . . . . . . . . 10
            
   
     
 
            |
90 | 89 | ex 115 |
. . . . . . . . 9
     
 
 


   
     
  
        
   |
91 | 90 | rexlimdva 2594 |
. . . . . . . 8
      
 


   
        
        
   |
92 | 13, 91 | biimtrid 152 |
. . . . . . 7
      
 


   
        
        
   |
93 | 92 | exp31 364 |
. . . . . 6
      

 
   
      

              |
94 | 5, 8, 93 | rexlimd 2591 |
. . . . 5
      
 

   
      

             |
95 | 94 | impd 254 |
. . . 4
      
  

          
   
         |
96 | 95 | ralrimivva 2559 |
. . 3
 
      
   
     

   
         |
97 | | breq2 4004 |
. . . . . 6
 
   |
98 | | breq1 4003 |
. . . . . 6
 
   
       |
99 | | oveq2 5876 |
. . . . . . 7
           |
100 | 99 | eqeq2d 2189 |
. . . . . 6
 
   
       |
101 | 97, 98, 100 | 3anbi123d 1312 |
. . . . 5
  
        
    
        |
102 | 101 | rexbidv 2478 |
. . . 4
  

        
 
            |
103 | 102 | rmo4 2930 |
. . 3
  

   
    
     
   
     

   
         |
104 | 96, 103 | sylibr 134 |
. 2
 
 
 
           |
105 | | reu5 2689 |
. 2
  

   
    
 
 
           
            |
106 | 4, 104, 105 | sylanbrc 417 |
1
 
 
 
           |