Step | Hyp | Ref
| Expression |
1 | | locfincmp.1 |
. . . . . . . . . 10
  |
2 | 1 | locfinnei 20593 |
. . . . . . . . 9
       

       |
3 | 2 | ralrimiva 2814 |
. . . . . . . 8
    



       |
4 | 1 | cmpcov2 20460 |
. . . . . . . 8
  

              
       |
5 | 3, 4 | sylan2 481 |
. . . . . . 7
      
       
       |
6 | | elfpw 7907 |
. . . . . . . . 9
   
    |
7 | | simplrr 776 |
. . . . . . . . . . 11
                |
8 | | eldifsn 4110 |
. . . . . . . . . . . . 13
    

   |
9 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . 19
          
  
 

       |
10 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . 20
          
  
 

       |
11 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . 20
          
  
 

       |
12 | | inelcm 3831 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
13 | 10, 11, 12 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
          
  
 

     
   |
14 | | ineq1 3639 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
15 | 14 | neeq1d 2695 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
16 | 15 | elrab 3208 |
. . . . . . . . . . . . . . . . . . 19
           |
17 | 9, 13, 16 | sylanbrc 675 |
. . . . . . . . . . . . . . . . . 18
          
  
 

           |
18 | | elunii 4217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    |
19 | | locfincmp.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  |
20 | 18, 19 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
21 | 20 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
22 | 21 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
    
    
  
 

    |
23 | 1, 19 | locfinbas 20592 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
  |
24 | 23 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
      
  |
25 | 24 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . . 21
    
    
  
 

 
  |
26 | 22, 25 | eleqtrrd 2543 |
. . . . . . . . . . . . . . . . . . . 20
    
    
  
 

    |
27 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . 20
    
    
  
 

 
   |
28 | 26, 27 | eleqtrd 2542 |
. . . . . . . . . . . . . . . . . . 19
    
    
  
 

     |
29 | | eluni2 4216 |
. . . . . . . . . . . . . . . . . . 19
 

  |
30 | 28, 29 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
    
    
  
 

  
  |
31 | 17, 30 | reximddv 2875 |
. . . . . . . . . . . . . . . . 17
    
    
  
 

  


    |
32 | 31 | expr 624 |
. . . . . . . . . . . . . . . 16
    
    
  
 
  


     |
33 | 32 | exlimdv 1790 |
. . . . . . . . . . . . . . 15
    
    
  
 
  
        |
34 | | n0 3753 |
. . . . . . . . . . . . . . 15
    |
35 | | eliun 4297 |
. . . . . . . . . . . . . . 15
             |
36 | 33, 34, 35 | 3imtr4g 278 |
. . . . . . . . . . . . . 14
    
    
  
 
          |
37 | 36 | expimpd 612 |
. . . . . . . . . . . . 13
                
        |
38 | 8, 37 | syl5bi 225 |
. . . . . . . . . . . 12
                  
        |
39 | 38 | ssrdv 3450 |
. . . . . . . . . . 11
                  


    |
40 | | iunfi 7893 |
. . . . . . . . . . . . 13
       



    |
41 | 40 | ex 440 |
. . . . . . . . . . . 12
  
            |
42 | | ssfi 7823 |
. . . . . . . . . . . . 13
                       |
43 | 42 | expcom 441 |
. . . . . . . . . . . 12
    
    
 
           |
44 | 41, 43 | sylan9 667 |
. . . . . . . . . . 11
  
  
       
           |
45 | 7, 39, 44 | syl2anc 671 |
. . . . . . . . . 10
                           |
46 | 45 | expimpd 612 |
. . . . . . . . 9
        
                  |
47 | 6, 46 | sylan2b 482 |
. . . . . . . 8
       
            
       |
48 | 47 | rexlimdva 2891 |
. . . . . . 7
      
 
           
       |
49 | 5, 48 | mpd 15 |
. . . . . 6
      
      |
50 | | snfi 7681 |
. . . . . 6
   |
51 | | unfi 7869 |
. . . . . 6
                   |
52 | 49, 50, 51 | sylancl 673 |
. . . . 5
      
          |
53 | | ssun1 3609 |
. . . . . 6

    |
54 | | undif1 3854 |
. . . . . 6
             |
55 | 53, 54 | sseqtr4i 3477 |
. . . . 5
         |
56 | | ssfi 7823 |
. . . . 5
         
        
  |
57 | 52, 55, 56 | sylancl 673 |
. . . 4
      
  |
58 | 57, 24 | jca 539 |
. . 3
      
    |
59 | 58 | ex 440 |
. 2

    
     |
60 | | cmptop 20465 |
. . 3

  |
61 | 1, 19 | finlocfin 20590 |
. . . 4
 
       |
62 | 61 | 3expib 1218 |
. . 3
           |
63 | 60, 62 | syl 17 |
. 2

 
        |
64 | 59, 63 | impbid 195 |
1

     
    |