Step | Hyp | Ref
| Expression |
1 | | df-3 12222 |
. . 3
β’ 3 = (2 +
1) |
2 | 1 | fveq2i 6846 |
. 2
β’
(Ackβ3) = (Ackβ(2 + 1)) |
3 | | 2nn0 12435 |
. . 3
β’ 2 β
β0 |
4 | | ackvalsuc1mpt 46850 |
. . 3
β’ (2 β
β0 β (Ackβ(2 + 1)) = (π β β0 β¦
(((IterCompβ(Ackβ2))β(π + 1))β1))) |
5 | 3, 4 | ax-mp 5 |
. 2
β’
(Ackβ(2 + 1)) = (π β β0 β¦
(((IterCompβ(Ackβ2))β(π + 1))β1)) |
6 | | peano2nn0 12458 |
. . . . . 6
β’ (π β β0
β (π + 1) β
β0) |
7 | | 3nn0 12436 |
. . . . . 6
β’ 3 β
β0 |
8 | | ackval2 46854 |
. . . . . . 7
β’
(Ackβ2) = (π
β β0 β¦ ((2 Β· π) + 3)) |
9 | 8 | itcovalt2 46849 |
. . . . . 6
β’ (((π + 1) β β0
β§ 3 β β0) β
((IterCompβ(Ackβ2))β(π + 1)) = (π β β0 β¦ (((π + 3) Β· (2β(π + 1))) β
3))) |
10 | 6, 7, 9 | sylancl 587 |
. . . . 5
β’ (π β β0
β ((IterCompβ(Ackβ2))β(π + 1)) = (π β β0 β¦ (((π + 3) Β· (2β(π + 1))) β
3))) |
11 | 10 | fveq1d 6845 |
. . . 4
β’ (π β β0
β (((IterCompβ(Ackβ2))β(π + 1))β1) = ((π β β0 β¦ (((π + 3) Β· (2β(π + 1))) β
3))β1)) |
12 | | eqidd 2734 |
. . . . 5
β’ (π β β0
β (π β
β0 β¦ (((π + 3) Β· (2β(π + 1))) β 3)) = (π β β0 β¦ (((π + 3) Β· (2β(π + 1))) β
3))) |
13 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = 1 β (π + 3) = (1 + 3)) |
14 | | 3cn 12239 |
. . . . . . . . . 10
β’ 3 β
β |
15 | | ax-1cn 11114 |
. . . . . . . . . 10
β’ 1 β
β |
16 | | 3p1e4 12303 |
. . . . . . . . . 10
β’ (3 + 1) =
4 |
17 | 14, 15, 16 | addcomli 11352 |
. . . . . . . . 9
β’ (1 + 3) =
4 |
18 | 13, 17 | eqtrdi 2789 |
. . . . . . . 8
β’ (π = 1 β (π + 3) = 4) |
19 | 18 | oveq1d 7373 |
. . . . . . 7
β’ (π = 1 β ((π + 3) Β· (2β(π + 1))) = (4 Β· (2β(π + 1)))) |
20 | 19 | oveq1d 7373 |
. . . . . 6
β’ (π = 1 β (((π + 3) Β· (2β(π + 1))) β 3) = ((4
Β· (2β(π + 1)))
β 3)) |
21 | 20 | adantl 483 |
. . . . 5
β’ ((π β β0
β§ π = 1) β
(((π + 3) Β·
(2β(π + 1))) β
3) = ((4 Β· (2β(π + 1))) β 3)) |
22 | | 1nn0 12434 |
. . . . . 6
β’ 1 β
β0 |
23 | 22 | a1i 11 |
. . . . 5
β’ (π β β0
β 1 β β0) |
24 | | ovexd 7393 |
. . . . 5
β’ (π β β0
β ((4 Β· (2β(π + 1))) β 3) β V) |
25 | 12, 21, 23, 24 | fvmptd 6956 |
. . . 4
β’ (π β β0
β ((π β
β0 β¦ (((π + 3) Β· (2β(π + 1))) β 3))β1) = ((4 Β·
(2β(π + 1))) β
3)) |
26 | | sq2 14107 |
. . . . . . . . 9
β’
(2β2) = 4 |
27 | 26 | eqcomi 2742 |
. . . . . . . 8
β’ 4 =
(2β2) |
28 | 27 | a1i 11 |
. . . . . . 7
β’ (π β β0
β 4 = (2β2)) |
29 | 28 | oveq1d 7373 |
. . . . . 6
β’ (π β β0
β (4 Β· (2β(π + 1))) = ((2β2) Β· (2β(π + 1)))) |
30 | | 2cnd 12236 |
. . . . . . 7
β’ (π β β0
β 2 β β) |
31 | 3 | a1i 11 |
. . . . . . 7
β’ (π β β0
β 2 β β0) |
32 | 30, 6, 31 | expaddd 14059 |
. . . . . 6
β’ (π β β0
β (2β(2 + (π +
1))) = ((2β2) Β· (2β(π + 1)))) |
33 | | nn0cn 12428 |
. . . . . . . . 9
β’ (π β β0
β π β
β) |
34 | | 1cnd 11155 |
. . . . . . . . 9
β’ (π β β0
β 1 β β) |
35 | 30, 33, 34 | add12d 11386 |
. . . . . . . 8
β’ (π β β0
β (2 + (π + 1)) =
(π + (2 +
1))) |
36 | | 2p1e3 12300 |
. . . . . . . . 9
β’ (2 + 1) =
3 |
37 | 36 | oveq2i 7369 |
. . . . . . . 8
β’ (π + (2 + 1)) = (π + 3) |
38 | 35, 37 | eqtrdi 2789 |
. . . . . . 7
β’ (π β β0
β (2 + (π + 1)) =
(π + 3)) |
39 | 38 | oveq2d 7374 |
. . . . . 6
β’ (π β β0
β (2β(2 + (π +
1))) = (2β(π +
3))) |
40 | 29, 32, 39 | 3eqtr2d 2779 |
. . . . 5
β’ (π β β0
β (4 Β· (2β(π + 1))) = (2β(π + 3))) |
41 | 40 | oveq1d 7373 |
. . . 4
β’ (π β β0
β ((4 Β· (2β(π + 1))) β 3) = ((2β(π + 3)) β
3)) |
42 | 11, 25, 41 | 3eqtrd 2777 |
. . 3
β’ (π β β0
β (((IterCompβ(Ackβ2))β(π + 1))β1) = ((2β(π + 3)) β
3)) |
43 | 42 | mpteq2ia 5209 |
. 2
β’ (π β β0
β¦ (((IterCompβ(Ackβ2))β(π + 1))β1)) = (π β β0 β¦
((2β(π + 3)) β
3)) |
44 | 2, 5, 43 | 3eqtri 2765 |
1
β’
(Ackβ3) = (π
β β0 β¦ ((2β(π + 3)) β 3)) |