Theorem ackval41

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

	Ref	Expression
Assertion	ackval41	Could not format assertion : No typesetting found for |- ( ( Ack ` 4 ) ` 1 ) = ; ; ; ; 6 5 5 3 3 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ackval41a	Could not format ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) with typecode |-
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	Could not format ( ( Ack ` 4 ) ` 1 ) = ; ; ; ; 6 5 5 3 3 : No typesetting found for |- ( ( Ack ` 4 ) ` 1 ) = ; ; ; ; 6 5 5 3 3 with typecode |-