Theorem ackval3

Description: The Ackermann function at 3. (Contributed by AV, 7-May-2024)

	Ref	Expression
Assertion	ackval3	Could not format assertion : No typesetting found for |- ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-3	$$⊢3=2+1$$
2	1	fveq2i	Could not format ( Ack ` 3 ) = ( Ack ` ( 2 + 1 ) ) : No typesetting found for |- ( Ack ` 3 ) = ( Ack ` ( 2 + 1 ) ) with typecode |-
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4		ackvalsuc1mpt	Could not format ( 2 e. NN0 -> ( Ack ` ( 2 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( 2 e. NN0 -> ( Ack ` ( 2 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-
5	3 4	ax-mp	Could not format ( Ack ` ( 2 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) : No typesetting found for |- ( Ack ` ( 2 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) with typecode |-
6		peano2nn0	$$⊢n\in {\mathbb{N}}_0\to n+1\in {\mathbb{N}}_0$$
7		3nn0	$$⊢3\in {\mathbb{N}}_0$$
8		ackval2	Could not format ( Ack ` 2 ) = ( i e. NN0 |-> ( ( 2 x. i ) + 3 ) ) : No typesetting found for |- ( Ack ` 2 ) = ( i e. NN0 |-> ( ( 2 x. i ) + 3 ) ) with typecode |-
9	8	itcovalt2	Could not format ( ( ( n + 1 ) e. NN0 /\ 3 e. NN0 ) -> ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ) : No typesetting found for |- ( ( ( n + 1 ) e. NN0 /\ 3 e. NN0 ) -> ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ) with typecode |-
10	6 7 9	sylancl	Could not format ( n e. NN0 -> ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ) : No typesetting found for |- ( n e. NN0 -> ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ) with typecode |-
11	10	fveq1d	Could not format ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ` 1 ) ) : No typesetting found for |- ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ` 1 ) ) with typecode |-
12		eqidd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)=\left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)$$
13		oveq1	$$⊢i=1\to i+3=1+3$$
14		3cn	$$⊢3\in ℂ$$
15		ax-1cn	$$⊢1\in ℂ$$
16		3p1e4	$$⊢3+1=4$$
17	14 15 16	addcomli	$$⊢1+3=4$$
18	13 17	eqtrdi	$$⊢i=1\to i+3=4$$
19	18	oveq1d	$$⊢i=1\to \left(i+3\right)2^{n+1}=42^{n+1}$$
20	19	oveq1d	$$⊢i=1\to \left(i+3\right)2^{n+1}-3=42^{n+1}-3$$
21	20	adantl	$$⊢\left(n\in {\mathbb{N}}_0\wedge i=1\right)\to \left(i+3\right)2^{n+1}-3=42^{n+1}-3$$
22		1nn0	$$⊢1\in {\mathbb{N}}_0$$
23	22	a1i	$$⊢n\in {\mathbb{N}}_0\to 1\in {\mathbb{N}}_0$$
24		ovexd	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}-3\in \mathrm{V}$$
25	12 21 23 24	fvmptd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼\left(i+3\right)2^{n+1}-3\right)\left(1\right)=42^{n+1}-3$$
26		sq2	$$⊢2^2=4$$
27	26	eqcomi	$$⊢4=2^2$$
28	27	a1i	$$⊢n\in {\mathbb{N}}_0\to 4=2^2$$
29	28	oveq1d	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}=2^2{2}^{n+1}$$
30		2cnd	$$⊢n\in {\mathbb{N}}_0\to 2\in ℂ$$
31	3	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
32	30 6 31	expaddd	$$⊢n\in {\mathbb{N}}_0\to 2^{2+n+1}=2^2{2}^{n+1}$$
33		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
34		1cnd	$$⊢n\in {\mathbb{N}}_0\to 1\in ℂ$$
35	30 33 34	add12d	$$⊢n\in {\mathbb{N}}_0\to 2+n+1=n+2+1$$
36		2p1e3	$$⊢2+1=3$$
37	36	oveq2i	$$⊢n+2+1=n+3$$
38	35 37	eqtrdi	$$⊢n\in {\mathbb{N}}_0\to 2+n+1=n+3$$
39	38	oveq2d	$$⊢n\in {\mathbb{N}}_0\to 2^{2+n+1}=2^{n+3}$$
40	29 32 39	3eqtr2d	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}=2^{n+3}$$
41	40	oveq1d	$$⊢n\in {\mathbb{N}}_0\to 42^{n+1}-3=2^{n+3}-3$$
42	11 25 41	3eqtrd	Could not format ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( 2 ^ ( n + 3 ) ) - 3 ) ) : No typesetting found for |- ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( 2 ^ ( n + 3 ) ) - 3 ) ) with typecode |-
43	42	mpteq2ia	Could not format ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) : No typesetting found for |- ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) with typecode |-
44	2 5 43	3eqtri	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 |-