Step | Hyp | Ref
| Expression |
1 | | nntopi.n |
. 2
         |
2 | | eqeq2 2187 |
. . 3
                     
    
            
    
          |
3 | 2 | rexbidv 2478 |
. 2
  
                   
    
             
    
          |
4 | | eqeq2 2187 |
. . 3
                     
    
            
    
          |
5 | 4 | rexbidv 2478 |
. 2
  
                   
    
             
    
          |
6 | | eqeq2 2187 |
. . 3
                       
    
            
    
            |
7 | 6 | rexbidv 2478 |
. 2
    
                   
    
             
    
            |
8 | | eqeq2 2187 |
. . 3
                     
    
            
    
          |
9 | 8 | rexbidv 2478 |
. 2
  
                   
    
             
    
          |
10 | | 1pi 7316 |
. . 3
 |
11 | | eqid 2177 |
. . 3
 |
12 | | opeq1 3780 |
. . . . . . . . . . . . . . . . 17
   
     |
13 | 12 | eceq1d 6573 |
. . . . . . . . . . . . . . . 16
            |
14 | | df-1nqqs 7352 |
. . . . . . . . . . . . . . . 16
      |
15 | 13, 14 | eqtr4di 2228 |
. . . . . . . . . . . . . . 15
        |
16 | 15 | breq2d 4017 |
. . . . . . . . . . . . . 14
      
   |
17 | 16 | abbidv 2295 |
. . . . . . . . . . . . 13
       
   |
18 | 15 | breq1d 4015 |
. . . . . . . . . . . . . 14
          |
19 | 18 | abbidv 2295 |
. . . . . . . . . . . . 13
       

   |
20 | 17, 19 | opeq12d 3788 |
. . . . . . . . . . . 12
                          |
21 | | df-i1p 7468 |
. . . . . . . . . . . 12
        |
22 | 20, 21 | eqtr4di 2228 |
. . . . . . . . . . 11
                   |
23 | 22 | oveq1d 5892 |
. . . . . . . . . 10
          
    
       |
24 | 23 | opeq1d 3786 |
. . . . . . . . 9
           
    
    
       |
25 | 24 | eceq1d 6573 |
. . . . . . . 8
            
    
              |
26 | | df-1r 7733 |
. . . . . . . 8
        |
27 | 25, 26 | eqtr4di 2228 |
. . . . . . 7
            
    
        |
28 | 27 | opeq1d 3786 |
. . . . . 6
             
    
            |
29 | | df-1 7821 |
. . . . . 6
    |
30 | 28, 29 | eqtr4di 2228 |
. . . . 5
             
    
         |
31 | 30 | eqeq1d 2186 |
. . . 4
                     
        |
32 | 31 | rspcev 2843 |
. . 3
 
                     
       |
33 | 10, 11, 32 | mp2an 426 |
. 2
             
    
        |
34 | | simplr 528 |
. . . . . . 7
  
             
    
          |
35 | | addclpi 7328 |
. . . . . . 7
    
  |
36 | 34, 10, 35 | sylancl 413 |
. . . . . 6
  
             
    
            |
37 | | pitonnlem2 7848 |
. . . . . . . 8
                     
                    
    
     
     |
38 | 34, 37 | syl 14 |
. . . . . . 7
  
             
    
                     
    
                      
    
     
     |
39 | | simpr 110 |
. . . . . . . 8
  
             
    
                    
    
         |
40 | 39 | oveq1d 5892 |
. . . . . . 7
  
             
    
                     
    
            |
41 | 38, 40 | eqtr3d 2212 |
. . . . . 6
  
             
    
                      
    
     
  
    |
42 | | opeq1 3780 |
. . . . . . . . . . . . . . . 16
     
       |
43 | 42 | eceq1d 6573 |
. . . . . . . . . . . . . . 15
                |
44 | 43 | breq2d 4017 |
. . . . . . . . . . . . . 14
        
    
    |
45 | 44 | abbidv 2295 |
. . . . . . . . . . . . 13
         
         |
46 | 43 | breq1d 4015 |
. . . . . . . . . . . . . 14
             
     |
47 | 46 | abbidv 2295 |
. . . . . . . . . . . . 13
         
           |
48 | 45, 47 | opeq12d 3788 |
. . . . . . . . . . . 12
                                         |
49 | 48 | oveq1d 5892 |
. . . . . . . . . . 11
            
    
     
                 
   |
50 | 49 | opeq1d 3786 |
. . . . . . . . . 10
             
    
    
            
    
     
   |
51 | 50 | eceq1d 6573 |
. . . . . . . . 9
              
    
                            
     |
52 | 51 | opeq1d 3786 |
. . . . . . . 8
               
    
                     
    
     
     |
53 | 52 | eqeq1d 2186 |
. . . . . . 7
                       
      
              
    
     
  
     |
54 | 53 | rspcev 2843 |
. . . . . 6
   
     
                 
                            
         |
55 | 36, 41, 54 | syl2anc 411 |
. . . . 5
  
             
    
                            
         |
56 | 55 | ex 115 |
. . . 4
 
              
    
       
                   
          |
57 | 56 | rexlimdva 2594 |
. . 3
  
                   
     
                   
          |
58 | | opeq1 3780 |
. . . . . . . . . . . . 13
   
     |
59 | 58 | eceq1d 6573 |
. . . . . . . . . . . 12
            |
60 | 59 | breq2d 4017 |
. . . . . . . . . . 11
      
       |
61 | 60 | abbidv 2295 |
. . . . . . . . . 10
       
       |
62 | 59 | breq1d 4015 |
. . . . . . . . . . 11
           
   |
63 | 62 | abbidv 2295 |
. . . . . . . . . 10
       
         |
64 | 61, 63 | opeq12d 3788 |
. . . . . . . . 9
                                   |
65 | 64 | oveq1d 5892 |
. . . . . . . 8
          
    
     
           
     |
66 | 65 | opeq1d 3786 |
. . . . . . 7
           
    
    
          
    
       |
67 | 66 | eceq1d 6573 |
. . . . . 6
            
    
                        
     |
68 | 67 | opeq1d 3786 |
. . . . 5
             
    
                   
    
         |
69 | 68 | eqeq1d 2186 |
. . . 4
                     
      
            
    
            |
70 | 69 | cbvrexv 2706 |
. . 3
       
           
        
             
    
           |
71 | 57, 70 | imbitrdi 161 |
. 2
  
                   
     
                   
          |
72 | 1, 3, 5, 7, 9, 33,
71 | nnindnn 7894 |
1
              
    
         |