This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackval50

Description: The Ackermann function at (5,0). (Contributed by AV, 9-May-2024)

		Ref	Expression
	Assertion	ackval50	$⊢ Ack (5) (0) = 65533$

Step	Hyp	Ref	Expression
1		df-5	$⊢ 5 = 4 + 1$
2	1	fveq2i	$⊢ Ack (5) = Ack (4 + 1)$
3	2	fveq1i	$⊢ Ack (5) (0) = Ack (4 + 1) (0)$
4		4nn0	$⊢ 4 \in ℕ_{0}$
5		ackvalsuc0val	$⊢ 4 \in ℕ_{0} \to Ack (4 + 1) (0) = Ack (4) (1)$
6	4 5	ax-mp	$⊢ Ack (4 + 1) (0) = Ack (4) (1)$
7		ackval41	$⊢ Ack (4) (1) = 65533$
8	3 6 7	3eqtri	$⊢ Ack (5) (0) = 65533$