Theorem ackval1

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

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

Proof

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