Proof of Theorem nninfwlpoimlemginf
Step | Hyp | Ref
| Expression |
1 | | nninfwlpoimlemg.g |
. . . . . . . 8
              |
2 | | suceq 4399 |
. . . . . . . . . 10

  |
3 | 2 | rexeqdv 2679 |
. . . . . . . . 9
  
     
        |
4 | 3 | ifbid 3555 |
. . . . . . . 8
                         |
5 | | simpr 110 |
. . . . . . . 8
         |
6 | | 0lt2o 6436 |
. . . . . . . . . 10
 |
7 | 6 | a1i 9 |
. . . . . . . . 9
         |
8 | | 1lt2o 6437 |
. . . . . . . . . 10
 |
9 | 8 | a1i 9 |
. . . . . . . . 9
         |
10 | | peano2 4591 |
. . . . . . . . . . . 12

  |
11 | 10 | adantl 277 |
. . . . . . . . . . 11
      
  |
12 | | nnfi 6866 |
. . . . . . . . . . 11
   |
13 | 11, 12 | syl 14 |
. . . . . . . . . 10
      
  |
14 | | 2ssom 6519 |
. . . . . . . . . . . . 13
 |
15 | | nninfwlpoimlemg.f |
. . . . . . . . . . . . . . 15
       |
16 | 15 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
   
           |
17 | | simpr 110 |
. . . . . . . . . . . . . . 15
   
       |
18 | 11 | adantr 276 |
. . . . . . . . . . . . . . 15
   
    
  |
19 | | elnn 4602 |
. . . . . . . . . . . . . . 15
     |
20 | 17, 18, 19 | syl2anc 411 |
. . . . . . . . . . . . . 14
   
       |
21 | 16, 20 | ffvelcdmd 5648 |
. . . . . . . . . . . . 13
   
           |
22 | 14, 21 | sselid 3153 |
. . . . . . . . . . . 12
   
           |
23 | | peano1 4590 |
. . . . . . . . . . . . 13
 |
24 | 23 | a1i 9 |
. . . . . . . . . . . 12
   
       |
25 | | nndceq 6494 |
. . . . . . . . . . . 12
      
DECID       |
26 | 22, 24, 25 | syl2anc 411 |
. . . . . . . . . . 11
   
    
DECID       |
27 | 26 | ralrimiva 2550 |
. . . . . . . . . 10
        DECID       |
28 | | finexdc 6896 |
. . . . . . . . . 10
   DECID     
DECID         |
29 | 13, 27, 28 | syl2anc 411 |
. . . . . . . . 9
       DECID 
       |
30 | 7, 9, 29 | ifcldcd 3569 |
. . . . . . . 8
                    |
31 | 1, 4, 5, 30 | fvmptd3 5605 |
. . . . . . 7
                        |
32 | 31 | adantr 276 |
. . . . . 6
   
                          |
33 | | vex 2740 |
. . . . . . . . . 10
 |
34 | 33 | sucid 4414 |
. . . . . . . . 9
 |
35 | 34 | a1i 9 |
. . . . . . . 8
   
           |
36 | | simpr 110 |
. . . . . . . 8
   
               |
37 | | fveqeq2 5520 |
. . . . . . . . 9
     
       |
38 | 37 | rspcev 2841 |
. . . . . . . 8
       
       |
39 | 35, 36, 38 | syl2anc 411 |
. . . . . . 7
   
                 |
40 | 39 | iftrued 3541 |
. . . . . 6
   
                      |
41 | 32, 40 | eqtrd 2210 |
. . . . 5
   
               |
42 | | 1n0 6427 |
. . . . . . 7
 |
43 | 42 | neii 2349 |
. . . . . 6
 |
44 | | simpllr 534 |
. . . . . . . . 9
   
             |
45 | 44 | fveq1d 5513 |
. . . . . . . 8
   
                     |
46 | | eqid 2177 |
. . . . . . . . 9
     |
47 | | eqidd 2178 |
. . . . . . . . 9
   |
48 | 5 | adantr 276 |
. . . . . . . . 9
   
           |
49 | 8 | a1i 9 |
. . . . . . . . 9
   
           |
50 | 46, 47, 48, 49 | fvmptd3 5605 |
. . . . . . . 8
   
                 |
51 | 45, 50 | eqtrd 2210 |
. . . . . . 7
   
               |
52 | 51 | eqeq1d 2186 |
. . . . . 6
   
                 |
53 | 43, 52 | mtbiri 675 |
. . . . 5
   
        
      |
54 | 41, 53 | pm2.65da 661 |
. . . 4
      
      |
55 | 15 | adantr 276 |
. . . . . . 7
 
         |
56 | 55 | ffvelcdmda 5647 |
. . . . . 6
             |
57 | | elpri 3614 |
. . . . . . 7
                    |
58 | | df2o3 6425 |
. . . . . . 7
    |
59 | 57, 58 | eleq2s 2272 |
. . . . . 6
                 |
60 | 56, 59 | syl 14 |
. . . . 5
                   |
61 | 60 | orcomd 729 |
. . . 4
                   |
62 | 54, 61 | ecased 1349 |
. . 3
             |
63 | 62 | ralrimiva 2550 |
. 2
 
          |
64 | | eqeq1 2184 |
. . . . . . . . . . 11
         
   |
65 | 43, 64 | mtbiri 675 |
. . . . . . . . . 10
           |
66 | 65 | ralimi 2540 |
. . . . . . . . 9
 
   
       |
67 | | ralnex 2465 |
. . . . . . . . 9
 
   
       |
68 | 66, 67 | sylib 122 |
. . . . . . . 8
 
   

      |
69 | | fveqeq2 5520 |
. . . . . . . . 9
     
       |
70 | 69 | cbvrexv 2704 |
. . . . . . . 8
             |
71 | 68, 70 | sylnib 676 |
. . . . . . 7
 
   

      |
72 | 71 | ad2antlr 489 |
. . . . . 6
   
             |
73 | | peano2 4591 |
. . . . . . . 8

  |
74 | 73 | adantl 277 |
. . . . . . 7
   
     
  |
75 | | elomssom 4601 |
. . . . . . 7

  |
76 | | ssrexv 3220 |
. . . . . . 7

               |
77 | 74, 75, 76 | 3syl 17 |
. . . . . 6
   
       
             |
78 | 72, 77 | mtod 663 |
. . . . 5
   
              |
79 | 78 | iffalsed 3544 |
. . . 4
   
                   |
80 | 79 | mpteq2dva 4090 |
. . 3
 
     
                 |
81 | 1, 80 | eqtrid 2222 |
. 2
 
     
    |
82 | 63, 81 | impbida 596 |
1
            |