Step | Hyp | Ref
| Expression |
1 | | r19.26 2904 |
. . . 4
 
 
       
 
    |
2 | | simpr 468 |
. . . . . . . . . 10
   
 

  |
3 | | simpl1 1033 |
. . . . . . . . . 10
   
 

  |
4 | 2, 3 | pccld 14879 |
. . . . . . . . 9
   
 
     |
5 | 4 | nn0red 10950 |
. . . . . . . 8
   
 
     |
6 | | simpl2 1034 |
. . . . . . . . . 10
   
 

  |
7 | 2, 6 | pccld 14879 |
. . . . . . . . 9
   
 
     |
8 | 7 | nn0red 10950 |
. . . . . . . 8
   
 
     |
9 | | 1red 9676 |
. . . . . . . 8
   
 
   |
10 | | le2add 10117 |
. . . . . . . 8
     
    
   

             |
11 | 5, 8, 9, 9, 10 | syl22anc 1293 |
. . . . . . 7
   
 
      
    
 
     |
12 | | ax-1ne0 9626 |
. . . . . . . . . . . 12
 |
13 | | simpl3 1035 |
. . . . . . . . . . . . . . . 16
   
 
     |
14 | 13 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
   
 
         |
15 | 3 | nnzd 11062 |
. . . . . . . . . . . . . . . 16
   
 

  |
16 | 6 | nnzd 11062 |
. . . . . . . . . . . . . . . 16
   
 

  |
17 | | pcgcd 14906 |
. . . . . . . . . . . . . . . 16
   
       
          |
18 | 2, 15, 16, 17 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
   
 
       
       
    |
19 | | pc1 14884 |
. . . . . . . . . . . . . . . 16

    |
20 | 19 | adantl 473 |
. . . . . . . . . . . . . . 15
   
 
     |
21 | 14, 18, 20 | 3eqtr3d 2513 |
. . . . . . . . . . . . . 14
   
 
    
   
       |
22 | | ifid 3909 |
. . . . . . . . . . . . . . . 16
   
      |
23 | | ifeq12 3889 |
. . . . . . . . . . . . . . . 16
          
         
          |
24 | 22, 23 | syl5eqr 2519 |
. . . . . . . . . . . . . . 15
           
          |
25 | 24 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
           
   
        |
26 | 21, 25 | syl5ibrcom 230 |
. . . . . . . . . . . . 13
   
 
    

 
   |
27 | 26 | necon3ad 2656 |
. . . . . . . . . . . 12
   
 
    

     |
28 | 12, 27 | mpi 20 |
. . . . . . . . . . 11
   
 
  


    |
29 | | ax-1cn 9615 |
. . . . . . . . . . . . 13
 |
30 | 5 | recnd 9687 |
. . . . . . . . . . . . 13
   
 
     |
31 | | subeq0 9920 |
. . . . . . . . . . . . 13
  
            |
32 | 29, 30, 31 | sylancr 676 |
. . . . . . . . . . . 12
   
 
           |
33 | 8 | recnd 9687 |
. . . . . . . . . . . . 13
   
 
     |
34 | | subeq0 9920 |
. . . . . . . . . . . . 13
  
            |
35 | 29, 33, 34 | sylancr 676 |
. . . . . . . . . . . 12
   
 
           |
36 | 32, 35 | anbi12d 725 |
. . . . . . . . . . 11
   
 
              

     |
37 | 28, 36 | mtbird 308 |
. . . . . . . . . 10
   
 
             |
38 | 37 | adantr 472 |
. . . . . . . . 9
          

  
            |
39 | | eqcom 2478 |
. . . . . . . . . . 11
      
     
      |
40 | | 1re 9660 |
. . . . . . . . . . . . . . . . . 18
 |
41 | 40, 40 | readdcli 9674 |
. . . . . . . . . . . . . . . . 17
   |
42 | 41 | recni 9673 |
. . . . . . . . . . . . . . . 16
   |
43 | 4, 7 | nn0addcld 10953 |
. . . . . . . . . . . . . . . . . 18
   
 
         |
44 | 43 | nn0red 10950 |
. . . . . . . . . . . . . . . . 17
   
 
         |
45 | 44 | recnd 9687 |
. . . . . . . . . . . . . . . 16
   
 
         |
46 | | subeq0 9920 |
. . . . . . . . . . . . . . . 16
                     
           |
47 | 42, 45, 46 | sylancr 676 |
. . . . . . . . . . . . . . 15
   
 
           
           |
48 | 47, 39 | syl6bb 269 |
. . . . . . . . . . . . . 14
   
 
           
 
         |
49 | 9 | recnd 9687 |
. . . . . . . . . . . . . . . 16
   
 
   |
50 | 49, 49, 30, 33 | addsub4d 10052 |
. . . . . . . . . . . . . . 15
   
 
                       |
51 | 50 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
   
 
           
      
      |
52 | 48, 51 | bitr3d 263 |
. . . . . . . . . . . . 13
   
 
     
   
      
      |
53 | 52 | adantr 472 |
. . . . . . . . . . . 12
          

     
                   |
54 | | subge0 10148 |
. . . . . . . . . . . . . . . 16
  
      
     |
55 | 40, 5, 54 | sylancr 676 |
. . . . . . . . . . . . . . 15
   
 
     
     |
56 | | subge0 10148 |
. . . . . . . . . . . . . . . 16
  
      
     |
57 | 40, 8, 56 | sylancr 676 |
. . . . . . . . . . . . . . 15
   
 
     
     |
58 | 55, 57 | anbi12d 725 |
. . . . . . . . . . . . . 14
   
 
    
 
       

     |
59 | | resubcl 9958 |
. . . . . . . . . . . . . . . 16
  
   
    |
60 | 40, 5, 59 | sylancr 676 |
. . . . . . . . . . . . . . 15
   
 
  
    |
61 | | resubcl 9958 |
. . . . . . . . . . . . . . . 16
  
   
    |
62 | 40, 8, 61 | sylancr 676 |
. . . . . . . . . . . . . . 15
   
 
  
    |
63 | | add20 10147 |
. . . . . . . . . . . . . . . . 17
      
         
             
                |
64 | 63 | an4s 842 |
. . . . . . . . . . . . . . . 16
        
     
 
     
   
                    |
65 | 64 | ex 441 |
. . . . . . . . . . . . . . 15
   
   
          
             
              |
66 | 60, 62, 65 | syl2anc 673 |
. . . . . . . . . . . . . 14
   
 
    
 
            
                 |
67 | 58, 66 | sylbird 243 |
. . . . . . . . . . . . 13
   
 
      
        
                 |
68 | 67 | imp 436 |
. . . . . . . . . . . 12
          

          
                |
69 | 53, 68 | bitrd 261 |
. . . . . . . . . . 11
          

     
                   |
70 | 39, 69 | syl5bb 265 |
. . . . . . . . . 10
          

           
             |
71 | 70 | necon3abid 2679 |
. . . . . . . . 9
          

           
  
   
      |
72 | 38, 71 | mpbird 240 |
. . . . . . . 8
          

             |
73 | 72 | ex 441 |
. . . . . . 7
   
 
      
            |
74 | 11, 73 | jcad 542 |
. . . . . 6
   
 
      
   
                  |
75 | | nnz 10983 |
. . . . . . . . . . 11
   |
76 | | nnne0 10664 |
. . . . . . . . . . 11
   |
77 | 75, 76 | jca 541 |
. . . . . . . . . 10
 
   |
78 | 3, 77 | syl 17 |
. . . . . . . . 9
   
 
     |
79 | | nnz 10983 |
. . . . . . . . . . 11
   |
80 | | nnne0 10664 |
. . . . . . . . . . 11
   |
81 | 79, 80 | jca 541 |
. . . . . . . . . 10
 
   |
82 | 6, 81 | syl 17 |
. . . . . . . . 9
   
 
     |
83 | | pcmul 14880 |
. . . . . . . . 9
  
 
   
   
      |
84 | 2, 78, 82, 83 | syl3anc 1292 |
. . . . . . . 8
   
 
  
   
      |
85 | 84 | breq1d 4405 |
. . . . . . 7
   
 
     
 
       |
86 | | 1nn0 10909 |
. . . . . . . 8
 |
87 | | nn0leltp1 11019 |
. . . . . . . 8
       

          
 
     |
88 | 43, 86, 87 | sylancl 675 |
. . . . . . 7
   
 
     
 
 
         |
89 | | ltlen 9753 |
. . . . . . . 8
                      
                  |
90 | 44, 41, 89 | sylancl 675 |
. . . . . . 7
   
 
     
 
 
                     |
91 | 85, 88, 90 | 3bitrd 287 |
. . . . . 6
   
 
     
                     |
92 | 74, 91 | sylibrd 242 |
. . . . 5
   
 
      
    
   |
93 | 92 | ralimdva 2805 |
. . . 4
 
    
  

  

      |
94 | 1, 93 | syl5bir 226 |
. . 3
 
       
 
      
   |
95 | | issqf 24142 |
. . . . 5
      
     |
96 | | issqf 24142 |
. . . . 5
      
     |
97 | 95, 96 | bi2anan9 890 |
. . . 4
 
               
 
     |
98 | 97 | 3adant3 1050 |
. . 3
 
                 
 
     |
99 | | nnmulcl 10654 |
. . . . 5
 
     |
100 | 99 | 3adant3 1050 |
. . . 4
 
   
   |
101 | | issqf 24142 |
. . . 4
       
  
       |
102 | 100, 101 | syl 17 |
. . 3
 
       
  
       |
103 | 94, 98, 102 | 3imtr4d 276 |
. 2
 
                 
     |
104 | 103 | imp 436 |
1
   
            
        |