Step | Hyp | Ref
| Expression |
1 | | df-2 12221 |
. . 3
β’ 2 = (1 +
1) |
2 | 1 | fveq2i 6846 |
. 2
β’
(Ackβ2) = (Ackβ(1 + 1)) |
3 | | 1nn0 12434 |
. . 3
β’ 1 β
β0 |
4 | | ackvalsuc1mpt 46850 |
. . 3
β’ (1 β
β0 β (Ackβ(1 + 1)) = (π β β0 β¦
(((IterCompβ(Ackβ1))β(π + 1))β1))) |
5 | 3, 4 | ax-mp 5 |
. 2
β’
(Ackβ(1 + 1)) = (π β β0 β¦
(((IterCompβ(Ackβ1))β(π + 1))β1)) |
6 | | peano2nn0 12458 |
. . . . . 6
β’ (π β β0
β (π + 1) β
β0) |
7 | | 2nn0 12435 |
. . . . . 6
β’ 2 β
β0 |
8 | | ackval1 46853 |
. . . . . . 7
β’
(Ackβ1) = (π
β β0 β¦ (π + 2)) |
9 | 8 | itcovalpc 46844 |
. . . . . 6
β’ (((π + 1) β β0
β§ 2 β β0) β
((IterCompβ(Ackβ1))β(π + 1)) = (π β β0 β¦ (π + (2 Β· (π + 1))))) |
10 | 6, 7, 9 | sylancl 587 |
. . . . 5
β’ (π β β0
β ((IterCompβ(Ackβ1))β(π + 1)) = (π β β0 β¦ (π + (2 Β· (π + 1))))) |
11 | 10 | fveq1d 6845 |
. . . 4
β’ (π β β0
β (((IterCompβ(Ackβ1))β(π + 1))β1) = ((π β β0 β¦ (π + (2 Β· (π +
1))))β1)) |
12 | | eqidd 2734 |
. . . . 5
β’ (π β β0
β (π β
β0 β¦ (π + (2 Β· (π + 1)))) = (π β β0 β¦ (π + (2 Β· (π + 1))))) |
13 | | oveq1 7365 |
. . . . . 6
β’ (π = 1 β (π + (2 Β· (π + 1))) = (1 + (2 Β· (π + 1)))) |
14 | 13 | adantl 483 |
. . . . 5
β’ ((π β β0
β§ π = 1) β (π + (2 Β· (π + 1))) = (1 + (2 Β·
(π + 1)))) |
15 | 3 | a1i 11 |
. . . . 5
β’ (π β β0
β 1 β β0) |
16 | | ovexd 7393 |
. . . . 5
β’ (π β β0
β (1 + (2 Β· (π
+ 1))) β V) |
17 | 12, 14, 15, 16 | fvmptd 6956 |
. . . 4
β’ (π β β0
β ((π β
β0 β¦ (π + (2 Β· (π + 1))))β1) = (1 + (2 Β· (π + 1)))) |
18 | | nn0cn 12428 |
. . . . 5
β’ (π β β0
β π β
β) |
19 | | 1cnd 11155 |
. . . . . . 7
β’ (π β β β 1 β
β) |
20 | | 2cnd 12236 |
. . . . . . . 8
β’ (π β β β 2 β
β) |
21 | | peano2cn 11332 |
. . . . . . . 8
β’ (π β β β (π + 1) β
β) |
22 | 20, 21 | mulcld 11180 |
. . . . . . 7
β’ (π β β β (2
Β· (π + 1)) β
β) |
23 | 19, 22 | addcomd 11362 |
. . . . . 6
β’ (π β β β (1 + (2
Β· (π + 1))) = ((2
Β· (π + 1)) +
1)) |
24 | | id 22 |
. . . . . . . 8
β’ (π β β β π β
β) |
25 | 20, 24, 19 | adddid 11184 |
. . . . . . 7
β’ (π β β β (2
Β· (π + 1)) = ((2
Β· π) + (2 Β·
1))) |
26 | 25 | oveq1d 7373 |
. . . . . 6
β’ (π β β β ((2
Β· (π + 1)) + 1) =
(((2 Β· π) + (2
Β· 1)) + 1)) |
27 | 20, 24 | mulcld 11180 |
. . . . . . . 8
β’ (π β β β (2
Β· π) β
β) |
28 | 20, 19 | mulcld 11180 |
. . . . . . . 8
β’ (π β β β (2
Β· 1) β β) |
29 | 27, 28, 19 | addassd 11182 |
. . . . . . 7
β’ (π β β β (((2
Β· π) + (2 Β·
1)) + 1) = ((2 Β· π)
+ ((2 Β· 1) + 1))) |
30 | | 2t1e2 12321 |
. . . . . . . . . . 11
β’ (2
Β· 1) = 2 |
31 | 30 | oveq1i 7368 |
. . . . . . . . . 10
β’ ((2
Β· 1) + 1) = (2 + 1) |
32 | | 2p1e3 12300 |
. . . . . . . . . 10
β’ (2 + 1) =
3 |
33 | 31, 32 | eqtri 2761 |
. . . . . . . . 9
β’ ((2
Β· 1) + 1) = 3 |
34 | 33 | a1i 11 |
. . . . . . . 8
β’ (π β β β ((2
Β· 1) + 1) = 3) |
35 | 34 | oveq2d 7374 |
. . . . . . 7
β’ (π β β β ((2
Β· π) + ((2 Β·
1) + 1)) = ((2 Β· π)
+ 3)) |
36 | 29, 35 | eqtrd 2773 |
. . . . . 6
β’ (π β β β (((2
Β· π) + (2 Β·
1)) + 1) = ((2 Β· π)
+ 3)) |
37 | 23, 26, 36 | 3eqtrd 2777 |
. . . . 5
β’ (π β β β (1 + (2
Β· (π + 1))) = ((2
Β· π) +
3)) |
38 | 18, 37 | syl 17 |
. . . 4
β’ (π β β0
β (1 + (2 Β· (π
+ 1))) = ((2 Β· π) +
3)) |
39 | 11, 17, 38 | 3eqtrd 2777 |
. . 3
β’ (π β β0
β (((IterCompβ(Ackβ1))β(π + 1))β1) = ((2 Β· π) + 3)) |
40 | 39 | mpteq2ia 5209 |
. 2
β’ (π β β0
β¦ (((IterCompβ(Ackβ1))β(π + 1))β1)) = (π β β0 β¦ ((2
Β· π) +
3)) |
41 | 2, 5, 40 | 3eqtri 2765 |
1
β’
(Ackβ2) = (π
β β0 β¦ ((2 Β· π) + 3)) |