Metamath Proof Explorer

Theorem ackval40

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

Ref Expression
Assertion ackval40 
|- ( ( Ack ` 4 ) ` 0 ) = ; 1 3

Proof

Step Hyp Ref Expression
1 df-4 
 |-  4 = ( 3 + 1 )
2 1 fveq2i 
 |-  ( Ack ` 4 ) = ( Ack ` ( 3 + 1 ) )
3 2 fveq1i 
 |-  ( ( Ack ` 4 ) ` 0 ) = ( ( Ack ` ( 3 + 1 ) ) ` 0 )
4 3nn0 
 |-  3 e. NN0
5 ackvalsuc0val 
 |-  ( 3 e. NN0 -> ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 3 ) ` 1 ) )
6 4 5 ax-mp 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 3 ) ` 1 )
7 ackval3012 
 |-  <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >.
8 fvex 
 |-  ( ( Ack ` 3 ) ` 0 ) e. _V
9 fvex 
 |-  ( ( Ack ` 3 ) ` 1 ) e. _V
10 fvex 
 |-  ( ( Ack ` 3 ) ` 2 ) e. _V
11 8 9 10 otth 
 |-  ( <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. <-> ( ( ( Ack ` 3 ) ` 0 ) = 5 /\ ( ( Ack ` 3 ) ` 1 ) = ; 1 3 /\ ( ( Ack ` 3 ) ` 2 ) = ; 2 9 ) )
12 11 simp2bi 
 |-  ( <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 )
13 7 12 ax-mp 
 |-  ( ( Ack ` 3 ) ` 1 ) = ; 1 3
14 3 6 13 3eqtri 
 |-  ( ( Ack ` 4 ) ` 0 ) = ; 1 3