Theorem ackval50

Description: The Ackermann function at (5,0). (Contributed by AV, 9-May-2024)

	Ref	Expression
Assertion	ackval50	$$⊢\mathrm{Ack}\left(5\right)\left(0\right)=65533$$

Proof

Step	Hyp	Ref	Expression
1		df-5	$$⊢5=4+1$$
2	1	fveq2i	$$⊢\mathrm{Ack}\left(5\right)=\mathrm{Ack}\left(4+1\right)$$
3	2	fveq1i	$$⊢\mathrm{Ack}\left(5\right)\left(0\right)=\mathrm{Ack}\left(4+1\right)\left(0\right)$$
4		4nn0	$$⊢4\in {\mathbb{N}}_0$$
5		ackvalsuc0val	$$⊢4\in {\mathbb{N}}_0\to \mathrm{Ack}\left(4+1\right)\left(0\right)=\mathrm{Ack}\left(4\right)\left(1\right)$$
6	4 5	ax-mp	$$⊢\mathrm{Ack}\left(4+1\right)\left(0\right)=\mathrm{Ack}\left(4\right)\left(1\right)$$
7		ackval41	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=65533$$
8	3 6 7	3eqtri	$$⊢\mathrm{Ack}\left(5\right)\left(0\right)=65533$$