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 )