Metamath Proof Explorer

Theorem ackval42a

Description: The Ackermann function at (4,2), expressed with powers of 2. (Contributed by AV, 9-May-2024)

Ref Expression
Assertion ackval42a ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( 2 ↑ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) ) − 3 )

Proof

Step Hyp Ref Expression
1 ackval42 ⊢ ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( 2 ↑ 6 5 5 3 6 ) − 3 )
2 sq2 ⊢ ( 2 ↑ 2 ) = 4
3 2 oveq2i ⊢ ( 2 ↑ ( 2 ↑ 2 ) ) = ( 2 ↑ 4 )
4 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
5 3 4 eqtri ⊢ ( 2 ↑ ( 2 ↑ 2 ) ) = 1 6
6 5 oveq2i ⊢ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) = ( 2 ↑ 1 6 )
7 2exp16 ⊢ ( 2 ↑ 1 6 ) = 6 5 5 3 6
8 6 7 eqtr2i ⊢ 6 5 5 3 6 = ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) )
9 8 oveq2i ⊢ ( 2 ↑ 6 5 5 3 6 ) = ( 2 ↑ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) )
10 9 oveq1i ⊢ ( ( 2 ↑ 6 5 5 3 6 ) − 3 ) = ( ( 2 ↑ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) ) − 3 )
11 1 10 eqtri ⊢ ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( 2 ↑ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) ) − 3 )