Theorem ackvalsuc0val

Description: The Ackermann function at a successor (of the first argument). This is the second equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		ackvalsuc1	Could not format ( ( M e. NN0 /\ 0 e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) ) : No typesetting found for |- ( ( M e. NN0 /\ 0 e. NN0 ) -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) ) with typecode |-
3	1 2	mpan2	Could not format ( M e. NN0 -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) ) : No typesetting found for |- ( M e. NN0 -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) ) with typecode |-
4		0p1e1	$$⊢0+1=1$$
5	4	a1i	$$⊢M\in {\mathbb{N}}_0\to 0+1=1$$
6	5	fveq2d	Could not format ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` 1 ) ) : No typesetting found for |- ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) = ( ( IterComp ` ( Ack ` M ) ) ` 1 ) ) with typecode |-
7		ackfnnn0	Could not format ( M e. NN0 -> ( Ack ` M ) Fn NN0 ) : No typesetting found for |- ( M e. NN0 -> ( Ack ` M ) Fn NN0 ) with typecode |-
8		fnfun	Could not format ( ( Ack ` M ) Fn NN0 -> Fun ( Ack ` M ) ) : No typesetting found for |- ( ( Ack ` M ) Fn NN0 -> Fun ( Ack ` M ) ) with typecode |-
9		funrel	Could not format ( Fun ( Ack ` M ) -> Rel ( Ack ` M ) ) : No typesetting found for |- ( Fun ( Ack ` M ) -> Rel ( Ack ` M ) ) with typecode |-
10	7 8 9	3syl	Could not format ( M e. NN0 -> Rel ( Ack ` M ) ) : No typesetting found for |- ( M e. NN0 -> Rel ( Ack ` M ) ) with typecode |-
11		fvex	Could not format ( Ack ` M ) e. _V : No typesetting found for |- ( Ack ` M ) e. _V with typecode |-
12		itcoval1	Could not format ( ( Rel ( Ack ` M ) /\ ( Ack ` M ) e. _V ) -> ( ( IterComp ` ( Ack ` M ) ) ` 1 ) = ( Ack ` M ) ) : No typesetting found for |- ( ( Rel ( Ack ` M ) /\ ( Ack ` M ) e. _V ) -> ( ( IterComp ` ( Ack ` M ) ) ` 1 ) = ( Ack ` M ) ) with typecode |-
13	10 11 12	sylancl	Could not format ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` 1 ) = ( Ack ` M ) ) : No typesetting found for |- ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` 1 ) = ( Ack ` M ) ) with typecode |-
14	6 13	eqtrd	Could not format ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) = ( Ack ` M ) ) : No typesetting found for |- ( M e. NN0 -> ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) = ( Ack ` M ) ) with typecode |-
15	14	fveq1d	Could not format ( M e. NN0 -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) = ( ( Ack ` M ) ` 1 ) ) : No typesetting found for |- ( M e. NN0 -> ( ( ( IterComp ` ( Ack ` M ) ) ` ( 0 + 1 ) ) ` 1 ) = ( ( Ack ` M ) ` 1 ) ) with typecode |-
16	3 15	eqtrd	Could not format ( M e. NN0 -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( Ack ` M ) ` 1 ) ) : No typesetting found for |- ( M e. NN0 -> ( ( Ack ` ( M + 1 ) ) ` 0 ) = ( ( Ack ` M ) ` 1 ) ) with typecode |-