Theorem ackval50

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

	Ref	Expression
Assertion	ackval50	⊢ ( ( Ack ‘ 5 ) ‘ 0 ) = ; ; ; ; 6 5 5 3 3

Proof

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 ∈ ℕ0
5		ackvalsuc0val	⊢ ( 4 ∈ ℕ0 → ( ( Ack ‘ ( 4 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 4 ) ‘ 1 ) )
6	4 5	ax-mp	⊢ ( ( Ack ‘ ( 4 + 1 ) ) ‘ 0 ) = ( ( Ack ‘ 4 ) ‘ 1 )
7		ackval41	⊢ ( ( Ack ‘ 4 ) ‘ 1 ) = ; ; ; ; 6 5 5 3 3
8	3 6 7	3eqtri	⊢ ( ( Ack ‘ 5 ) ‘ 0 ) = ; ; ; ; 6 5 5 3 3