Step | Hyp | Ref
| Expression |
1 | | rpnnen1.1 |
. . . 4
     |
2 | | rpnnen1.2 |
. . . 4
      
    |
3 | 1, 2 | rpnnen1lem3 11292 |
. . 3
         |
4 | 1, 2 | rpnnen1lem1 11290 |
. . . . . 6
         |
5 | | qex 11276 |
. . . . . . 7
 |
6 | | nnex 10615 |
. . . . . . 7
 |
7 | 5, 6 | elmap 7500 |
. . . . . 6
      
          |
8 | 4, 7 | sylib 200 |
. . . . 5
           |
9 | | frn 5735 |
. . . . . 6
            
  |
10 | | qssre 11274 |
. . . . . 6
 |
11 | 9, 10 | syl6ss 3444 |
. . . . 5
            
  |
12 | 8, 11 | syl 17 |
. . . 4
       |
13 | | 1nn 10620 |
. . . . . . . 8
 |
14 | 13 | ne0ii 3738 |
. . . . . . 7
 |
15 | | fdm 5733 |
. . . . . . . 8
               |
16 | 15 | neeq1d 2683 |
. . . . . . 7
             
   |
17 | 14, 16 | mpbiri 237 |
. . . . . 6
               |
18 | | dm0rn0 5051 |
. . . . . . 7
    
      |
19 | 18 | necon3bii 2676 |
. . . . . 6
    
      |
20 | 17, 19 | sylib 200 |
. . . . 5
               |
21 | 8, 20 | syl 17 |
. . . 4
       |
22 | | breq2 4406 |
. . . . . . 7
 
   |
23 | 22 | ralbidv 2827 |
. . . . . 6
  
    
         |
24 | 23 | rspcev 3150 |
. . . . 5
       
       
  |
25 | 3, 24 | mpdan 674 |
. . . 4
          |
26 | | id 22 |
. . . 4
   |
27 | | suprleub 10573 |
. . . 4
                                  
   |
28 | 12, 21, 25, 26, 27 | syl31anc 1271 |
. . 3
               
   |
29 | 3, 28 | mpbird 236 |
. 2
           |
30 | 1, 2 | rpnnen1lem4 11293 |
. . . . . . . . 9
           |
31 | | resubcl 9938 |
. . . . . . . . 9
                       |
32 | 30, 31 | mpdan 674 |
. . . . . . . 8
             |
33 | 32 | adantr 467 |
. . . . . . 7
                       |
34 | | posdif 10107 |
. . . . . . . . . 10
                                 |
35 | 30, 34 | mpancom 675 |
. . . . . . . . 9
                       |
36 | 35 | biimpa 487 |
. . . . . . . 8
                       |
37 | 36 | gt0ne0d 10178 |
. . . . . . 7
                       |
38 | 33, 37 | rereccld 10434 |
. . . . . 6
                         |
39 | | arch 10866 |
. . . . . 6
            
               |
40 | 38, 39 | syl 17 |
. . . . 5
                          |
41 | 40 | ex 436 |
. . . 4
         
                |
42 | 1, 2 | rpnnen1lem2 11291 |
. . . . . . . . 9
 
    
  |
43 | 42 | zred 11040 |
. . . . . . . 8
 
    
  |
44 | 43 | 3adant3 1028 |
. . . . . . 7
 
                   |
45 | 44 | ltp1d 10537 |
. . . . . 6
 
                         |
46 | 33, 36 | jca 535 |
. . . . . . . . . . . . 13
                                   |
47 | | nnre 10616 |
. . . . . . . . . . . . . 14
   |
48 | | nngt0 10638 |
. . . . . . . . . . . . . 14
   |
49 | 47, 48 | jca 535 |
. . . . . . . . . . . . 13
     |
50 | | ltrec1 10493 |
. . . . . . . . . . . . 13
                                                       |
51 | 46, 49, 50 | syl2an 480 |
. . . . . . . . . . . 12
                                         |
52 | 30 | ad2antrr 732 |
. . . . . . . . . . . . . 14
                       |
53 | | nnrecre 10646 |
. . . . . . . . . . . . . . 15
     |
54 | 53 | adantl 468 |
. . . . . . . . . . . . . 14
                 |
55 | | simpll 760 |
. . . . . . . . . . . . . 14
               |
56 | 52, 54, 55 | ltaddsub2d 10214 |
. . . . . . . . . . . . 13
                         
               |
57 | 12 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
       |
58 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . 19
               |
59 | 8, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
60 | | fnfvelrn 6019 |
. . . . . . . . . . . . . . . . . 18
     
               |
61 | 59, 60 | sylan 474 |
. . . . . . . . . . . . . . . . 17
 
               |
62 | 57, 61 | sseldd 3433 |
. . . . . . . . . . . . . . . 16
 
           |
63 | 30 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
           |
64 | 53 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
     |
65 | 12, 21, 25 | 3jca 1188 |
. . . . . . . . . . . . . . . . . 18
     
              |
66 | 65 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
                    |
67 | | suprub 10570 |
. . . . . . . . . . . . . . . . 17
                                       
          |
68 | 66, 61, 67 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
        
          |
69 | 62, 63, 64, 68 | leadd1dd 10227 |
. . . . . . . . . . . . . . 15
 
            
              |
70 | 62, 64 | readdcld 9670 |
. . . . . . . . . . . . . . . 16
 
               |
71 | | readdcl 9622 |
. . . . . . . . . . . . . . . . 17
                           |
72 | 30, 53, 71 | syl2an 480 |
. . . . . . . . . . . . . . . 16
 
               |
73 | | simpl 459 |
. . . . . . . . . . . . . . . 16
 
   |
74 | | lelttr 9724 |
. . . . . . . . . . . . . . . . 17
                                                                                 |
75 | 74 | expd 438 |
. . . . . . . . . . . . . . . 16
                                       
           
            
                |
76 | 70, 72, 73, 75 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
 
                                                       |
77 | 69, 76 | mpd 15 |
. . . . . . . . . . . . . 14
 
                             |
78 | 77 | adantlr 721 |
. . . . . . . . . . . . 13
                                         |
79 | 56, 78 | sylbird 239 |
. . . . . . . . . . . 12
               
         
               |
80 | 51, 79 | sylbid 219 |
. . . . . . . . . . 11
                         
               |
81 | 42 | peano2zd 11043 |
. . . . . . . . . . . . . . . 16
 
         |
82 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . 19
    
              |
83 | 82 | breq1d 4412 |
. . . . . . . . . . . . . . . . . 18
    
                |
84 | 83, 1 | elrab2 3198 |
. . . . . . . . . . . . . . . . 17
     
             
 
   |
85 | 84 | biimpri 210 |
. . . . . . . . . . . . . . . 16
             
 
         |
86 | 81, 85 | sylan 474 |
. . . . . . . . . . . . . . 15
                     |
87 | | ssrab2 3514 |
. . . . . . . . . . . . . . . . . . . 20
     |
88 | 1, 87 | eqsstri 3462 |
. . . . . . . . . . . . . . . . . . 19
 |
89 | | zssre 10944 |
. . . . . . . . . . . . . . . . . . 19
 |
90 | 88, 89 | sstri 3441 |
. . . . . . . . . . . . . . . . . 18
 |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 

  |
92 | | remulcl 9624 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
93 | 92 | ancoms 455 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
94 | 47, 93 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
95 | | btwnz 11037 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  
     |
96 | 95 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . 21
        |
97 | 94, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
98 | | zre 10941 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
99 | 98 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
100 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
101 | 49 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
102 | | ltdivmul 10480 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
     |
103 | 99, 100, 101, 102 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
       
     |
104 | 103 | rexbidva 2898 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
105 | 97, 104 | mpbird 236 |
. . . . . . . . . . . . . . . . . . 19
 
  

  |
106 | | rabn0 3752 |
. . . . . . . . . . . . . . . . . . 19
   
  

  |
107 | 105, 106 | sylibr 216 |
. . . . . . . . . . . . . . . . . 18
 
       |
108 | 1 | neeq1i 2688 |
. . . . . . . . . . . . . . . . . 18
       |
109 | 107, 108 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
 
   |
110 | 1 | rabeq2i 3042 |
. . . . . . . . . . . . . . . . . . . 20

      |
111 | 47 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
112 | 111, 100,
92 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
113 | | ltle 9722 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
     |
114 | 99, 112, 113 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . 22
       
     |
115 | 103, 114 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . . 21
       
     |
116 | 115 | impr 625 |
. . . . . . . . . . . . . . . . . . . 20
             |
117 | 110, 116 | sylan2b 478 |
. . . . . . . . . . . . . . . . . . 19
    
    |
118 | 117 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . 18
 
      |
119 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
120 | 119 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . 19
    

     |
121 | 120 | rspcev 3150 |
. . . . . . . . . . . . . . . . . 18
        
   |
122 | 94, 118, 121 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
     |
123 | 91, 109, 122 | 3jca 1188 |
. . . . . . . . . . . . . . . 16
 
  

   |
124 | | suprub 10570 |
. . . . . . . . . . . . . . . 16
   

           
     
  |
125 | 123, 124 | sylan 474 |
. . . . . . . . . . . . . . 15
       
               |
126 | 86, 125 | syldan 473 |
. . . . . . . . . . . . . 14
                         |
127 | 126 | ex 436 |
. . . . . . . . . . . . 13
 
               
  
    |
128 | 42 | zcnd 11041 |
. . . . . . . . . . . . . . . 16
 
    
  |
129 | | 1cnd 9659 |
. . . . . . . . . . . . . . . 16
 
   |
130 | | nncn 10617 |
. . . . . . . . . . . . . . . . . 18
   |
131 | | nnne0 10642 |
. . . . . . . . . . . . . . . . . 18
   |
132 | 130, 131 | jca 535 |
. . . . . . . . . . . . . . . . 17
     |
133 | 132 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
     |
134 | | divdir 10293 |
. . . . . . . . . . . . . . . 16
     
       
       
       |
135 | 128, 129,
133, 134 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
 
     
       
       |
136 | 6 | mptex 6136 |
. . . . . . . . . . . . . . . . . . 19
         |
137 | 2 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . . . 19
       
           
     |
138 | 136, 137 | mpan2 677 |
. . . . . . . . . . . . . . . . . 18
         
     |
139 | 138 | fveq1d 5867 |
. . . . . . . . . . . . . . . . 17
                       |
140 | | ovex 6318 |
. . . . . . . . . . . . . . . . . 18
       |
141 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
             
   |
142 | 141 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . . 18
      
                      |
143 | 140, 142 | mpan2 677 |
. . . . . . . . . . . . . . . . 17
       
         
   |
144 | 139, 143 | sylan9eq 2505 |
. . . . . . . . . . . . . . . 16
 
                 |
145 | 144 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
 
                  
      |
146 | 135, 145 | eqtr4d 2488 |
. . . . . . . . . . . . . 14
 
     
                 |
147 | 146 | breq1d 4412 |
. . . . . . . . . . . . 13
 
         
               |
148 | 81 | zred 11040 |
. . . . . . . . . . . . . 14
 
         |
149 | 148, 43 | lenltd 9781 |
. . . . . . . . . . . . 13
 
     
     
  
          |
150 | 127, 147,
149 | 3imtr3d 271 |
. . . . . . . . . . . 12
 
                     
     |
151 | 150 | adantlr 721 |
. . . . . . . . . . 11
                             
         |
152 | 80, 151 | syld 45 |
. . . . . . . . . 10
                         
  
          |
153 | 152 | exp31 609 |
. . . . . . . . 9
         

            
  
            |
154 | 153 | com4l 87 |
. . . . . . . 8
        

            

  
            |
155 | 154 | com14 91 |
. . . . . . 7
              
                
       |
156 | 155 | 3imp 1202 |
. . . . . 6
 
                     
  
          |
157 | 45, 156 | mt2d 121 |
. . . . 5
 
                       |
158 | 157 | rexlimdv3a 2881 |
. . . 4
  
           
           |
159 | 41, 158 | syld 45 |
. . 3
         
           |
160 | 159 | pm2.01d 173 |
. 2
           |
161 | | eqlelt 9721 |
. . 3
                   
        
            |
162 | 30, 161 | mpancom 675 |
. 2
         
        
            |
163 | 29, 160, 162 | mpbir2and 933 |
1
           |