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 |
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 |