ackvalsucsucval

Description: The Ackermann function at the successors. This is the third equation of Péter's definition of the Ackermann function. (Contributed by AV, 8-May-2024)

		Ref	Expression
	Assertion	ackvalsucsucval	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M + 1) (N + 1) = Ack (M) (Ack (M + 1) (N))$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
2		ackvalsuc1	$⊢ (M \in ℕ_{0} \land N + 1 \in ℕ_{0}) \to Ack (M + 1) (N + 1) = IterComp (Ack (M)) (N + 1 + 1) (1)$
3	1 2	sylan2	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M + 1) (N + 1) = IterComp (Ack (M)) (N + 1 + 1) (1)$
4		fvexd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M) \in V$
5	1	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N + 1 \in ℕ_{0}$
6		eqidd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N + 1) = IterComp (Ack (M)) (N + 1)$
7		itcovalsucov	$⊢ (Ack (M) \in V \land N + 1 \in ℕ_{0} \land IterComp (Ack (M)) (N + 1) = IterComp (Ack (M)) (N + 1)) \to IterComp (Ack (M)) (N + 1 + 1) = Ack (M) \circ IterComp (Ack (M)) (N + 1)$
8	4 5 6 7	syl3anc	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N + 1 + 1) = Ack (M) \circ IterComp (Ack (M)) (N + 1)$
9	8	fveq1d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N + 1 + 1) (1) = (Ack (M) \circ IterComp (Ack (M)) (N + 1)) (1)$
10		ackfnnn0	$⊢ M \in ℕ_{0} \to Ack (M) Fn ℕ_{0}$
11	10	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M) Fn ℕ_{0}$
12		nn0ex	$⊢ ℕ_{0} \in V$
13	12	a1i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ℕ_{0} \in V$
14		ackendofnn0	$⊢ M \in ℕ_{0} \to Ack (M) : ℕ_{0} ⟶ ℕ_{0}$
15	14	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M) : ℕ_{0} ⟶ ℕ_{0}$
16		simpr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℕ_{0}$
17	13 15 16	itcovalendof	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N) : ℕ_{0} ⟶ ℕ_{0}$
18	17	ffnd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N) Fn ℕ_{0}$
19	17	frnd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ran IterComp (Ack (M)) (N) \subseteq ℕ_{0}$
20		fnco	$⊢ (Ack (M) Fn ℕ_{0} \land IterComp (Ack (M)) (N) Fn ℕ_{0} \land ran IterComp (Ack (M)) (N) \subseteq ℕ_{0}) \to (Ack (M) \circ IterComp (Ack (M)) (N)) Fn ℕ_{0}$
21	11 18 19 20	syl3anc	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (Ack (M) \circ IterComp (Ack (M)) (N)) Fn ℕ_{0}$
22		eqidd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N) = IterComp (Ack (M)) (N)$
23		itcovalsucov	$⊢ (Ack (M) \in V \land N \in ℕ_{0} \land IterComp (Ack (M)) (N) = IterComp (Ack (M)) (N)) \to IterComp (Ack (M)) (N + 1) = Ack (M) \circ IterComp (Ack (M)) (N)$
24	4 16 22 23	syl3anc	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N + 1) = Ack (M) \circ IterComp (Ack (M)) (N)$
25	24	fneq1d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (IterComp (Ack (M)) (N + 1) Fn ℕ_{0} \leftrightarrow (Ack (M) \circ IterComp (Ack (M)) (N)) Fn ℕ_{0})$
26	21 25	mpbird	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N + 1) Fn ℕ_{0}$
27		1nn0	$⊢ 1 \in ℕ_{0}$
28		fvco2	$⊢ (IterComp (Ack (M)) (N + 1) Fn ℕ_{0} \land 1 \in ℕ_{0}) \to (Ack (M) \circ IterComp (Ack (M)) (N + 1)) (1) = Ack (M) (IterComp (Ack (M)) (N + 1) (1))$
29	26 27 28	sylancl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (Ack (M) \circ IterComp (Ack (M)) (N + 1)) (1) = Ack (M) (IterComp (Ack (M)) (N + 1) (1))$
30	9 29	eqtrd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N + 1 + 1) (1) = Ack (M) (IterComp (Ack (M)) (N + 1) (1))$
31		ackvalsuc1	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M + 1) (N) = IterComp (Ack (M)) (N + 1) (1)$
32	31	eqcomd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to IterComp (Ack (M)) (N + 1) (1) = Ack (M + 1) (N)$
33	32	fveq2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M) (IterComp (Ack (M)) (N + 1) (1)) = Ack (M) (Ack (M + 1) (N))$
34	3 30 33	3eqtrd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to Ack (M + 1) (N + 1) = Ack (M) (Ack (M + 1) (N))$

Metamath Proof Explorer

Theorem ackvalsucsucval

Proof