Metamath Proof Explorer

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	$⊢ M \in ℕ_{0} \to Ack (M + 1) (0) = Ack (M) (1)$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		ackvalsuc1	$⊢ (M \in ℕ_{0} \land 0 \in ℕ_{0}) \to Ack (M + 1) (0) = IterComp (Ack (M)) (0 + 1) (1)$
3	1 2	mpan2	$⊢ M \in ℕ_{0} \to Ack (M + 1) (0) = IterComp (Ack (M)) (0 + 1) (1)$
4		0p1e1	$⊢ 0 + 1 = 1$
5	4	a1i	$⊢ M \in ℕ_{0} \to 0 + 1 = 1$
6	5	fveq2d	$⊢ M \in ℕ_{0} \to IterComp (Ack (M)) (0 + 1) = IterComp (Ack (M)) (1)$
7		ackfnnn0	$⊢ M \in ℕ_{0} \to Ack (M) Fn ℕ_{0}$
8		fnfun	$⊢ Ack (M) Fn ℕ_{0} \to Fun Ack (M)$
9		funrel	$⊢ Fun Ack (M) \to Rel Ack (M)$
10	7 8 9	3syl	$⊢ M \in ℕ_{0} \to Rel Ack (M)$
11		fvex	$⊢ Ack (M) \in V$
12		itcoval1	$⊢ (Rel Ack (M) \land Ack (M) \in V) \to IterComp (Ack (M)) (1) = Ack (M)$
13	10 11 12	sylancl	$⊢ M \in ℕ_{0} \to IterComp (Ack (M)) (1) = Ack (M)$
14	6 13	eqtrd	$⊢ M \in ℕ_{0} \to IterComp (Ack (M)) (0 + 1) = Ack (M)$
15	14	fveq1d	$⊢ M \in ℕ_{0} \to IterComp (Ack (M)) (0 + 1) (1) = Ack (M) (1)$
16	3 15	eqtrd	$⊢ M \in ℕ_{0} \to Ack (M + 1) (0) = Ack (M) (1)$