Step |
Hyp |
Ref |
Expression |
1 |
|
ackval41a |
⊢ ( ( Ack ‘ 4 ) ‘ 1 ) = ( ( 2 ↑ ; 1 6 ) − 3 ) |
2 |
|
6nn0 |
⊢ 6 ∈ ℕ0 |
3 |
|
5nn0 |
⊢ 5 ∈ ℕ0 |
4 |
2 3
|
deccl |
⊢ ; 6 5 ∈ ℕ0 |
5 |
4 3
|
deccl |
⊢ ; ; 6 5 5 ∈ ℕ0 |
6 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
7 |
5 6
|
deccl |
⊢ ; ; ; 6 5 5 3 ∈ ℕ0 |
8 |
|
2exp16 |
⊢ ( 2 ↑ ; 1 6 ) = ; ; ; ; 6 5 5 3 6 |
9 |
|
3p1e4 |
⊢ ( 3 + 1 ) = 4 |
10 |
|
eqid |
⊢ ; ; ; 6 5 5 3 = ; ; ; 6 5 5 3 |
11 |
5 6 9 10
|
decsuc |
⊢ ( ; ; ; 6 5 5 3 + 1 ) = ; ; ; 6 5 5 4 |
12 |
|
3cn |
⊢ 3 ∈ ℂ |
13 |
|
gbpart6 |
⊢ 6 = ( 3 + 3 ) |
14 |
12 12 13
|
mvrraddi |
⊢ ( 6 − 3 ) = 3 |
15 |
7 2 6 8 11 14
|
decsubi |
⊢ ( ( 2 ↑ ; 1 6 ) − 3 ) = ; ; ; ; 6 5 5 3 3 |
16 |
1 15
|
eqtri |
⊢ ( ( Ack ‘ 4 ) ‘ 1 ) = ; ; ; ; 6 5 5 3 3 |