Step | Hyp | Ref
| Expression |
1 | | suceq 4399 |
. . . . . 6

  |
2 | 1 | raleqdv 2678 |
. . . . 5

 
           
                |
3 | 2 | dcbid 838 |
. . . 4

DECID             
DECID                 |
4 | 3 | imbi2d 230 |
. . 3

   ℕ∞ DECID 
            
 
ℕ∞
DECID                  |
5 | | suceq 4399 |
. . . . . 6

  |
6 | 5 | raleqdv 2678 |
. . . . 5
  
                            |
7 | 6 | dcbid 838 |
. . . 4
 DECID 
           
DECID                 |
8 | 7 | imbi2d 230 |
. . 3
   
ℕ∞
DECID              
 
ℕ∞
DECID                  |
9 | | suceq 4399 |
. . . . . 6
   |
10 | 9 | raleqdv 2678 |
. . . . 5
              

               |
11 | 10 | dcbid 838 |
. . . 4
 DECID 
            DECID                 |
12 | 11 | imbi2d 230 |
. . 3
   
ℕ∞
DECID              
 
ℕ∞
DECID                  |
13 | | suceq 4399 |
. . . . . 6

  |
14 | 13 | raleqdv 2678 |
. . . . 5
  
                            |
15 | 14 | dcbid 838 |
. . . 4
 DECID 
           
DECID                 |
16 | 15 | imbi2d 230 |
. . 3
   
ℕ∞
DECID              
 
ℕ∞
DECID                  |
17 | | elmapi 6664 |
. . . . . . 7
  ℕ∞  ℕ∞   |
18 | | peano1 4590 |
. . . . . . . 8
 |
19 | | nnnninf 7118 |
. . . . . . . 8

      
ℕ∞ |
20 | 18, 19 | mp1i 10 |
. . . . . . 7
  ℕ∞        ℕ∞ |
21 | 17, 20 | ffvelcdmd 5648 |
. . . . . 6
  ℕ∞              |
22 | | 2onn 6516 |
. . . . . 6
 |
23 | | elnn 4602 |
. . . . . 6
                           |
24 | 21, 22, 23 | sylancl 413 |
. . . . 5
  ℕ∞              |
25 | | 1onn 6515 |
. . . . 5
 |
26 | | nndceq 6494 |
. . . . 5
              DECID              |
27 | 24, 25, 26 | sylancl 413 |
. . . 4
  ℕ∞ DECID              |
28 | | suc0 4408 |
. . . . . . 7
   |
29 | 28 | raleqi 2676 |
. . . . . 6
 
           
                |
30 | | 0ex 4127 |
. . . . . . 7
 |
31 | | eleq2 2241 |
. . . . . . . . . . 11


   |
32 | 31 | ifbid 3555 |
. . . . . . . . . 10

            |
33 | 32 | mpteq2dv 4091 |
. . . . . . . . 9

                |
34 | 33 | fveq2d 5515 |
. . . . . . . 8

                        |
35 | 34 | eqeq1d 2186 |
. . . . . . 7

           
              |
36 | 30, 35 | ralsn 3634 |
. . . . . 6
 
            
             |
37 | 29, 36 | bitri 184 |
. . . . 5
 
           
             |
38 | 37 | dcbii 840 |
. . . 4
DECID              DECID              |
39 | 27, 38 | sylibr 134 |
. . 3
  ℕ∞ DECID                |
40 | 17 | adantl 277 |
. . . . . . . . . . . 12
 
 ℕ∞
 ℕ∞   |
41 | | peano2 4591 |
. . . . . . . . . . . . . 14

  |
42 | 41 | adantr 276 |
. . . . . . . . . . . . 13
 
 ℕ∞
  |
43 | | nnnninf 7118 |
. . . . . . . . . . . . 13
    
  
ℕ∞ |
44 | 42, 43 | syl 14 |
. . . . . . . . . . . 12
 
 ℕ∞
       ℕ∞ |
45 | 40, 44 | ffvelcdmd 5648 |
. . . . . . . . . . 11
 
 ℕ∞
      
      |
46 | | elnn 4602 |
. . . . . . . . . . 11
        
    
      
      |
47 | 45, 22, 46 | sylancl 413 |
. . . . . . . . . 10
 
 ℕ∞
      
      |
48 | | nndceq 6494 |
. . . . . . . . . 10
        
   

DECID       
      |
49 | 47, 25, 48 | sylancl 413 |
. . . . . . . . 9
 
 ℕ∞
DECID       
      |
50 | | eleq2 2241 |
. . . . . . . . . . . . . . . 16
     |
51 | 50 | ifbid 3555 |
. . . . . . . . . . . . . . 15
     
       |
52 | 51 | mpteq2dv 4091 |
. . . . . . . . . . . . . 14
           
     |
53 | 52 | fveq2d 5515 |
. . . . . . . . . . . . 13
                  
      |
54 | 53 | eqeq1d 2186 |
. . . . . . . . . . . 12
                   
       |
55 | 54 | ralsng 3631 |
. . . . . . . . . . 11
               
      
       |
56 | 42, 55 | syl 14 |
. . . . . . . . . 10
 
 ℕ∞
 
 
                 
       |
57 | 56 | dcbid 838 |
. . . . . . . . 9
 
 ℕ∞
DECID
              DECID               |
58 | 49, 57 | mpbird 167 |
. . . . . . . 8
 
 ℕ∞
DECID                 |
59 | | dcan2 934 |
. . . . . . . 8
DECID              DECID 
 
          
DECID               
 
               |
60 | 58, 59 | mpan9 281 |
. . . . . . 7
    ℕ∞ DECID
              DECID  
                             |
61 | | ralunb 3316 |
. . . . . . . 8
 

              
 
              
              |
62 | 61 | dcbii 840 |
. . . . . . 7
DECID   
              DECID                                |
63 | 60, 62 | sylibr 134 |
. . . . . 6
    ℕ∞ DECID
              DECID   
                |
64 | | df-suc 4368 |
. . . . . . . 8

    |
65 | 64 | raleqi 2676 |
. . . . . . 7
 
                               |
66 | 65 | dcbii 840 |
. . . . . 6
DECID 
           
DECID                    |
67 | 63, 66 | sylibr 134 |
. . . . 5
    ℕ∞ DECID
              DECID 
              |
68 | 67 | exp31 364 |
. . . 4
 
 ℕ∞ DECID             
DECID                  |
69 | 68 | a2d 26 |
. . 3
   
ℕ∞
DECID               
 ℕ∞ DECID                  |
70 | 4, 8, 12, 16, 39, 69 | finds 4596 |
. 2
 
 ℕ∞ DECID                 |
71 | 70 | impcom 125 |
1
   ℕ∞  DECID 
              |