Theorem ackval42a

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

	Ref	Expression
Assertion	ackval42a	Could not format assertion : No typesetting found for |- ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ( 2 ^ ( 2 ^ ( 2 ^ 2 ) ) ) ) - 3 ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ackval42	Could not format ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 ) with typecode |-
2		sq2	$$⊢2^2=4$$
3	2	oveq2i	$$⊢2^{2^2}=2^4$$
4		2exp4	$$⊢2^4=16$$
5	3 4	eqtri	$$⊢2^{2^2}=16$$
6	5	oveq2i	$$⊢2^{2^{2^2}}=2^{16}$$
7		2exp16	$$⊢2^{16}=65536$$
8	6 7	eqtr2i	$$⊢65536=2^{2^{2^2}}$$
9	8	oveq2i	$$⊢2^{65536}=2^{2^{2^{2^2}}}$$
10	9	oveq1i	$$⊢2^{65536}-3=2^{2^{2^{2^2}}}-3$$
11	1 10	eqtri	Could not format ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ( 2 ^ ( 2 ^ ( 2 ^ 2 ) ) ) ) - 3 ) : No typesetting found for |- ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ( 2 ^ ( 2 ^ ( 2 ^ 2 ) ) ) ) - 3 ) with typecode |-