Step | Hyp | Ref
| Expression |
1 | | suceq 4396 |
. . . . . 6
|
2 | 1 | raleqdv 2676 |
. . . . 5
|
3 | 2 | dcbid 838 |
. . . 4
DECID
DECID |
4 | 3 | imbi2d 230 |
. . 3
ℕ∞ DECID
ℕ∞
DECID |
5 | | suceq 4396 |
. . . . . 6
|
6 | 5 | raleqdv 2676 |
. . . . 5
|
7 | 6 | dcbid 838 |
. . . 4
DECID
DECID |
8 | 7 | imbi2d 230 |
. . 3
ℕ∞
DECID
ℕ∞
DECID |
9 | | suceq 4396 |
. . . . . 6
|
10 | 9 | raleqdv 2676 |
. . . . 5
|
11 | 10 | dcbid 838 |
. . . 4
DECID
DECID |
12 | 11 | imbi2d 230 |
. . 3
ℕ∞
DECID
ℕ∞
DECID |
13 | | suceq 4396 |
. . . . . 6
|
14 | 13 | raleqdv 2676 |
. . . . 5
|
15 | 14 | dcbid 838 |
. . . 4
DECID
DECID |
16 | 15 | imbi2d 230 |
. . 3
ℕ∞
DECID
ℕ∞
DECID |
17 | | elmapi 6660 |
. . . . . . 7
ℕ∞ ℕ∞ |
18 | | peano1 4587 |
. . . . . . . 8
|
19 | | nnnninf 7114 |
. . . . . . . 8
ℕ∞ |
20 | 18, 19 | mp1i 10 |
. . . . . . 7
ℕ∞ ℕ∞ |
21 | 17, 20 | ffvelcdmd 5644 |
. . . . . 6
ℕ∞ |
22 | | 2onn 6512 |
. . . . . 6
|
23 | | elnn 4599 |
. . . . . 6
|
24 | 21, 22, 23 | sylancl 413 |
. . . . 5
ℕ∞ |
25 | | 1onn 6511 |
. . . . 5
|
26 | | nndceq 6490 |
. . . . 5
DECID |
27 | 24, 25, 26 | sylancl 413 |
. . . 4
ℕ∞ DECID |
28 | | suc0 4405 |
. . . . . . 7
|
29 | 28 | raleqi 2674 |
. . . . . 6
|
30 | | 0ex 4125 |
. . . . . . 7
|
31 | | eleq2 2239 |
. . . . . . . . . . 11
|
32 | 31 | ifbid 3553 |
. . . . . . . . . 10
|
33 | 32 | mpteq2dv 4089 |
. . . . . . . . 9
|
34 | 33 | fveq2d 5511 |
. . . . . . . 8
|
35 | 34 | eqeq1d 2184 |
. . . . . . 7
|
36 | 30, 35 | ralsn 3632 |
. . . . . 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 4588 |
. . . . . . . . . . . . . 14
|
42 | 41 | adantr 276 |
. . . . . . . . . . . . 13
ℕ∞
|
43 | | nnnninf 7114 |
. . . . . . . . . . . . 13
ℕ∞ |
44 | 42, 43 | syl 14 |
. . . . . . . . . . . 12
ℕ∞
ℕ∞ |
45 | 40, 44 | ffvelcdmd 5644 |
. . . . . . . . . . 11
ℕ∞
|
46 | | elnn 4599 |
. . . . . . . . . . 11
|
47 | 45, 22, 46 | sylancl 413 |
. . . . . . . . . 10
ℕ∞
|
48 | | nndceq 6490 |
. . . . . . . . . 10
DECID
|
49 | 47, 25, 48 | sylancl 413 |
. . . . . . . . 9
ℕ∞
DECID
|
50 | | eleq2 2239 |
. . . . . . . . . . . . . . . 16
|
51 | 50 | ifbid 3553 |
. . . . . . . . . . . . . . 15
|
52 | 51 | mpteq2dv 4089 |
. . . . . . . . . . . . . 14
|
53 | 52 | fveq2d 5511 |
. . . . . . . . . . . . 13
|
54 | 53 | eqeq1d 2184 |
. . . . . . . . . . . 12
|
55 | 54 | ralsng 3629 |
. . . . . . . . . . 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 3314 |
. . . . . . . 8
|
62 | 61 | dcbii 840 |
. . . . . . 7
DECID
DECID |
63 | 60, 62 | sylibr 134 |
. . . . . 6
ℕ∞ DECID
DECID
|
64 | | df-suc 4365 |
. . . . . . . 8
|
65 | 64 | raleqi 2674 |
. . . . . . 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 4593 |
. 2
ℕ∞ DECID |
71 | 70 | impcom 125 |
1
ℕ∞ DECID
|