Step | Hyp | Ref
| Expression |
1 | | iftrue 3887 |
. . . . . . . . 9
    
                 |
2 | 1 | adantl 468 |
. . . . . . . 8
  
               
     |
3 | | 0ex 4535 |
. . . . . . . . . . 11
 |
4 | 3 | snid 3996 |
. . . . . . . . . 10
   |
5 | | elun2 3602 |
. . . . . . . . . 10
         |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
     |
7 | 6 | a1i 11 |
. . . . . . . 8
  
          |
8 | 2, 7 | eqeltrd 2529 |
. . . . . . 7
  
               
         |
9 | 8 | adantll 720 |
. . . . . 6
                    
         |
10 | | iffalse 3890 |
. . . . . . . 8
                
           |
11 | 10 | adantl 468 |
. . . . . . 7
    
               
           |
12 | | nnfoctbdjlem.g |
. . . . . . . . . . . 12
       |
13 | | f1of 5814 |
. . . . . . . . . . . 12
    
      |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
       |
15 | 14 | adantr 467 |
. . . . . . . . . 10
 
           |
16 | | pm2.46 400 |
. . . . . . . . . . . 12
         |
17 | | notnot2 116 |
. . . . . . . . . . . 12
       |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
         |
19 | 18 | adantl 468 |
. . . . . . . . . 10
 
         |
20 | 15, 19 | ffvelrnd 6023 |
. . . . . . . . 9
 
             |
21 | 20 | adantlr 721 |
. . . . . . . 8
    
            |
22 | | elun1 3601 |
. . . . . . . 8
                   |
23 | 21, 22 | syl 17 |
. . . . . . 7
    
                |
24 | 11, 23 | eqeltrd 2529 |
. . . . . 6
    
               
         |
25 | 9, 24 | pm2.61dan 800 |
. . . . 5
 

                     |
26 | | nnfoctbdjlem.f |
. . . . 5
            
     |
27 | 25, 26 | fmptd 6046 |
. . . 4
           |
28 | | simpr 463 |
. . . . . . . . . . 11
 
   |
29 | | f1ofo 5821 |
. . . . . . . . . . . . . 14
    
      |
30 | | forn 5796 |
. . . . . . . . . . . . . 14
       |
31 | 12, 29, 30 | 3syl 18 |
. . . . . . . . . . . . 13
   |
32 | 31 | eqcomd 2457 |
. . . . . . . . . . . 12
   |
33 | 32 | adantr 467 |
. . . . . . . . . . 11
 
   |
34 | 28, 33 | eleqtrd 2531 |
. . . . . . . . . 10
 
   |
35 | 14 | ffnd 5729 |
. . . . . . . . . . . 12
   |
36 | | fvelrnb 5912 |
. . . . . . . . . . . 12
          |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
  
       |
38 | 37 | adantr 467 |
. . . . . . . . . 10
 
          |
39 | 34, 38 | mpbid 214 |
. . . . . . . . 9
 
 
      |
40 | | nnfoctbdjlem.a |
. . . . . . . . . . . . . . . 16

  |
41 | 40 | sselda 3432 |
. . . . . . . . . . . . . . 15
 
   |
42 | | peano2nn 10621 |
. . . . . . . . . . . . . . 15
     |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
 
     |
44 | 43 | 3adant3 1028 |
. . . . . . . . . . . . 13
 
    
    |
45 | 26 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
                    |
46 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
47 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
48 | 41 | nnrpd 11339 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
49 | 47, 48 | ltaddrp2d 11372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
50 | 49 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
    |
51 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
52 | 51 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
53 | 52 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
54 | 50, 53 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . . . 22
      
  |
55 | 46, 54 | gtned 9770 |
. . . . . . . . . . . . . . . . . . . . 21
         |
56 | 55 | neneqd 2629 |
. . . . . . . . . . . . . . . . . . . 20
      
  |
57 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
58 | 57 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
59 | 41 | nncnd 10625 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
60 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
61 | 59, 60 | pncand 9987 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
62 | 61 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
63 | 58, 62 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
64 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
65 | 63, 64 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . 21
           |
66 | | notnot 293 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
67 | 65, 66 | sylib 200 |
. . . . . . . . . . . . . . . . . . . 20
           |
68 | 56, 67 | jca 535 |
. . . . . . . . . . . . . . . . . . 19
        
    |
69 | | ioran 493 |
. . . . . . . . . . . . . . . . . . 19
    

     |
70 | 68, 69 | sylibr 216 |
. . . . . . . . . . . . . . . . . 18
             |
71 | 70 | iffalsed 3892 |
. . . . . . . . . . . . . . . . 17
                  
           |
72 | 63 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
                   |
73 | 71, 72 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
                  
         |
74 | 14 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . 16
 
       |
75 | 45, 73, 43, 74 | fvmptd 5954 |
. . . . . . . . . . . . . . 15
 
             |
76 | 75 | 3adant3 1028 |
. . . . . . . . . . . . . 14
 
    
            |
77 | | simp3 1010 |
. . . . . . . . . . . . . 14
 
    
      |
78 | 76, 77 | eqtrd 2485 |
. . . . . . . . . . . . 13
 
    
        |
79 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
               |
80 | 79 | eqeq1d 2453 |
. . . . . . . . . . . . . 14
       
         |
81 | 80 | rspcev 3150 |
. . . . . . . . . . . . 13
           
      |
82 | 44, 78, 81 | syl2anc 667 |
. . . . . . . . . . . 12
 
    
       |
83 | 82 | 3exp 1207 |
. . . . . . . . . . 11
                |
84 | 83 | adantr 467 |
. . . . . . . . . 10
 
                |
85 | 84 | rexlimdv 2877 |
. . . . . . . . 9
 
  
            |
86 | 39, 85 | mpd 15 |
. . . . . . . 8
 
        |
87 | | id 22 |
. . . . . . . . . . 11
           |
88 | 87 | eqcomd 2457 |
. . . . . . . . . 10
           |
89 | 88 | a1i 11 |
. . . . . . . . 9
                 |
90 | 89 | reximdva 2862 |
. . . . . . . 8
 
  
            |
91 | 86, 90 | mpd 15 |
. . . . . . 7
 
        |
92 | 91 | adantlr 721 |
. . . . . 6
       
 
      |
93 | | simpll 760 |
. . . . . . 7
       

  |
94 | | elunnel1 3575 |
. . . . . . . . 9
           |
95 | | elsni 3993 |
. . . . . . . . 9
     |
96 | 94, 95 | syl 17 |
. . . . . . . 8
         |
97 | 96 | adantll 720 |
. . . . . . 7
       

  |
98 | | 1nn 10620 |
. . . . . . . . 9
 |
99 | 98 | a1i 11 |
. . . . . . . 8
 

  |
100 | 26 | a1i 11 |
. . . . . . . . . . 11
                    |
101 | 1 | orcs 396 |
. . . . . . . . . . . 12
            
     |
102 | 101 | adantl 468 |
. . . . . . . . . . 11
 
            
     |
103 | 98 | a1i 11 |
. . . . . . . . . . 11
   |
104 | 3 | a1i 11 |
. . . . . . . . . . 11

  |
105 | 100, 102,
103, 104 | fvmptd 5954 |
. . . . . . . . . 10
       |
106 | 105 | adantr 467 |
. . . . . . . . 9
 

      |
107 | | id 22 |
. . . . . . . . . . 11

  |
108 | 107 | eqcomd 2457 |
. . . . . . . . . 10

  |
109 | 108 | adantl 468 |
. . . . . . . . 9
 

  |
110 | 106, 109 | eqtr2d 2486 |
. . . . . . . 8
 

      |
111 | | fveq2 5865 |
. . . . . . . . . 10
           |
112 | 111 | eqeq2d 2461 |
. . . . . . . . 9
     
       |
113 | 112 | rspcev 3150 |
. . . . . . . 8
 
     
      |
114 | 99, 110, 113 | syl2anc 667 |
. . . . . . 7
 

       |
115 | 93, 97, 114 | syl2anc 667 |
. . . . . 6
       

       |
116 | 92, 115 | pm2.61dan 800 |
. . . . 5
 

           |
117 | 116 | ralrimiva 2802 |
. . . 4
              |
118 | 27, 117 | jca 535 |
. . 3
      
                 |
119 | | dffo3 6037 |
. . 3
              
                 |
120 | 118, 119 | sylibr 216 |
. 2
     
     |
121 | | orc 387 |
. . . . . 6
               |
122 | 121 | adantl 468 |
. . . . 5
   
 
               |
123 | | simpl 459 |
. . . . . 6
   
 
       |
124 | | neqne 37374 |
. . . . . . 7
   |
125 | 124 | adantl 468 |
. . . . . 6
   
 
   |
126 | | simpl 459 |
. . . . . . . . . . . . . 14
  
      |
127 | 2, 3 | syl6eqel 2537 |
. . . . . . . . . . . . . 14
  
               
     |
128 | 26 | fvmpt2 5957 |
. . . . . . . . . . . . . 14
             
           
             |
129 | 126, 127,
128 | syl2anc 667 |
. . . . . . . . . . . . 13
  
           
             |
130 | 129, 2 | eqtrd 2485 |
. . . . . . . . . . . 12
  
          |
131 | 130 | ineq1d 3633 |
. . . . . . . . . . 11
  
        
     
       |
132 | | 0in 37393 |
. . . . . . . . . . . 12
       |
133 | 132 | a1i 11 |
. . . . . . . . . . 11
  
            |
134 | 131, 133 | eqtrd 2485 |
. . . . . . . . . 10
  
        
       |
135 | 134 | adantlr 721 |
. . . . . . . . 9
                     |
136 | 135 | ad4ant24 1240 |
. . . . . . . 8
    
            
       |
137 | 26 | a1i 11 |
. . . . . . . . . . . . . . 15
  
                       |
138 | | eqeq1 2455 |
. . . . . . . . . . . . . . . . . 18
     |
139 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . 20
       |
140 | 139 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . 19
   
     |
141 | 140 | notbid 296 |
. . . . . . . . . . . . . . . . . 18
   
     |
142 | 138, 141 | orbi12d 716 |
. . . . . . . . . . . . . . . . 17
     
 
     |
143 | | eqidd 2452 |
. . . . . . . . . . . . . . . . 17
   |
144 | 139 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
          
    |
145 | 142, 143,
144 | ifbieq12d 3908 |
. . . . . . . . . . . . . . . 16
            
      
             |
146 | 145 | adantl 468 |
. . . . . . . . . . . . . . 15
       
    
                            |
147 | | simpl 459 |
. . . . . . . . . . . . . . 15
  
      |
148 | | iftrue 3887 |
. . . . . . . . . . . . . . . . 17
    
                 |
149 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    
  |
150 | 148, 149 | eqeltrd 2529 |
. . . . . . . . . . . . . . . 16
    
                 |
151 | 150 | adantl 468 |
. . . . . . . . . . . . . . 15
  
               
     |
152 | 137, 146,
147, 151 | fvmptd 5954 |
. . . . . . . . . . . . . 14
  
           
             |
153 | 148 | adantl 468 |
. . . . . . . . . . . . . 14
  
               
     |
154 | 152, 153 | eqtrd 2485 |
. . . . . . . . . . . . 13
  
          |
155 | 154 | ineq2d 3634 |
. . . . . . . . . . . 12
  
        
             |
156 | | in0 3760 |
. . . . . . . . . . . . 13
       |
157 | 156 | a1i 11 |
. . . . . . . . . . . 12
  
        
   |
158 | 155, 157 | eqtrd 2485 |
. . . . . . . . . . 11
  
        
       |
159 | 158 | adantll 720 |
. . . . . . . . . 10
                     |
160 | 159 | ad5ant25 1248 |
. . . . . . . . 9
         
             
       |
161 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
162 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . 19
       |
163 | 3, 162 | ifex 3949 |
. . . . . . . . . . . . . . . . . 18
                |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . 17
            
     |
165 | 161, 164,
128 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
        
             |
166 | 165 | adantr 467 |
. . . . . . . . . . . . . . 15
                            |
167 | 10 | adantl 468 |
. . . . . . . . . . . . . . 15
                  
           |
168 | 166, 167 | eqtrd 2485 |
. . . . . . . . . . . . . 14
                   |
169 | 168 | adantlr 721 |
. . . . . . . . . . . . 13
     
  
            |
170 | 169 | 3adant3 1028 |
. . . . . . . . . . . 12
     
   
  
            |
171 | 26 | a1i 11 |
. . . . . . . . . . . . . . 15
      
                   |
172 | 145 | adantl 468 |
. . . . . . . . . . . . . . . 16
        
                          
     |
173 | | iffalse 3890 |
. . . . . . . . . . . . . . . . 17
                
           |
174 | 173 | ad2antlr 733 |
. . . . . . . . . . . . . . . 16
        
                       |
175 | 172, 174 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
        
                       |
176 | | simpl 459 |
. . . . . . . . . . . . . . 15
      
  |
177 | | fvex 5875 |
. . . . . . . . . . . . . . . 16
       |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . 15
               |
179 | 171, 175,
176, 178 | fvmptd 5954 |
. . . . . . . . . . . . . 14
                   |
180 | 179 | adantll 720 |
. . . . . . . . . . . . 13
     
  
            |
181 | 180 | 3adant2 1027 |
. . . . . . . . . . . 12
     
   
  
            |
182 | 170, 181 | ineq12d 3635 |
. . . . . . . . . . 11
     
   
  
                          |
183 | 182 | ad5ant245 1249 |
. . . . . . . . . 10
         
    
        
         
           |
184 | 18 | ad2antlr 733 |
. . . . . . . . . . . . . 14
         
    
        |
185 | | pm2.46 400 |
. . . . . . . . . . . . . . . 16
         |
186 | 185 | notnotrd 117 |
. . . . . . . . . . . . . . 15
         |
187 | 186 | adantl 468 |
. . . . . . . . . . . . . 14
         
    
        |
188 | | f1of1 5813 |
. . . . . . . . . . . . . . . . . . 19
    
      |
189 | 12, 188 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
190 | | dff14a 6170 |
. . . . . . . . . . . . . . . . . 18
    
     

             |
191 | 189, 190 | sylib 200 |
. . . . . . . . . . . . . . . . 17
        
            |
192 | 191 | simprd 465 |
. . . . . . . . . . . . . . . 16
  

           |
193 | 192 | adantr 467 |
. . . . . . . . . . . . . . 15
 
   


           |
194 | 193 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
         
    
    


           |
195 | 184, 187,
194 | jca31 537 |
. . . . . . . . . . . . 13
         
    
             
            |
196 | | nncn 10617 |
. . . . . . . . . . . . . . . . 17
   |
197 | 196 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
   |
198 | 197 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
   
 
   |
199 | | nncn 10617 |
. . . . . . . . . . . . . . . . 17
   |
200 | 199 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
   |
201 | 200 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
   
 
   |
202 | | 1cnd 9659 |
. . . . . . . . . . . . . . 15
   
 
   |
203 | | simpr 463 |
. . . . . . . . . . . . . . 15
   
 
   |
204 | 198, 201,
202, 203 | subneintr2d 10032 |
. . . . . . . . . . . . . 14
   
 
       |
205 | 204 | ad2antrr 732 |
. . . . . . . . . . . . 13
         
    
          |
206 | | neeq1 2686 |
. . . . . . . . . . . . . . 15
   
     |
207 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
          
    |
208 | 207 | neeq1d 2683 |
. . . . . . . . . . . . . . 15
           
             |
209 | 206, 208 | imbi12d 322 |
. . . . . . . . . . . . . 14
                               |
210 | | neeq2 2687 |
. . . . . . . . . . . . . . 15
     
       |
211 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
          
    |
212 | 211 | neeq2d 2684 |
. . . . . . . . . . . . . . 15
             
               |
213 | 210, 212 | imbi12d 322 |
. . . . . . . . . . . . . 14
                          
            |
214 | 209, 213 | rspc2va 3160 |
. . . . . . . . . . . . 13
          
                              |
215 | 195, 205,
214 | sylc 62 |
. . . . . . . . . . . 12
         
    
             
    |
216 | 215 | neneqd 2629 |
. . . . . . . . . . 11
         
    
             
    |
217 | 20 | ad4ant13 1234 |
. . . . . . . . . . . . 13
    
       
            |
218 | | simpl 459 |
. . . . . . . . . . . . . . 15
 
       |
219 | 186 | adantl 468 |
. . . . . . . . . . . . . . 15
 
         |
220 | 14 | ffvelrnda 6022 |
. . . . . . . . . . . . . . 15
 
           |
221 | 218, 219,
220 | syl2anc 667 |
. . . . . . . . . . . . . 14
 
             |
222 | 221 | ad4ant14 1235 |
. . . . . . . . . . . . 13
    
       
            |
223 | | nnfoctbdjlem.dj |
. . . . . . . . . . . . . . 15
 Disj
  |
224 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
225 | 224 | disjor 4387 |
. . . . . . . . . . . . . . 15
Disj




    |
226 | 223, 225 | sylib 200 |
. . . . . . . . . . . . . 14
  
      |
227 | 226 | ad3antrrr 736 |
. . . . . . . . . . . . 13
    
       
    



    |
228 | | eqeq1 2455 |
. . . . . . . . . . . . . . 15
    
  
         |
229 | | ineq1 3627 |
. . . . . . . . . . . . . . . 16
    
  
           |
230 | 229 | eqeq1d 2453 |
. . . . . . . . . . . . . . 15
    
    
           |
231 | 228, 230 | orbi12d 716 |
. . . . . . . . . . . . . 14
    
           
              |
232 | | eqeq2 2462 |
. . . . . . . . . . . . . . 15
    
        
               |
233 | | ineq2 3628 |
. . . . . . . . . . . . . . . 16
    
                          |
234 | 233 | eqeq1d 2453 |
. . . . . . . . . . . . . . 15
    
       
  
          
      |
235 | 232, 234 | orbi12d 716 |
. . . . . . . . . . . . . 14
    
       
               
                          |
236 | 231, 235 | rspc2va 3160 |
. . . . . . . . . . . . 13
      
                                 
            |
237 | 217, 222,
227, 236 | syl21anc 1267 |
. . . . . . . . . . . 12
    
       
                     
            |
238 | 237 | adantllr 725 |
. . . . . . . . . . 11
         
    
                     
            |
239 | | orel1 384 |
. . . . . . . . . . 11
                                     
   
          
      |
240 | 216, 238,
239 | sylc 62 |
. . . . . . . . . 10
         
    
                    |
241 | 183, 240 | eqtrd 2485 |
. . . . . . . . 9
         
    
        
       |
242 | 160, 241 | pm2.61dan 800 |
. . . . . . . 8
    
   
        
       |
243 | 136, 242 | pm2.61dan 800 |
. . . . . . 7
   
 
     
       |
244 | | olc 386 |
. . . . . . 7
     
                   |
245 | 243, 244 | syl 17 |
. . . . . 6
   
 
               |
246 | 123, 125,
245 | syl2anc 667 |
. . . . 5
   
 
               |
247 | 122, 246 | pm2.61dan 800 |
. . . 4
 
                 |
248 | 247 | ralrimivva 2809 |
. . 3
                 |
249 | | fveq2 5865 |
. . . 4
           |
250 | 249 | disjor 4387 |
. . 3
Disj    
                |
251 | 248, 250 | sylibr 216 |
. 2
 Disj
      |
252 | | nnex 10615 |
. . . . 5
 |
253 | 252 | mptex 6136 |
. . . 4
                  |
254 | 26, 253 | eqeltri 2525 |
. . 3
 |
255 | | foeq1 5789 |
. . . 4
      
       
      |
256 | | simpl 459 |
. . . . . 6
 
   |
257 | 256 | fveq1d 5867 |
. . . . 5
 
           |
258 | 257 | disjeq2dv 4378 |
. . . 4
 Disj    
Disj        |
259 | 255, 258 | anbi12d 717 |
. . 3
           Disj     
         Disj         |
260 | 254, 259 | spcev 3141 |
. 2
      
   Disj     
           Disj        |
261 | 120, 251,
260 | syl2anc 667 |
1
            Disj        |