Theorem ackval41

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

	Ref	Expression
Assertion	ackval41	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=65533$$

Proof

Step	Hyp	Ref	Expression
1		ackval41a	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=2^{16}-3$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3		5nn0	$$⊢5\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢65\in {\mathbb{N}}_0$$
5	4 3	deccl	$$⊢655\in {\mathbb{N}}_0$$
6		3nn0	$$⊢3\in {\mathbb{N}}_0$$
7	5 6	deccl	$$⊢6553\in {\mathbb{N}}_0$$
8		2exp16	$$⊢2^{16}=65536$$
9		3p1e4	$$⊢3+1=4$$
10		eqid	$$⊢6553=6553$$
11	5 6 9 10	decsuc	$$⊢6553+1=6554$$
12		3cn	$$⊢3\in ℂ$$
13		gbpart6	$$⊢6=3+3$$
14	12 12 13	mvrraddi	$$⊢6-3=3$$
15	7 2 6 8 11 14	decsubi	$$⊢2^{16}-3=65533$$
16	1 15	eqtri	$$⊢\mathrm{Ack}\left(4\right)\left(1\right)=65533$$