Step | Hyp | Ref
| Expression |
1 | | iftrue 3878 |
. . . . . . . . 9
    
                 |
2 | 1 | adantl 473 |
. . . . . . . 8
  
               
     |
3 | | 0ex 4528 |
. . . . . . . . . . 11
 |
4 | 3 | snid 3988 |
. . . . . . . . . 10
   |
5 | | elun2 3593 |
. . . . . . . . . 10
         |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
     |
7 | 6 | a1i 11 |
. . . . . . . 8
  
          |
8 | 2, 7 | eqeltrd 2549 |
. . . . . . 7
  
               
         |
9 | 8 | adantll 728 |
. . . . . 6
                    
         |
10 | | iffalse 3881 |
. . . . . . . 8
                
           |
11 | 10 | adantl 473 |
. . . . . . 7
    
               
           |
12 | | nnfoctbdjlem.g |
. . . . . . . . . . . 12
       |
13 | | f1of 5828 |
. . . . . . . . . . . 12
    
      |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
       |
15 | 14 | adantr 472 |
. . . . . . . . . 10
 
           |
16 | | pm2.46 405 |
. . . . . . . . . . . 12
         |
17 | | notnot2 116 |
. . . . . . . . . . . 12
       |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
         |
19 | 18 | adantl 473 |
. . . . . . . . . 10
 
         |
20 | 15, 19 | ffvelrnd 6038 |
. . . . . . . . 9
 
             |
21 | 20 | adantlr 729 |
. . . . . . . 8
    
            |
22 | | elun1 3592 |
. . . . . . . 8
                   |
23 | 21, 22 | syl 17 |
. . . . . . 7
    
                |
24 | 11, 23 | eqeltrd 2549 |
. . . . . 6
    
               
         |
25 | 9, 24 | pm2.61dan 808 |
. . . . 5
 

                     |
26 | | nnfoctbdjlem.f |
. . . . 5
            
     |
27 | 25, 26 | fmptd 6061 |
. . . 4
           |
28 | | simpr 468 |
. . . . . . . . . . 11
 
   |
29 | | f1ofo 5835 |
. . . . . . . . . . . . . 14
    
      |
30 | | forn 5809 |
. . . . . . . . . . . . . 14
       |
31 | 12, 29, 30 | 3syl 18 |
. . . . . . . . . . . . 13
   |
32 | 31 | eqcomd 2477 |
. . . . . . . . . . . 12
   |
33 | 32 | adantr 472 |
. . . . . . . . . . 11
 
   |
34 | 28, 33 | eleqtrd 2551 |
. . . . . . . . . 10
 
   |
35 | 14 | ffnd 5740 |
. . . . . . . . . . . 12
   |
36 | | fvelrnb 5926 |
. . . . . . . . . . . 12
          |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
  
       |
38 | 37 | adantr 472 |
. . . . . . . . . 10
 
          |
39 | 34, 38 | mpbid 215 |
. . . . . . . . 9
 
 
      |
40 | | nnfoctbdjlem.a |
. . . . . . . . . . . . . . . 16

  |
41 | 40 | sselda 3418 |
. . . . . . . . . . . . . . 15
 
   |
42 | | peano2nn 10643 |
. . . . . . . . . . . . . . 15
     |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
 
     |
44 | 43 | 3adant3 1050 |
. . . . . . . . . . . . 13
 
    
    |
45 | 26 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
                    |
46 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
47 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
48 | 41 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
49 | 47, 48 | ltaddrp2d 11395 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
50 | 49 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
    |
51 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
52 | 51 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
53 | 52 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
54 | 50, 53 | breqtrd 4420 |
. . . . . . . . . . . . . . . . . . . . . 22
      
  |
55 | 46, 54 | gtned 9787 |
. . . . . . . . . . . . . . . . . . . . 21
         |
56 | 55 | neneqd 2648 |
. . . . . . . . . . . . . . . . . . . 20
      
  |
57 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
58 | 57 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
59 | 41 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
60 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
61 | 59, 60 | pncand 10006 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
62 | 61 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
63 | 58, 62 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
64 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
65 | 63, 64 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . 21
           |
66 | 65 | notnotd 128 |
. . . . . . . . . . . . . . . . . . . 20
           |
67 | 56, 66 | jca 541 |
. . . . . . . . . . . . . . . . . . 19
        
    |
68 | | ioran 498 |
. . . . . . . . . . . . . . . . . . 19
    

     |
69 | 67, 68 | sylibr 217 |
. . . . . . . . . . . . . . . . . 18
             |
70 | 69 | iffalsed 3883 |
. . . . . . . . . . . . . . . . 17
                  
           |
71 | 63 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
                   |
72 | 70, 71 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
                  
         |
73 | 14 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . 16
 
       |
74 | 45, 72, 43, 73 | fvmptd 5969 |
. . . . . . . . . . . . . . 15
 
             |
75 | 74 | 3adant3 1050 |
. . . . . . . . . . . . . 14
 
    
            |
76 | | simp3 1032 |
. . . . . . . . . . . . . 14
 
    
      |
77 | 75, 76 | eqtrd 2505 |
. . . . . . . . . . . . 13
 
    
        |
78 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
               |
79 | 78 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
       
         |
80 | 79 | rspcev 3136 |
. . . . . . . . . . . . 13
           
      |
81 | 44, 77, 80 | syl2anc 673 |
. . . . . . . . . . . 12
 
    
       |
82 | 81 | 3exp 1230 |
. . . . . . . . . . 11
                |
83 | 82 | adantr 472 |
. . . . . . . . . 10
 
                |
84 | 83 | rexlimdv 2870 |
. . . . . . . . 9
 
  
            |
85 | 39, 84 | mpd 15 |
. . . . . . . 8
 
        |
86 | | id 22 |
. . . . . . . . . . 11
           |
87 | 86 | eqcomd 2477 |
. . . . . . . . . 10
           |
88 | 87 | a1i 11 |
. . . . . . . . 9
                 |
89 | 88 | reximdva 2858 |
. . . . . . . 8
 
  
            |
90 | 85, 89 | mpd 15 |
. . . . . . 7
 
        |
91 | 90 | adantlr 729 |
. . . . . 6
       
 
      |
92 | | simpll 768 |
. . . . . . 7
       

  |
93 | | elunnel1 3566 |
. . . . . . . . 9
           |
94 | | elsni 3985 |
. . . . . . . . 9
     |
95 | 93, 94 | syl 17 |
. . . . . . . 8
         |
96 | 95 | adantll 728 |
. . . . . . 7
       

  |
97 | | 1nn 10642 |
. . . . . . . . 9
 |
98 | 97 | a1i 11 |
. . . . . . . 8
 

  |
99 | 26 | a1i 11 |
. . . . . . . . . . 11
                    |
100 | 1 | orcs 401 |
. . . . . . . . . . . 12
            
     |
101 | 100 | adantl 473 |
. . . . . . . . . . 11
 
            
     |
102 | 97 | a1i 11 |
. . . . . . . . . . 11
   |
103 | 3 | a1i 11 |
. . . . . . . . . . 11

  |
104 | 99, 101, 102, 103 | fvmptd 5969 |
. . . . . . . . . 10
       |
105 | 104 | adantr 472 |
. . . . . . . . 9
 

      |
106 | | id 22 |
. . . . . . . . . . 11

  |
107 | 106 | eqcomd 2477 |
. . . . . . . . . 10

  |
108 | 107 | adantl 473 |
. . . . . . . . 9
 

  |
109 | 105, 108 | eqtr2d 2506 |
. . . . . . . 8
 

      |
110 | | fveq2 5879 |
. . . . . . . . . 10
           |
111 | 110 | eqeq2d 2481 |
. . . . . . . . 9
     
       |
112 | 111 | rspcev 3136 |
. . . . . . . 8
 
     
      |
113 | 98, 109, 112 | syl2anc 673 |
. . . . . . 7
 

       |
114 | 92, 96, 113 | syl2anc 673 |
. . . . . 6
       

       |
115 | 91, 114 | pm2.61dan 808 |
. . . . 5
 

           |
116 | 115 | ralrimiva 2809 |
. . . 4
              |
117 | 27, 116 | jca 541 |
. . 3
      
                 |
118 | | dffo3 6052 |
. . 3
              
                 |
119 | 117, 118 | sylibr 217 |
. 2
     
     |
120 | | orc 392 |
. . . . . 6
               |
121 | 120 | adantl 473 |
. . . . 5
   
 
               |
122 | | simpl 464 |
. . . . . 6
   
 
       |
123 | | neqne 2651 |
. . . . . . 7
   |
124 | 123 | adantl 473 |
. . . . . 6
   
 
   |
125 | | simpl 464 |
. . . . . . . . . . . . . 14
  
      |
126 | 2, 3 | syl6eqel 2557 |
. . . . . . . . . . . . . 14
  
               
     |
127 | 26 | fvmpt2 5972 |
. . . . . . . . . . . . . 14
             
           
             |
128 | 125, 126,
127 | syl2anc 673 |
. . . . . . . . . . . . 13
  
           
             |
129 | 128, 2 | eqtrd 2505 |
. . . . . . . . . . . 12
  
          |
130 | 129 | ineq1d 3624 |
. . . . . . . . . . 11
  
        
     
       |
131 | | 0in 37452 |
. . . . . . . . . . . 12
       |
132 | 131 | a1i 11 |
. . . . . . . . . . 11
  
            |
133 | 130, 132 | eqtrd 2505 |
. . . . . . . . . 10
  
        
       |
134 | 133 | adantlr 729 |
. . . . . . . . 9
                     |
135 | 134 | ad4ant24 1264 |
. . . . . . . 8
    
            
       |
136 | 26 | a1i 11 |
. . . . . . . . . . . . . . 15
  
                       |
137 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . 18
     |
138 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . 20
       |
139 | 138 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . 19
   
     |
140 | 139 | notbid 301 |
. . . . . . . . . . . . . . . . . 18
   
     |
141 | 137, 140 | orbi12d 724 |
. . . . . . . . . . . . . . . . 17
     
 
     |
142 | | eqidd 2472 |
. . . . . . . . . . . . . . . . 17
   |
143 | 138 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
          
    |
144 | 141, 142,
143 | ifbieq12d 3899 |
. . . . . . . . . . . . . . . 16
            
      
             |
145 | 144 | adantl 473 |
. . . . . . . . . . . . . . 15
       
    
                            |
146 | | simpl 464 |
. . . . . . . . . . . . . . 15
  
      |
147 | | iftrue 3878 |
. . . . . . . . . . . . . . . . 17
    
                 |
148 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    
  |
149 | 147, 148 | eqeltrd 2549 |
. . . . . . . . . . . . . . . 16
    
                 |
150 | 149 | adantl 473 |
. . . . . . . . . . . . . . 15
  
               
     |
151 | 136, 145,
146, 150 | fvmptd 5969 |
. . . . . . . . . . . . . 14
  
           
             |
152 | 147 | adantl 473 |
. . . . . . . . . . . . . 14
  
               
     |
153 | 151, 152 | eqtrd 2505 |
. . . . . . . . . . . . 13
  
          |
154 | 153 | ineq2d 3625 |
. . . . . . . . . . . 12
  
        
             |
155 | | in0 3763 |
. . . . . . . . . . . . 13
       |
156 | 155 | a1i 11 |
. . . . . . . . . . . 12
  
        
   |
157 | 154, 156 | eqtrd 2505 |
. . . . . . . . . . 11
  
        
       |
158 | 157 | adantll 728 |
. . . . . . . . . 10
                     |
159 | 158 | ad5ant25 1272 |
. . . . . . . . 9
         
             
       |
160 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
161 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . 19
       |
162 | 3, 161 | ifex 3940 |
. . . . . . . . . . . . . . . . . 18
                |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . 17
            
     |
164 | 160, 163,
127 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
        
             |
165 | 164 | adantr 472 |
. . . . . . . . . . . . . . 15
                            |
166 | 10 | adantl 473 |
. . . . . . . . . . . . . . 15
                  
           |
167 | 165, 166 | eqtrd 2505 |
. . . . . . . . . . . . . 14
                   |
168 | 167 | adantlr 729 |
. . . . . . . . . . . . 13
     
  
            |
169 | 168 | 3adant3 1050 |
. . . . . . . . . . . 12
     
   
  
            |
170 | 26 | a1i 11 |
. . . . . . . . . . . . . . 15
      
                   |
171 | 144 | adantl 473 |
. . . . . . . . . . . . . . . 16
        
                          
     |
172 | | iffalse 3881 |
. . . . . . . . . . . . . . . . 17
                
           |
173 | 172 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
        
                       |
174 | 171, 173 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
        
                       |
175 | | simpl 464 |
. . . . . . . . . . . . . . 15
      
  |
176 | | fvex 5889 |
. . . . . . . . . . . . . . . 16
       |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . 15
               |
178 | 170, 174,
175, 177 | fvmptd 5969 |
. . . . . . . . . . . . . 14
                   |
179 | 178 | adantll 728 |
. . . . . . . . . . . . 13
     
  
            |
180 | 179 | 3adant2 1049 |
. . . . . . . . . . . 12
     
   
  
            |
181 | 169, 180 | ineq12d 3626 |
. . . . . . . . . . 11
     
   
  
                          |
182 | 181 | ad5ant245 1273 |
. . . . . . . . . 10
         
    
        
         
           |
183 | 18 | ad2antlr 741 |
. . . . . . . . . . . . . 14
         
    
        |
184 | | pm2.46 405 |
. . . . . . . . . . . . . . . 16
         |
185 | 184 | notnotrd 117 |
. . . . . . . . . . . . . . 15
         |
186 | 185 | adantl 473 |
. . . . . . . . . . . . . 14
         
    
        |
187 | | f1of1 5827 |
. . . . . . . . . . . . . . . . . . 19
    
      |
188 | 12, 187 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
189 | | dff14a 6188 |
. . . . . . . . . . . . . . . . . 18
    
     

             |
190 | 188, 189 | sylib 201 |
. . . . . . . . . . . . . . . . 17
        
            |
191 | 190 | simprd 470 |
. . . . . . . . . . . . . . . 16
  

           |
192 | 191 | adantr 472 |
. . . . . . . . . . . . . . 15
 
   


           |
193 | 192 | ad3antrrr 744 |
. . . . . . . . . . . . . 14
         
    
    


           |
194 | 183, 186,
193 | jca31 543 |
. . . . . . . . . . . . 13
         
    
             
            |
195 | | nncn 10639 |
. . . . . . . . . . . . . . . . 17
   |
196 | 195 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
   |
197 | 196 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
   
 
   |
198 | | nncn 10639 |
. . . . . . . . . . . . . . . . 17
   |
199 | 198 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
   |
200 | 199 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
   
 
   |
201 | | 1cnd 9677 |
. . . . . . . . . . . . . . 15
   
 
   |
202 | | simpr 468 |
. . . . . . . . . . . . . . 15
   
 
   |
203 | 197, 200,
201, 202 | subneintr2d 10051 |
. . . . . . . . . . . . . 14
   
 
       |
204 | 203 | ad2antrr 740 |
. . . . . . . . . . . . 13
         
    
          |
205 | | neeq1 2705 |
. . . . . . . . . . . . . . 15
   
     |
206 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
          
    |
207 | 206 | neeq1d 2702 |
. . . . . . . . . . . . . . 15
           
             |
208 | 205, 207 | imbi12d 327 |
. . . . . . . . . . . . . 14
                               |
209 | | neeq2 2706 |
. . . . . . . . . . . . . . 15
     
       |
210 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
          
    |
211 | 210 | neeq2d 2703 |
. . . . . . . . . . . . . . 15
             
               |
212 | 209, 211 | imbi12d 327 |
. . . . . . . . . . . . . 14
                          
            |
213 | 208, 212 | rspc2va 3148 |
. . . . . . . . . . . . 13
          
                              |
214 | 194, 204,
213 | sylc 61 |
. . . . . . . . . . . 12
         
    
             
    |
215 | 214 | neneqd 2648 |
. . . . . . . . . . 11
         
    
             
    |
216 | 20 | ad4ant13 1258 |
. . . . . . . . . . . . 13
    
       
            |
217 | | simpl 464 |
. . . . . . . . . . . . . . 15
 
       |
218 | 185 | adantl 473 |
. . . . . . . . . . . . . . 15
 
         |
219 | 14 | ffvelrnda 6037 |
. . . . . . . . . . . . . . 15
 
           |
220 | 217, 218,
219 | syl2anc 673 |
. . . . . . . . . . . . . 14
 
             |
221 | 220 | ad4ant14 1259 |
. . . . . . . . . . . . 13
    
       
            |
222 | | nnfoctbdjlem.dj |
. . . . . . . . . . . . . . 15
 Disj
  |
223 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
224 | 223 | disjor 4380 |
. . . . . . . . . . . . . . 15
Disj




    |
225 | 222, 224 | sylib 201 |
. . . . . . . . . . . . . 14
  
      |
226 | 225 | ad3antrrr 744 |
. . . . . . . . . . . . 13
    
       
    



    |
227 | | eqeq1 2475 |
. . . . . . . . . . . . . . 15
    
  
         |
228 | | ineq1 3618 |
. . . . . . . . . . . . . . . 16
    
  
           |
229 | 228 | eqeq1d 2473 |
. . . . . . . . . . . . . . 15
    
    
           |
230 | 227, 229 | orbi12d 724 |
. . . . . . . . . . . . . 14
    
           
              |
231 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
    
        
               |
232 | | ineq2 3619 |
. . . . . . . . . . . . . . . 16
    
                          |
233 | 232 | eqeq1d 2473 |
. . . . . . . . . . . . . . 15
    
       
  
          
      |
234 | 231, 233 | orbi12d 724 |
. . . . . . . . . . . . . 14
    
       
               
                          |
235 | 230, 234 | rspc2va 3148 |
. . . . . . . . . . . . 13
      
                                 
            |
236 | 216, 221,
226, 235 | syl21anc 1291 |
. . . . . . . . . . . 12
    
       
                     
            |
237 | 236 | adantllr 733 |
. . . . . . . . . . 11
         
    
                     
            |
238 | | orel1 389 |
. . . . . . . . . . 11
                                     
   
          
      |
239 | 215, 237,
238 | sylc 61 |
. . . . . . . . . 10
         
    
                    |
240 | 182, 239 | eqtrd 2505 |
. . . . . . . . 9
         
    
        
       |
241 | 159, 240 | pm2.61dan 808 |
. . . . . . . 8
    
   
        
       |
242 | 135, 241 | pm2.61dan 808 |
. . . . . . 7
   
 
     
       |
243 | | olc 391 |
. . . . . . 7
     
                   |
244 | 242, 243 | syl 17 |
. . . . . 6
   
 
               |
245 | 122, 124,
244 | syl2anc 673 |
. . . . 5
   
 
               |
246 | 121, 245 | pm2.61dan 808 |
. . . 4
 
                 |
247 | 246 | ralrimivva 2814 |
. . 3
                 |
248 | | fveq2 5879 |
. . . 4
           |
249 | 248 | disjor 4380 |
. . 3
Disj    
                |
250 | 247, 249 | sylibr 217 |
. 2
 Disj
      |
251 | | nnex 10637 |
. . . . 5
 |
252 | 251 | mptex 6152 |
. . . 4
                  |
253 | 26, 252 | eqeltri 2545 |
. . 3
 |
254 | | foeq1 5802 |
. . . 4
      
       
      |
255 | | simpl 464 |
. . . . . 6
 
   |
256 | 255 | fveq1d 5881 |
. . . . 5
 
           |
257 | 256 | disjeq2dv 4371 |
. . . 4
 Disj    
Disj        |
258 | 254, 257 | anbi12d 725 |
. . 3
           Disj     
         Disj         |
259 | 253, 258 | spcev 3127 |
. 2
      
   Disj     
           Disj        |
260 | 119, 250,
259 | syl2anc 673 |
1
            Disj        |