Step | Hyp | Ref
| Expression |
1 | | 0cn 6817 |
. 2
 |
2 | | cnre 6821 |
. 2
 
       |
3 | | ax-rnegex 6792 |
. . . . . 6
 

   |
4 | 3 | adantr 261 |
. . . . 5
 
  

  |
5 | | recn 6812 |
. . . . . . . . . . 11
   |
6 | | ax-icn 6778 |
. . . . . . . . . . . 12
 |
7 | | recn 6812 |
. . . . . . . . . . . 12
   |
8 | | mulcl 6806 |
. . . . . . . . . . . 12
 
  
  |
9 | 6, 7, 8 | sylancr 393 |
. . . . . . . . . . 11
     |
10 | | recn 6812 |
. . . . . . . . . . 11
   |
11 | | addid2 6949 |
. . . . . . . . . . . . . . 15
     |
12 | 11 | 3ad2ant3 926 |
. . . . . . . . . . . . . 14
  

     |
13 | 12 | adantr 261 |
. . . . . . . . . . . . 13
    
  

          |
14 | | oveq1 5462 |
. . . . . . . . . . . . . . 15
    

         |
15 | 14 | ad2antrl 459 |
. . . . . . . . . . . . . 14
    
  

                  |
16 | | add32 6967 |
. . . . . . . . . . . . . . . . 17
 
    

     
 
   |
17 | 16 | 3com23 1109 |
. . . . . . . . . . . . . . . 16
  

  

     
 
   |
18 | | oveq1 5462 |
. . . . . . . . . . . . . . . . 17
  
 
          |
19 | 18 | eqcomd 2042 |
. . . . . . . . . . . . . . . 16
  
 
 
        |
20 | 17, 19 | sylan9eq 2089 |
. . . . . . . . . . . . . . 15
    
       

       |
21 | 20 | adantrl 447 |
. . . . . . . . . . . . . 14
    
  

                |
22 | | addid2 6949 |
. . . . . . . . . . . . . . . 16
           |
23 | 22 | 3ad2ant2 925 |
. . . . . . . . . . . . . . 15
  

         |
24 | 23 | adantr 261 |
. . . . . . . . . . . . . 14
    
  

              |
25 | 15, 21, 24 | 3eqtr3d 2077 |
. . . . . . . . . . . . 13
    
  

            |
26 | 13, 25 | eqtr3d 2071 |
. . . . . . . . . . . 12
    
  

     
    |
27 | 26 | ex 108 |
. . . . . . . . . . 11
  

         
     |
28 | 5, 9, 10, 27 | syl3an 1176 |
. . . . . . . . . 10
 
         
     |
29 | 28 | 3expa 1103 |
. . . . . . . . 9
   
               |
30 | 29 | imp 115 |
. . . . . . . 8
       

     
    |
31 | | simplr 482 |
. . . . . . . 8
       

     
  |
32 | 30, 31 | eqeltrrd 2112 |
. . . . . . 7
       

      

  |
33 | 32 | exp32 347 |
. . . . . 6
   
      
 
      |
34 | 33 | rexlimdva 2427 |
. . . . 5
 
    
      
    |
35 | 4, 34 | mpd 13 |
. . . 4
 
       
   |
36 | 35 | reximdva 2415 |
. . 3
  
   
  
   |
37 | 36 | rexlimiv 2421 |
. 2
 
      

  |
38 | 1, 2, 37 | mp2b 8 |
1
  
 |