Theorem ackval0val

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

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

Proof

Step	Hyp	Ref	Expression
1		ackval0	Could not format ( Ack ` 0 ) = ( m e. NN0 |-> ( m + 1 ) ) : No typesetting found for |- ( Ack ` 0 ) = ( m e. NN0 |-> ( m + 1 ) ) with typecode |-
2	1	a1i	Could not format ( M e. NN0 -> ( Ack ` 0 ) = ( m e. NN0 |-> ( m + 1 ) ) ) : No typesetting found for |- ( M e. NN0 -> ( Ack ` 0 ) = ( m e. NN0 |-> ( m + 1 ) ) ) with typecode |-
3		oveq1	$$⊢m=M\to m+1=M+1$$
4	3	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge m=M\right)\to m+1=M+1$$
5		id	$$⊢M\in {\mathbb{N}}_0\to M\in {\mathbb{N}}_0$$
6		peano2nn0	$$⊢M\in {\mathbb{N}}_0\to M+1\in {\mathbb{N}}_0$$
7	2 4 5 6	fvmptd	Could not format ( M e. NN0 -> ( ( Ack ` 0 ) ` M ) = ( M + 1 ) ) : No typesetting found for |- ( M e. NN0 -> ( ( Ack ` 0 ) ` M ) = ( M + 1 ) ) with typecode |-