Step | Hyp | Ref
| Expression |
1 | | 0cn 7949 |
. 2
 |
2 | | cnre 7953 |
. 2
         |
3 | | ax-rnegex 7920 |
. . . . . 6
      |
4 | 3 | adantr 276 |
. . . . 5
 
  
   |
5 | | recn 7944 |
. . . . . . . . . . 11
   |
6 | | ax-icn 7906 |
. . . . . . . . . . . 12
 |
7 | | recn 7944 |
. . . . . . . . . . . 12
   |
8 | | mulcl 7938 |
. . . . . . . . . . . 12
 
     |
9 | 6, 7, 8 | sylancr 414 |
. . . . . . . . . . 11
 
   |
10 | | recn 7944 |
. . . . . . . . . . 11
   |
11 | | addlid 8096 |
. . . . . . . . . . . . . . 15
     |
12 | 11 | 3ad2ant3 1020 |
. . . . . . . . . . . . . 14
  

     |
13 | 12 | adantr 276 |
. . . . . . . . . . . . 13
    
              |
14 | | oveq1 5882 |
. . . . . . . . . . . . . . 15
               |
15 | 14 | ad2antrl 490 |
. . . . . . . . . . . . . 14
    
                      |
16 | | add32 8116 |
. . . . . . . . . . . . . . . . 17
 

                |
17 | 16 | 3com23 1209 |
. . . . . . . . . . . . . . . 16
  

               |
18 | | oveq1 5882 |
. . . . . . . . . . . . . . . . 17
  
            |
19 | 18 | eqcomd 2183 |
. . . . . . . . . . . . . . . 16
  
            |
20 | 17, 19 | sylan9eq 2230 |
. . . . . . . . . . . . . . 15
    

    
          |
21 | 20 | adantrl 478 |
. . . . . . . . . . . . . 14
    
                    |
22 | | addlid 8096 |
. . . . . . . . . . . . . . . 16
           |
23 | 22 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . 15
  

         |
24 | 23 | adantr 276 |
. . . . . . . . . . . . . 14
    
                  |
25 | 15, 21, 24 | 3eqtr3d 2218 |
. . . . . . . . . . . . 13
    
                |
26 | 13, 25 | eqtr3d 2212 |
. . . . . . . . . . . 12
    
              |
27 | 26 | ex 115 |
. . . . . . . . . . 11
  

               |
28 | 5, 9, 10, 27 | syl3an 1280 |
. . . . . . . . . 10
 
         

    |
29 | 28 | 3expa 1203 |
. . . . . . . . 9
          
        |
30 | 29 | imp 124 |
. . . . . . . 8
              

   |
31 | | simplr 528 |
. . . . . . . 8
              
  |
32 | 30, 31 | eqeltrrd 2255 |
. . . . . . 7
              
    |
33 | 32 | exp32 365 |
. . . . . 6
       
  
  
     |
34 | 33 | rexlimdva 2594 |
. . . . 5
 
         
      |
35 | 4, 34 | mpd 13 |
. . . 4
 
           |
36 | 35 | reximdva 2579 |
. . 3
  
    

    |
37 | 36 | rexlimiv 2588 |
. 2
  
 
       |
38 | 1, 2, 37 | mp2b 8 |
1
    |