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	$$⊢M\in {\mathbb{N}}_0\to \mathrm{Ack}\left(0\right)\left(M\right)=M+1$$

Proof

Step	Hyp	Ref	Expression
1		ackval0	$$⊢\mathrm{Ack}\left(0\right)=\left(m\in {\mathbb{N}}_0⟼m+1\right)$$
2	1	a1i	$$⊢M\in {\mathbb{N}}_0\to \mathrm{Ack}\left(0\right)=\left(m\in {\mathbb{N}}_0⟼m+1\right)$$
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	$$⊢M\in {\mathbb{N}}_0\to \mathrm{Ack}\left(0\right)\left(M\right)=M+1$$