Theorem ackval2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	fveq2i	Could not format ( Ack ` 2 ) = ( Ack ` ( 1 + 1 ) ) : No typesetting found for |- ( Ack ` 2 ) = ( Ack ` ( 1 + 1 ) ) with typecode |-
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		ackvalsuc1mpt	Could not format ( 1 e. NN0 -> ( Ack ` ( 1 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for |- ( 1 e. NN0 -> ( Ack ` ( 1 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode |-
5	3 4	ax-mp	Could not format ( Ack ` ( 1 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) : No typesetting found for |- ( Ack ` ( 1 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) with typecode |-
6		peano2nn0	$$⊢n\in {\mathbb{N}}_0\to n+1\in {\mathbb{N}}_0$$
7		2nn0	$$⊢2\in {\mathbb{N}}_0$$
8		ackval1	Could not format ( Ack ` 1 ) = ( i e. NN0 |-> ( i + 2 ) ) : No typesetting found for |- ( Ack ` 1 ) = ( i e. NN0 |-> ( i + 2 ) ) with typecode |-
9	8	itcovalpc	Could not format ( ( ( n + 1 ) e. NN0 /\ 2 e. NN0 ) -> ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ) : No typesetting found for |- ( ( ( n + 1 ) e. NN0 /\ 2 e. NN0 ) -> ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ) with typecode |-
10	6 7 9	sylancl	Could not format ( n e. NN0 -> ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ) : No typesetting found for |- ( n e. NN0 -> ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ) with typecode |-
11	10	fveq1d	Could not format ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ` 1 ) ) : No typesetting found for |- ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ` 1 ) ) with typecode |-
12		eqidd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)=\left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)$$
13		oveq1	$$⊢i=1\to i+2\left(n+1\right)=1+2\left(n+1\right)$$
14	13	adantl	$$⊢\left(n\in {\mathbb{N}}_0\wedge i=1\right)\to i+2\left(n+1\right)=1+2\left(n+1\right)$$
15	3	a1i	$$⊢n\in {\mathbb{N}}_0\to 1\in {\mathbb{N}}_0$$
16		ovexd	$$⊢n\in {\mathbb{N}}_0\to 1+2\left(n+1\right)\in \mathrm{V}$$
17	12 14 15 16	fvmptd	$$⊢n\in {\mathbb{N}}_0\to \left(i\in {\mathbb{N}}_0⟼i+2\left(n+1\right)\right)\left(1\right)=1+2\left(n+1\right)$$
18		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
19		1cnd	$$⊢n\in ℂ\to 1\in ℂ$$
20		2cnd	$$⊢n\in ℂ\to 2\in ℂ$$
21		peano2cn	$$⊢n\in ℂ\to n+1\in ℂ$$
22	20 21	mulcld	$$⊢n\in ℂ\to 2\left(n+1\right)\in ℂ$$
23	19 22	addcomd	$$⊢n\in ℂ\to 1+2\left(n+1\right)=2\left(n+1\right)+1$$
24		id	$$⊢n\in ℂ\to n\in ℂ$$
25	20 24 19	adddid	$$⊢n\in ℂ\to 2\left(n+1\right)=2n+2\cdot 1$$
26	25	oveq1d	$$⊢n\in ℂ\to 2\left(n+1\right)+1=2n+2\cdot 1+1$$
27	20 24	mulcld	$$⊢n\in ℂ\to 2n\in ℂ$$
28	20 19	mulcld	$$⊢n\in ℂ\to 2\cdot 1\in ℂ$$
29	27 28 19	addassd	$$⊢n\in ℂ\to 2n+2\cdot 1+1=2n+2\cdot 1+1$$
30		2t1e2	$$⊢2\cdot 1=2$$
31	30	oveq1i	$$⊢2\cdot 1+1=2+1$$
32		2p1e3	$$⊢2+1=3$$
33	31 32	eqtri	$$⊢2\cdot 1+1=3$$
34	33	a1i	$$⊢n\in ℂ\to 2\cdot 1+1=3$$
35	34	oveq2d	$$⊢n\in ℂ\to 2n+2\cdot 1+1=2n+3$$
36	29 35	eqtrd	$$⊢n\in ℂ\to 2n+2\cdot 1+1=2n+3$$
37	23 26 36	3eqtrd	$$⊢n\in ℂ\to 1+2\left(n+1\right)=2n+3$$
38	18 37	syl	$$⊢n\in {\mathbb{N}}_0\to 1+2\left(n+1\right)=2n+3$$
39	11 17 38	3eqtrd	Could not format ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( 2 x. n ) + 3 ) ) : No typesetting found for |- ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( 2 x. n ) + 3 ) ) with typecode |-
40	39	mpteq2ia	Could not format ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) : No typesetting found for |- ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) with typecode |-
41	2 5 40	3eqtri	Could not format ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) : No typesetting found for |- ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) with typecode |-