Step | Hyp | Ref
| Expression |
1 | | ax-1cn 6776 |
. . . . . 6
 |
2 | | 1ap0 7374 |
. . . . . 6
#  |
3 | 1, 2 | div0api 7504 |
. . . . 5
   |
4 | | 0z 8032 |
. . . . . 6
 |
5 | | 1nn 7706 |
. . . . . 6
 |
6 | | znq 8335 |
. . . . . 6
 
  
  |
7 | 4, 5, 6 | mp2an 402 |
. . . . 5
   |
8 | 3, 7 | eqeltrri 2108 |
. . . 4
 |
9 | | qapne 8350 |
. . . 4
 
  #    |
10 | 8, 9 | mpan2 401 |
. . 3
  #
   |
11 | 10 | biimpar 281 |
. 2
   #   |
12 | | elq 8333 |
. . . 4
       |
13 | | nnne0 7723 |
. . . . . . . 8
   |
14 | 13 | ancli 306 |
. . . . . . 7
 
   |
15 | | nnz 8040 |
. . . . . . . . . . . . . . . 16
   |
16 | | zapne 8091 |
. . . . . . . . . . . . . . . 16
 
  #    |
17 | 15, 4, 16 | sylancl 392 |
. . . . . . . . . . . . . . 15
  #
   |
18 | 17 | adantl 262 |
. . . . . . . . . . . . . 14
 
  #    |
19 | 18 | pm5.32i 427 |
. . . . . . . . . . . . 13
   
#    
   |
20 | 19 | anbi1i 431 |
. . . . . . . . . . . 12
     # 

 
  

      |
21 | | breq1 3758 |
. . . . . . . . . . . . 13
  
 #
  #    |
22 | | zcn 8026 |
. . . . . . . . . . . . . . . 16
   |
23 | | nncn 7703 |
. . . . . . . . . . . . . . . 16
   |
24 | 22, 23 | anim12i 321 |
. . . . . . . . . . . . . . 15
 
     |
25 | | divap0b 7444 |
. . . . . . . . . . . . . . . 16
 
# 
 #
  #    |
26 | 25 | 3expa 1103 |
. . . . . . . . . . . . . . 15
   
#   #   #    |
27 | 24, 26 | sylan 267 |
. . . . . . . . . . . . . 14
   
#   #   #    |
28 | 27 | bicomd 129 |
. . . . . . . . . . . . 13
   
#     #
#    |
29 | 21, 28 | sylan9bbr 436 |
. . . . . . . . . . . 12
     # 

 
 #
#    |
30 | 20, 29 | sylbir 125 |
. . . . . . . . . . 11
        
 #
#    |
31 | | simplll 485 |
. . . . . . . . . . . 12
        
  |
32 | | zapne 8091 |
. . . . . . . . . . . 12
 
  #    |
33 | 31, 4, 32 | sylancl 392 |
. . . . . . . . . . 11
        
 #
   |
34 | 30, 33 | bitrd 177 |
. . . . . . . . . 10
        
 #
   |
35 | | zmulcl 8073 |
. . . . . . . . . . . . . . . . 17
 
  
  |
36 | 15, 35 | sylan2 270 |
. . . . . . . . . . . . . . . 16
 
  
  |
37 | 36 | adantr 261 |
. . . . . . . . . . . . . . 15
   
  
  |
38 | | msqznn 8114 |
. . . . . . . . . . . . . . . 16
   

  |
39 | 38 | adantlr 446 |
. . . . . . . . . . . . . . 15
   
  
  |
40 | 37, 39 | jca 290 |
. . . . . . . . . . . . . 14
   
         |
41 | 40 | adantlr 446 |
. . . . . . . . . . . . 13
        

     |
42 | 41 | adantlr 446 |
. . . . . . . . . . . 12
         
  

     |
43 | 20 | anbi1i 431 |
. . . . . . . . . . . . . 14
      # 

 
# 
    
    #    |
44 | 33 | pm5.32i 427 |
. . . . . . . . . . . . . 14
         
# 
    
       |
45 | 43, 44 | bitri 173 |
. . . . . . . . . . . . 13
      # 

 
# 
    
       |
46 | | oveq2 5463 |
. . . . . . . . . . . . . . 15
  

       |
47 | | dividap 7460 |
. . . . . . . . . . . . . . . . . . . . 21
  #      |
48 | 47 | adantr 261 |
. . . . . . . . . . . . . . . . . . . 20
   #  
#    
  |
49 | 48 | oveq1d 5470 |
. . . . . . . . . . . . . . . . . . 19
   #  
#     
    
    |
50 | | simpll 481 |
. . . . . . . . . . . . . . . . . . . 20
   #  
#     |
51 | | simpl 102 |
. . . . . . . . . . . . . . . . . . . 20
   #  
#    #    |
52 | | simpr 103 |
. . . . . . . . . . . . . . . . . . . 20
   #  
#    #    |
53 | | divdivdivap 7471 |
. . . . . . . . . . . . . . . . . . . 20
    #     #   #      
      
    |
54 | 50, 51, 51, 52, 53 | syl22anc 1135 |
. . . . . . . . . . . . . . . . . . 19
   #  
#     
      
    |
55 | 49, 54 | eqtr3d 2071 |
. . . . . . . . . . . . . . . . . 18
   #  
#          
    |
56 | 55 | an4s 522 |
. . . . . . . . . . . . . . . . 17
     # #          
    |
57 | 24, 56 | sylan 267 |
. . . . . . . . . . . . . . . 16
     # #          
    |
58 | 57 | anass1rs 505 |
. . . . . . . . . . . . . . 15
     # 
# 

     
     |
59 | 46, 58 | sylan9eqr 2091 |
. . . . . . . . . . . . . 14
      # 
# 

 

   
     |
60 | 59 | an32s 502 |
. . . . . . . . . . . . 13
      # 

 
# 

   
     |
61 | 45, 60 | sylbir 125 |
. . . . . . . . . . . 12
         
 
   
     |
62 | 42, 61 | jca 290 |
. . . . . . . . . . 11
         
    
   
   
      |
63 | 62 | ex 108 |
. . . . . . . . . 10
        
    
   
   
       |
64 | 34, 63 | sylbid 139 |
. . . . . . . . 9
        
 #
   
   
   
       |
65 | 64 | ex 108 |
. . . . . . . 8
   
  
  #        
   
        |
66 | 65 | anasss 379 |
. . . . . . 7
  
    
 #
   
   
   
        |
67 | 14, 66 | sylan2 270 |
. . . . . 6
 
     #    
 
  
   
       |
68 | | rspceov 5489 |
. . . . . . . 8
   
           
 
     |
69 | 68 | 3expa 1103 |
. . . . . . 7
    
 
  
   
   
  
    |
70 | | elq 8333 |
. . . . . . 7
      
    |
71 | 69, 70 | sylibr 137 |
. . . . . 6
    
 
  
   
   
   |
72 | 67, 71 | syl8 65 |
. . . . 5
 
     #  
    |
73 | 72 | rexlimivv 2432 |
. . . 4
 
    #  
   |
74 | 12, 73 | sylbi 114 |
. . 3
  #

    |
75 | 74 | imp 115 |
. 2
  #  
   |
76 | 11, 75 | syldan 266 |
1
    
  |