Step | Hyp | Ref
| Expression |
1 | | ee4anv 1858 |
. . . 4
               
 
     
      
                        
 
     |
2 | | an4 554 |
. . . . . . 7
       
 
     
      
    
  
                 |
3 | | eleq1 2151 |
. . . . . . . . . . . . 13
  
          |
4 | | eleq1 2151 |
. . . . . . . . . . . . 13
  
          |
5 | 3, 4 | bi2anan9 574 |
. . . . . . . . . . . 12
            
             |
6 | 5 | adantr 271 |
. . . . . . . . . . 11
    
  
        
                |
7 | 6 | biimpac 293 |
. . . . . . . . . 10
    
               
            |
8 | | eqtr2 2107 |
. . . . . . . . . . . . 13
           |
9 | | eqtr2 2107 |
. . . . . . . . . . . . 13
           |
10 | 8, 9 | anim12i 332 |
. . . . . . . . . . . 12
    
  
                |
11 | 10 | an4s 556 |
. . . . . . . . . . 11
    
  
                |
12 | 11 | adantl 272 |
. . . . . . . . . 10
    
               
           |
13 | | th3qlem1.1 |
. . . . . . . . . . . 12
 |
14 | 13 | a1i 9 |
. . . . . . . . . . 11
           
            |
15 | | simprl 499 |
. . . . . . . . . . . . 13
           
               |
16 | | erdm 6316 |
. . . . . . . . . . . . . . . 16
  |
17 | 13, 16 | ax-mp 7 |
. . . . . . . . . . . . . . 15
 |
18 | | simpll 497 |
. . . . . . . . . . . . . . 15
           
                |
19 | | ecelqsdm 6376 |
. . . . . . . . . . . . . . 15
         |
20 | 17, 18, 19 | sylancr 406 |
. . . . . . . . . . . . . 14
           
            |
21 | 14, 20 | erth 6350 |
. . . . . . . . . . . . 13
           
          
      |
22 | 15, 21 | mpbird 166 |
. . . . . . . . . . . 12
           
            |
23 | | simprr 500 |
. . . . . . . . . . . . 13
           
               |
24 | | simplr 498 |
. . . . . . . . . . . . . . 15
           
                |
25 | | ecelqsdm 6376 |
. . . . . . . . . . . . . . 15
         |
26 | 17, 24, 25 | sylancr 406 |
. . . . . . . . . . . . . 14
           
            |
27 | 14, 26 | erth 6350 |
. . . . . . . . . . . . 13
           
          
      |
28 | 23, 27 | mpbird 166 |
. . . . . . . . . . . 12
           
            |
29 | 15, 18 | eqeltrrd 2166 |
. . . . . . . . . . . . . 14
           
                |
30 | | ecelqsdm 6376 |
. . . . . . . . . . . . . 14
         |
31 | 17, 29, 30 | sylancr 406 |
. . . . . . . . . . . . 13
           
            |
32 | 23, 24 | eqeltrrd 2166 |
. . . . . . . . . . . . . 14
           
                |
33 | | ecelqsdm 6376 |
. . . . . . . . . . . . . 14
         |
34 | 17, 32, 33 | sylancr 406 |
. . . . . . . . . . . . 13
           
            |
35 | | th3qlem1.3 |
. . . . . . . . . . . . 13
  


    
  
    |
36 | 20, 31, 26, 34, 35 | syl22anc 1176 |
. . . . . . . . . . . 12
           
           

  
    |
37 | 22, 28, 36 | mp2and 425 |
. . . . . . . . . . 11
           
          
     |
38 | 14, 37 | erthi 6352 |
. . . . . . . . . 10
           
                   |
39 | 7, 12, 38 | syl2anc 404 |
. . . . . . . . 9
    
               
 
       |
40 | | eqeq12 2101 |
. . . . . . . . 9
                     |
41 | 39, 40 | syl5ibrcom 156 |
. . . . . . . 8
    
               
             |
42 | 41 | expimpd 356 |
. . . . . . 7
   
                              |
43 | 2, 42 | syl5bi 151 |
. . . . . 6
   
                    
 
  
   |
44 | 43 | exlimdvv 1826 |
. . . . 5
   
                        
 
  
   |
45 | 44 | exlimdvv 1826 |
. . . 4
   
                            
 
  
   |
46 | 1, 45 | syl5bir 152 |
. . 3
   
                            
 
  
   |
47 | 46 | alrimivv 1804 |
. 2
   
                                
 
  
   |
48 | | eqeq1 2095 |
. . . . . 6
     
      |
49 | 48 | anbi2d 453 |
. . . . 5
       
 
 
 
           |
50 | 49 | 2exbidv 1797 |
. . . 4
         
               
 
     |
51 | | eceq1 6341 |
. . . . . . . 8
      |
52 | 51 | eqeq2d 2100 |
. . . . . . 7
 
 
    |
53 | | eceq1 6341 |
. . . . . . . 8
      |
54 | 53 | eqeq2d 2100 |
. . . . . . 7
 
 
    |
55 | 52, 54 | bi2anan9 574 |
. . . . . 6
 
      
        |
56 | | oveq12 5675 |
. . . . . . . 8
 
       |
57 | 56 | eceq1d 6342 |
. . . . . . 7
 
          |
58 | 57 | eqeq2d 2100 |
. . . . . 6
 
     
      |
59 | 55, 58 | anbi12d 458 |
. . . . 5
 
               
         |
60 | 59 | cbvex2v 1848 |
. . . 4
        
               
 
    |
61 | 50, 60 | syl6bb 195 |
. . 3
         
               
 
     |
62 | 61 | mo4 2010 |
. 2
                                              
 
  
   |
63 | 47, 62 | sylibr 133 |
1
   
                     |