Theorem ackval41a

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

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

Proof

Step	Hyp	Ref	Expression
1		df-4	$$⊢4=3+1$$
2	1	fveq2i	Could not format ( Ack ` 4 ) = ( Ack ` ( 3 + 1 ) ) : No typesetting found for |- ( Ack ` 4 ) = ( Ack ` ( 3 + 1 ) ) with typecode |-
3		1e0p1	$$⊢1=0+1$$
4	2 3	fveq12i	Could not format ( ( Ack ` 4 ) ` 1 ) = ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) : No typesetting found for |- ( ( Ack ` 4 ) ` 1 ) = ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) with typecode |-
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7		ackvalsucsucval	Could not format ( ( 3 e. NN0 /\ 0 e. NN0 ) -> ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) ) : No typesetting found for |- ( ( 3 e. NN0 /\ 0 e. NN0 ) -> ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) ) with typecode |-
8	5 6 7	mp2an	Could not format ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) with typecode |-
9		3p1e4	$$⊢3+1=4$$
10	9	fveq2i	Could not format ( Ack ` ( 3 + 1 ) ) = ( Ack ` 4 ) : No typesetting found for |- ( Ack ` ( 3 + 1 ) ) = ( Ack ` 4 ) with typecode |-
11	10	fveq1i	Could not format ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 4 ) ` 0 ) : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 4 ) ` 0 ) with typecode |-
12		ackval40	Could not format ( ( Ack ` 4 ) ` 0 ) = ; 1 3 : No typesetting found for |- ( ( Ack ` 4 ) ` 0 ) = ; 1 3 with typecode |-
13	11 12	eqtri	Could not format ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ; 1 3 : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ; 1 3 with typecode |-
14	13	fveq2i	Could not format ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) = ( ( Ack ` 3 ) ` ; 1 3 ) : No typesetting found for |- ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) = ( ( Ack ` 3 ) ` ; 1 3 ) with typecode |-
15		1nn0	$$⊢1\in {\mathbb{N}}_0$$
16	15 5	deccl	$$⊢13\in {\mathbb{N}}_0$$
17		oveq1	$$⊢n=13\to n+3=13+3$$
18	17	oveq2d	$$⊢n=13\to 2^{n+3}=2^{13+3}$$
19	18	oveq1d	$$⊢n=13\to 2^{n+3}-3=2^{13+3}-3$$
20		eqid	$$⊢13=13$$
21		3p3e6	$$⊢3+3=6$$
22	15 5 5 20 21	decaddi	$$⊢13+3=16$$
23	22	oveq2i	$$⊢2^{13+3}=2^{16}$$
24	23	oveq1i	$$⊢2^{13+3}-3=2^{16}-3$$
25	19 24	eqtrdi	$$⊢n=13\to 2^{n+3}-3=2^{16}-3$$
26		ackval3	Could not format ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) : No typesetting found for |- ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) with typecode |-
27		ovex	$$⊢2^{16}-3\in \mathrm{V}$$
28	25 26 27	fvmpt	Could not format ( ; 1 3 e. NN0 -> ( ( Ack ` 3 ) ` ; 1 3 ) = ( ( 2 ^ ; 1 6 ) - 3 ) ) : No typesetting found for |- ( ; 1 3 e. NN0 -> ( ( Ack ` 3 ) ` ; 1 3 ) = ( ( 2 ^ ; 1 6 ) - 3 ) ) with typecode |-
29	16 28	ax-mp	Could not format ( ( Ack ` 3 ) ` ; 1 3 ) = ( ( 2 ^ ; 1 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 3 ) ` ; 1 3 ) = ( ( 2 ^ ; 1 6 ) - 3 ) with typecode |-
30	14 29	eqtri	Could not format ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) = ( ( 2 ^ ; 1 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) = ( ( 2 ^ ; 1 6 ) - 3 ) with typecode |-
31	8 30	eqtri	Could not format ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( 2 ^ ; 1 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( 2 ^ ; 1 6 ) - 3 ) with typecode |-
32	4 31	eqtri	Could not format ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) with typecode |-