Step | Hyp | Ref
| Expression |
1 | | zfpow 4595 |
. . . 4
        
  |
2 | | 19.8a 1945 |
. . . . . . . 8
 
  |
3 | | sp 1947 |
. . . . . . . 8
 
  |
4 | 2, 3 | imim12i 59 |
. . . . . . 7
  

     |
5 | 4 | alimi 1694 |
. . . . . 6
    
 
      |
6 | 5 | imim1i 60 |
. . . . 5
           
 
   |
7 | 6 | alimi 1694 |
. . . 4
       
       

    |
8 | 1, 7 | eximii 1719 |
. . 3
         
   |
9 | | nfnae 2162 |
. . . . 5
   |
10 | | nfnae 2162 |
. . . . 5
   |
11 | 9, 10 | nfan 2021 |
. . . 4
   
   |
12 | | nfnae 2162 |
. . . . . 6
   |
13 | | nfnae 2162 |
. . . . . 6
   |
14 | 12, 13 | nfan 2021 |
. . . . 5
   
   |
15 | | nfv 1771 |
. . . . . . 7
   
   |
16 | | nfnae 2162 |
. . . . . . . . . 10
   |
17 | | nfcvd 2603 |
. . . . . . . . . . 11
 
    |
18 | | nfcvf 2625 |
. . . . . . . . . . 11
 
    |
19 | 17, 18 | nfeld 2610 |
. . . . . . . . . 10
 

  |
20 | 16, 19 | nfexd 2045 |
. . . . . . . . 9
 
  
  |
21 | 20 | adantr 471 |
. . . . . . . 8
    
  
  |
22 | | nfcvd 2603 |
. . . . . . . . . . 11
 
    |
23 | | nfcvf 2625 |
. . . . . . . . . . 11
 
    |
24 | 22, 23 | nfeld 2610 |
. . . . . . . . . 10
 

  |
25 | 13, 24 | nfald 2044 |
. . . . . . . . 9
 
  
  |
26 | 25 | adantl 472 |
. . . . . . . 8
    
  
  |
27 | 21, 26 | nfimd 2010 |
. . . . . . 7
    
    
   |
28 | 15, 27 | nfald 2044 |
. . . . . 6
    
     
    |
29 | 18, 17 | nfeld 2610 |
. . . . . . 7
 

  |
30 | 29 | adantr 471 |
. . . . . 6
    

  |
31 | 28, 30 | nfimd 2010 |
. . . . 5
    
      

    |
32 | 14, 31 | nfald 2044 |
. . . 4
    
         
    |
33 | | nfeqf2 2145 |
. . . . . . . . 9
 

  |
34 | 33 | naecoms 2157 |
. . . . . . . 8
 

  |
35 | 34 | adantr 471 |
. . . . . . 7
    

  |
36 | 14, 35 | nfan1 2020 |
. . . . . 6
    
 
  |
37 | | nfnae 2162 |
. . . . . . . . . . . . . 14
   |
38 | | nfeqf2 2145 |
. . . . . . . . . . . . . . 15
 

  |
39 | 38 | naecoms 2157 |
. . . . . . . . . . . . . 14
 

  |
40 | 37, 39 | nfan1 2020 |
. . . . . . . . . . . . 13
   
  |
41 | | elequ1 1904 |
. . . . . . . . . . . . . 14
 
   |
42 | 41 | adantl 472 |
. . . . . . . . . . . . 13
    
   |
43 | 40, 42 | exbid 1974 |
. . . . . . . . . . . 12
     
    |
44 | 43 | adantll 725 |
. . . . . . . . . . 11
   
    
    |
45 | 12, 34 | nfan1 2020 |
. . . . . . . . . . . . 13
   
  |
46 | | elequ1 1904 |
. . . . . . . . . . . . . 14
 
   |
47 | 46 | adantl 472 |
. . . . . . . . . . . . 13
    
   |
48 | 45, 47 | albid 1973 |
. . . . . . . . . . . 12
     
    |
49 | 48 | adantlr 726 |
. . . . . . . . . . 11
   
    
    |
50 | 44, 49 | imbi12d 326 |
. . . . . . . . . 10
   
      
  

    |
51 | 50 | ex 440 |
. . . . . . . . 9
    

  

  

     |
52 | 11, 27, 51 | cbvald 2128 |
. . . . . . . 8
    
    
           |
53 | 52 | adantr 471 |
. . . . . . 7
   
       
           |
54 | | elequ2 1911 |
. . . . . . . 8
 
   |
55 | 54 | adantl 472 |
. . . . . . 7
   
   
   |
56 | 53, 55 | imbi12d 326 |
. . . . . 6
   
        

      

     |
57 | 36, 56 | albid 1973 |
. . . . 5
   
           
         
     |
58 | 57 | ex 440 |
. . . 4
    

        
         
      |
59 | 11, 32, 58 | cbvexd 2129 |
. . 3
    
         
 

         
     |
60 | 8, 59 | mpbii 216 |
. 2
    
         
    |
61 | 60 | ex 440 |
1
 
          

     |