Theorem ackval42

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

	Ref	Expression
Assertion	ackval42	Could not format assertion : No typesetting found for |- ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 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		df-2	$$⊢2=1+1$$
4	2 3	fveq12i	Could not format ( ( Ack ` 4 ) ` 2 ) = ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) : No typesetting found for |- ( ( Ack ` 4 ) ` 2 ) = ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) with typecode |-
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		ackvalsucsucval	Could not format ( ( 3 e. NN0 /\ 1 e. NN0 ) -> ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( ( 3 e. NN0 /\ 1 e. NN0 ) -> ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) ) with typecode |-
8	5 6 7	mp2an	Could not format ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) 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 ) ) ` 1 ) = ( ( Ack ` 4 ) ` 1 ) : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` 1 ) = ( ( Ack ` 4 ) ` 1 ) with typecode |-
12		ackval41a	Could not format ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) with typecode |-
13	11 12	eqtri	Could not format ( ( Ack ` ( 3 + 1 ) ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` ( 3 + 1 ) ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 ) with typecode |-
14	13	fveq2i	Could not format ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) = ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) : No typesetting found for |- ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) = ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) with typecode |-
15		2cn	$$⊢2\in ℂ$$
16		6nn0	$$⊢6\in {\mathbb{N}}_0$$
17	6 16	deccl	$$⊢16\in {\mathbb{N}}_0$$
18		expcl	$$⊢\left(2\in ℂ\wedge 16\in {\mathbb{N}}_0\right)\to 2^{16}\in ℂ$$
19	15 17 18	mp2an	$$⊢2^{16}\in ℂ$$
20		3cn	$$⊢3\in ℂ$$
21		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 |-
22		oveq1	$$⊢n=2^{16}-3\to n+3=2^{16}-3+3$$
23		npcan	$$⊢\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\to 2^{16}-3+3=2^{16}$$
24	22 23	sylan9eqr	$$⊢\left(\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\wedge n=2^{16}-3\right)\to n+3=2^{16}$$
25	24	oveq2d	$$⊢\left(\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\wedge n=2^{16}-3\right)\to 2^{n+3}=2^{2^{16}}$$
26	25	oveq1d	$$⊢\left(\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\wedge n=2^{16}-3\right)\to 2^{n+3}-3=2^{2^{16}}-3$$
27		3re	$$⊢3\in ℝ$$
28		4re	$$⊢4\in ℝ$$
29		3lt4	$$⊢3<4$$
30	27 28 29	ltleii	$$⊢3\le 4$$
31		sq2	$$⊢2^2=4$$
32	30 31	breqtrri	$$⊢3\le 2^2$$
33		2re	$$⊢2\in ℝ$$
34		1le2	$$⊢1\le 2$$
35	17	nn0zi	$$⊢16\in \mathbb{Z}$$
36		1nn	$$⊢1\in \mathbb{N}$$
37		2nn0	$$⊢2\in {\mathbb{N}}_0$$
38		9re	$$⊢9\in ℝ$$
39		2lt9	$$⊢2<9$$
40	33 38 39	ltleii	$$⊢2\le 9$$
41	36 16 37 40	declei	$$⊢2\le 16$$
42		2z	$$⊢2\in \mathbb{Z}$$
43	42	eluz1i	$$⊢16\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(16\in \mathbb{Z}\wedge 2\le 16\right)$$
44	35 41 43	mpbir2an	$$⊢16\in {\mathbb{Z}}_{\ge 2}$$
45		leexp2a	$$⊢\left(2\in ℝ\wedge 1\le 2\wedge 16\in {\mathbb{Z}}_{\ge 2}\right)\to 2^2\le 2^{16}$$
46	33 34 44 45	mp3an	$$⊢2^2\le 2^{16}$$
47		4nn0	$$⊢4\in {\mathbb{N}}_0$$
48	31 47	eqeltri	$$⊢2^2\in {\mathbb{N}}_0$$
49	48	nn0rei	$$⊢2^2\in ℝ$$
50	37 17	nn0expcli	$$⊢2^{16}\in {\mathbb{N}}_0$$
51	50	nn0rei	$$⊢2^{16}\in ℝ$$
52	27 49 51	letri	$$⊢\left(3\le 2^2\wedge 2^2\le 2^{16}\right)\to 3\le 2^{16}$$
53	32 46 52	mp2an	$$⊢3\le 2^{16}$$
54		nn0sub	$$⊢\left(3\in {\mathbb{N}}_0\wedge 2^{16}\in {\mathbb{N}}_0\right)\to \left(3\le 2^{16}\leftrightarrow 2^{16}-3\in {\mathbb{N}}_0\right)$$
55	5 50 54	mp2an	$$⊢3\le 2^{16}\leftrightarrow 2^{16}-3\in {\mathbb{N}}_0$$
56	53 55	mpbi	$$⊢2^{16}-3\in {\mathbb{N}}_0$$
57	56	a1i	$$⊢\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\to 2^{16}-3\in {\mathbb{N}}_0$$
58		ovexd	$$⊢\left(2^{16}\in ℂ\wedge 3\in ℂ\right)\to 2^{2^{16}}-3\in \mathrm{V}$$
59	21 26 57 58	fvmptd2	Could not format ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) -> ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) = ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) ) : No typesetting found for |- ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) -> ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) = ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) ) with typecode |-
60	19 20 59	mp2an	Could not format ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) = ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) : No typesetting found for |- ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) = ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) with typecode |-
61		2exp16	$$⊢2^{16}=65536$$
62	61	oveq2i	$$⊢2^{2^{16}}=2^{65536}$$
63	62	oveq1i	$$⊢2^{2^{16}}-3=2^{65536}-3$$
64	14 60 63	3eqtri	Could not format ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 ) with typecode |-
65	4 8 64	3eqtri	Could not format ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 ) : No typesetting found for |- ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 ) with typecode |-