Step | Hyp | Ref
| Expression |
1 | | ee4anv 1806 |
. . . 4
               
 
         
           
                 
     |
2 | | an4 520 |
. . . . . . 7
     
         
              
    

     
     |
3 | | eleq1 2097 |
. . . . . . . . . . . . 13
             |
4 | | eleq1 2097 |
. . . . . . . . . . . . 13
             |
5 | 3, 4 | bi2anan9 538 |
. . . . . . . . . . . 12
                          |
6 | 5 | adantr 261 |
. . . . . . . . . . 11
         
                       |
7 | 6 | biimpac 282 |
. . . . . . . . . 10
           
  
     
            |
8 | | eqtr2 2055 |
. . . . . . . . . . . . 13
           |
9 | | eqtr2 2055 |
. . . . . . . . . . . . 13
           |
10 | 8, 9 | anim12i 321 |
. . . . . . . . . . . 12
         
              |
11 | 10 | an4s 522 |
. . . . . . . . . . 11
         
              |
12 | 11 | adantl 262 |
. . . . . . . . . 10
           
  
     
           |
13 | | th3qlem1.1 |
. . . . . . . . . . . 12
 |
14 | 13 | a1i 9 |
. . . . . . . . . . 11
              
         |
15 | | simprl 483 |
. . . . . . . . . . . . 13
              
            |
16 | | erdm 6052 |
. . . . . . . . . . . . . . . 16
  |
17 | 13, 16 | ax-mp 7 |
. . . . . . . . . . . . . . 15
 |
18 | | simpll 481 |
. . . . . . . . . . . . . . 15
              
             |
19 | | ecelqsdm 6112 |
. . . . . . . . . . . . . . 15
      
  |
20 | 17, 18, 19 | sylancr 393 |
. . . . . . . . . . . . . 14
              
      
  |
21 | 14, 20 | erth 6086 |
. . . . . . . . . . . . 13
              
       
      |
22 | 15, 21 | mpbird 156 |
. . . . . . . . . . . 12
              
         |
23 | | simprr 484 |
. . . . . . . . . . . . 13
              
            |
24 | | simplr 482 |
. . . . . . . . . . . . . . 15
              
             |
25 | | ecelqsdm 6112 |
. . . . . . . . . . . . . . 15
      
  |
26 | 17, 24, 25 | sylancr 393 |
. . . . . . . . . . . . . 14
              
      
  |
27 | 14, 26 | erth 6086 |
. . . . . . . . . . . . 13
              
       
      |
28 | 23, 27 | mpbird 156 |
. . . . . . . . . . . 12
              
         |
29 | 15, 18 | eqeltrrd 2112 |
. . . . . . . . . . . . . 14
              
             |
30 | | ecelqsdm 6112 |
. . . . . . . . . . . . . 14
      
  |
31 | 17, 29, 30 | sylancr 393 |
. . . . . . . . . . . . 13
              
      
  |
32 | 23, 24 | eqeltrrd 2112 |
. . . . . . . . . . . . . 14
              
             |
33 | | ecelqsdm 6112 |
. . . . . . . . . . . . . 14
      
  |
34 | 17, 32, 33 | sylancr 393 |
. . . . . . . . . . . . 13
              
      
  |
35 | | th3qlem1.3 |
. . . . . . . . . . . . 13
  
     
  
     |
36 | 20, 31, 26, 34, 35 | syl22anc 1135 |
. . . . . . . . . . . 12
              
        
  
     |
37 | 22, 28, 36 | mp2and 409 |
. . . . . . . . . . 11
              
       
     |
38 | 14, 37 | erthi 6088 |
. . . . . . . . . 10
              
            
   |
39 | 7, 12, 38 | syl2anc 391 |
. . . . . . . . 9
           
  
     
   
     |
40 | | eqeq12 2049 |
. . . . . . . . 9
       
  
     
    |
41 | 39, 40 | syl5ibrcom 146 |
. . . . . . . 8
           
  
     
 
 
         |
42 | 41 | expimpd 345 |
. . . . . . 7
   
           
    

     
      |
43 | 2, 42 | syl5bi 141 |
. . . . . 6
   
          
   
 
     
      |
44 | 43 | exlimdvv 1774 |
. . . . 5
   
            
         
          |
45 | 44 | exlimdvv 1774 |
. . . 4
   
                
         
          |
46 | 1, 45 | syl5bir 142 |
. . 3
   
            
                 
      |
47 | 46 | alrimivv 1752 |
. 2
   
                
                 
      |
48 | | eqeq1 2043 |
. . . . . 6
 
          |
49 | 48 | anbi2d 437 |
. . . . 5
         
       
 
     |
50 | 49 | 2exbidv 1745 |
. . . 4
             
           
       |
51 | | eceq1 6077 |
. . . . . . . 8
      |
52 | 51 | eqeq2d 2048 |
. . . . . . 7
 
      |
53 | | eceq1 6077 |
. . . . . . . 8
      |
54 | 53 | eqeq2d 2048 |
. . . . . . 7
 
      |
55 | 52, 54 | bi2anan9 538 |
. . . . . 6
 
    
          |
56 | | oveq12 5464 |
. . . . . . . 8
 
  
    |
57 | 56 | eceq1d 6078 |
. . . . . . 7
 
          |
58 | 57 | eqeq2d 2048 |
. . . . . 6
 
   
        |
59 | 55, 58 | anbi12d 442 |
. . . . 5
 
       
   
 
   
 
     |
60 | 59 | cbvex2v 1796 |
. . . 4
          
 
           
      |
61 | 50, 60 | syl6bb 185 |
. . 3
             
           
       |
62 | 61 | mo4 1958 |
. 2
          
                   
                 
      |
63 | 47, 62 | sylibr 137 |
1
   
            
        |