Theorem ackval42a

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

	Ref	Expression
Assertion	ackval42a	$$⊢\mathrm{Ack}\left(4\right)\left(2\right)=2^{2^{2^{2^2}}}-3$$

Proof

Step	Hyp	Ref	Expression
1		ackval42	$$⊢\mathrm{Ack}\left(4\right)\left(2\right)=2^{65536}-3$$
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	$$⊢\mathrm{Ack}\left(4\right)\left(2\right)=2^{2^{2^{2^2}}}-3$$