Step | Hyp | Ref
| Expression |
1 | | opeq1 3540 |
. . . . . . . . . . . . . . 15
         |
2 | 1 | eceq1d 6078 |
. . . . . . . . . . . . . 14
            |
3 | 2 | breq2d 3767 |
. . . . . . . . . . . . 13
              |
4 | 3 | abbidv 2152 |
. . . . . . . . . . . 12
               |
5 | 2 | breq1d 3765 |
. . . . . . . . . . . . 13
               |
6 | 5 | abbidv 2152 |
. . . . . . . . . . . 12
 
               |
7 | 4, 6 | opeq12d 3548 |
. . . . . . . . . . 11
         
               
         |
8 | 7 | oveq1d 5470 |
. . . . . . . . . 10
          
                 
          |
9 | 8 | opeq1d 3546 |
. . . . . . . . 9
           
                           
     |
10 | 9 | eceq1d 6078 |
. . . . . . . 8
     
                      
                   |
11 | 10 | opeq1d 3546 |
. . . . . . 7
      
                               
              |
12 | 11 | eleq1d 2103 |
. . . . . 6
                     
                 
               |
13 | 12 | imbi2d 219 |
. . . . 5
                    
                                      
         |
14 | | opeq1 3540 |
. . . . . . . . . . . . . . 15
         |
15 | 14 | eceq1d 6078 |
. . . . . . . . . . . . . 14
            |
16 | 15 | breq2d 3767 |
. . . . . . . . . . . . 13
              |
17 | 16 | abbidv 2152 |
. . . . . . . . . . . 12
               |
18 | 15 | breq1d 3765 |
. . . . . . . . . . . . 13
               |
19 | 18 | abbidv 2152 |
. . . . . . . . . . . 12
 
               |
20 | 17, 19 | opeq12d 3548 |
. . . . . . . . . . 11
         
               
         |
21 | 20 | oveq1d 5470 |
. . . . . . . . . 10
          
                 
          |
22 | 21 | opeq1d 3546 |
. . . . . . . . 9
           
                           
     |
23 | 22 | eceq1d 6078 |
. . . . . . . 8
     
                      
                   |
24 | 23 | opeq1d 3546 |
. . . . . . 7
      
                               
              |
25 | 24 | eleq1d 2103 |
. . . . . 6
                     
                 
               |
26 | 25 | imbi2d 219 |
. . . . 5
                    
                                      
         |
27 | | opeq1 3540 |
. . . . . . . . . . . . . . 15
             |
28 | 27 | eceq1d 6078 |
. . . . . . . . . . . . . 14
                |
29 | 28 | breq2d 3767 |
. . . . . . . . . . . . 13
                  |
30 | 29 | abbidv 2152 |
. . . . . . . . . . . 12
                   |
31 | 28 | breq1d 3765 |
. . . . . . . . . . . . 13
                   |
32 | 31 | abbidv 2152 |
. . . . . . . . . . . 12
   
                 |
33 | 30, 32 | opeq12d 3548 |
. . . . . . . . . . 11
           
                 
    
      |
34 | 33 | oveq1d 5470 |
. . . . . . . . . 10
            
                   
    
       |
35 | 34 | opeq1d 3546 |
. . . . . . . . 9
             
                               
     |
36 | 35 | eceq1d 6078 |
. . . . . . . 8
       
                      
                 
     |
37 | 36 | opeq1d 3546 |
. . . . . . 7
        
                                 
    
     
     |
38 | 37 | eleq1d 2103 |
. . . . . 6
                       
                   
    
     
  
   |
39 | 38 | imbi2d 219 |
. . . . 5
                      
                                          
         |
40 | | opeq1 3540 |
. . . . . . . . . . . . . . 15
         |
41 | 40 | eceq1d 6078 |
. . . . . . . . . . . . . 14
            |
42 | 41 | breq2d 3767 |
. . . . . . . . . . . . 13
              |
43 | 42 | abbidv 2152 |
. . . . . . . . . . . 12
               |
44 | 41 | breq1d 3765 |
. . . . . . . . . . . . 13
               |
45 | 44 | abbidv 2152 |
. . . . . . . . . . . 12
 
               |
46 | 43, 45 | opeq12d 3548 |
. . . . . . . . . . 11
         
               
         |
47 | 46 | oveq1d 5470 |
. . . . . . . . . 10
          
                 
          |
48 | 47 | opeq1d 3546 |
. . . . . . . . 9
           
                           
     |
49 | 48 | eceq1d 6078 |
. . . . . . . 8
     
                      
                   |
50 | 49 | opeq1d 3546 |
. . . . . . 7
      
                               
              |
51 | 50 | eleq1d 2103 |
. . . . . 6
                     
                 
               |
52 | 51 | imbi2d 219 |
. . . . 5
                    
                                      
         |
53 | | pitonnlem1 6741 |
. . . . . . . 8
            
             |
54 | 53 | eleq1i 2100 |
. . . . . . 7
      
                     |
55 | 54 | biimpri 124 |
. . . . . 6
      
                     |
56 | 55 | adantr 261 |
. . . . 5
                         
       |
57 | | oveq1 5462 |
. . . . . . . . . . 11
             
                                  
        |
58 | 57 | eleq1d 2103 |
. . . . . . . . . 10
             
                            
                |
59 | 58 | rspccv 2647 |
. . . . . . . . 9
 

                     
                  
                |
60 | 59 | ad2antll 460 |
. . . . . . . 8
              
                                       
         |
61 | | pitonnlem2 6743 |
. . . . . . . . . 10
                     
                    
    
     
     |
62 | 61 | eleq1d 2103 |
. . . . . . . . 9
               
                           
    
     
  
   |
63 | 62 | adantr 261 |
. . . . . . . 8
                             
                    
    
     
  
   |
64 | 60, 63 | sylibd 138 |
. . . . . . 7
              
                        
                 
        |
65 | 64 | ex 108 |
. . . . . 6
                    
                 
                 
         |
66 | 65 | a2d 23 |
. . . . 5
                    
                                 
    
     
  
    |
67 | 13, 26, 39, 52, 56, 66 | indpi 6326 |
. . . 4
                   
               |
68 | 67 | alrimiv 1751 |
. . 3
     
        
                      |
69 | | eleq2 2098 |
. . . . 5
     |
70 | | eleq2 2098 |
. . . . . 6
  

     |
71 | 70 | raleqbi1dv 2507 |
. . . . 5
  



     |
72 | 69, 71 | anbi12d 442 |
. . . 4
    

         |
73 | 72 | ralab 2695 |
. . 3
 
   

               
                                
               |
74 | 68, 73 | sylibr 137 |
. 2
 
   

               
              |
75 | | nnprlu 6534 |
. . . . . . 7
         
         |
76 | | 1pr 6535 |
. . . . . . 7
 |
77 | | addclpr 6520 |
. . . . . . 7
          
      

         
          |
78 | 75, 76, 77 | sylancl 392 |
. . . . . 6
          
          |
79 | | opelxpi 4319 |
. . . . . 6
    
                                 
  
    |
80 | 78, 76, 79 | sylancl 392 |
. . . . 5
           
              |
81 | | enrex 6665 |
. . . . . 6
 |
82 | 81 | ecelqsi 6096 |
. . . . 5
           
           
           
                 |
83 | 80, 82 | syl 14 |
. . . 4
     
                        |
84 | | 0r 6678 |
. . . 4
 |
85 | | opelxpi 4319 |
. . . 4
                    
                            
             |
86 | 83, 84, 85 | sylancl 392 |
. . 3
      
                           |
87 | | elintg 3614 |
. . 3
      
                                      
                

  
   

               
               |
88 | 86, 87 | syl 14 |
. 2
                     
         

  
   

               
               |
89 | 74, 88 | mpbird 156 |
1
      
                       

    |