Metamath Proof Explorer


Theorem ackval41

Description: The Ackermann function at (4,1). (Contributed by AV, 9-May-2024)

Ref Expression
Assertion ackval41 ( ( Ack ‘ 4 ) ‘ 1 ) = 6 5 5 3 3

Proof

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