This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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