Metamath Proof Explorer

Theorem ackval41a

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

Ref Expression
Assertion ackval41a 
|- ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 )

Proof

Step Hyp Ref Expression
1 df-4 
 |-  4 = ( 3 + 1 )
2 1 fveq2i 
 |-  ( Ack ` 4 ) = ( Ack ` ( 3 + 1 ) )
3 1e0p1 
 |-  1 = ( 0 + 1 )
4 2 3 fveq12i 
 |-  ( ( Ack ` 4 ) ` 1 ) = ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) )
5 3nn0 
 |-  3 e. NN0
6 0nn0 
 |-  0 e. NN0
7 ackvalsucsucval 
 |-  ( ( 3 e. NN0 /\ 0 e. NN0 ) -> ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) )
8 5 6 7 mp2an 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) )
9 3p1e4 
 |-  ( 3 + 1 ) = 4
10 9 fveq2i 
 |-  ( Ack ` ( 3 + 1 ) ) = ( Ack ` 4 )
11 10 fveq1i 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ( ( Ack ` 4 ) ` 0 )
12 ackval40 
 |-  ( ( Ack ` 4 ) ` 0 ) = ; 1 3
13 11 12 eqtri 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` 0 ) = ; 1 3
14 13 fveq2i 
 |-  ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) = ( ( Ack ` 3 ) ` ; 1 3 )
15 1nn0 
 |-  1 e. NN0
16 15 5 deccl 
 |-  ; 1 3 e. NN0
17 oveq1 
 |-  ( n = ; 1 3 -> ( n + 3 ) = ( ; 1 3 + 3 ) )
18 17 oveq2d 
 |-  ( n = ; 1 3 -> ( 2 ^ ( n + 3 ) ) = ( 2 ^ ( ; 1 3 + 3 ) ) )
19 18 oveq1d 
 |-  ( n = ; 1 3 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ( ( 2 ^ ( ; 1 3 + 3 ) ) - 3 ) )
20 eqid 
 |-  ; 1 3 = ; 1 3
21 3p3e6 
 |-  ( 3 + 3 ) = 6
22 15 5 5 20 21 decaddi 
 |-  ( ; 1 3 + 3 ) = ; 1 6
23 22 oveq2i 
 |-  ( 2 ^ ( ; 1 3 + 3 ) ) = ( 2 ^ ; 1 6 )
24 23 oveq1i 
 |-  ( ( 2 ^ ( ; 1 3 + 3 ) ) - 3 ) = ( ( 2 ^ ; 1 6 ) - 3 )
25 19 24 eqtrdi 
 |-  ( n = ; 1 3 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ( ( 2 ^ ; 1 6 ) - 3 ) )
26 ackval3 
 |-  ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) )
27 ovex 
 |-  ( ( 2 ^ ; 1 6 ) - 3 ) e. _V
28 25 26 27 fvmpt 
 |-  ( ; 1 3 e. NN0 -> ( ( Ack ` 3 ) ` ; 1 3 ) = ( ( 2 ^ ; 1 6 ) - 3 ) )
29 16 28 ax-mp 
 |-  ( ( Ack ` 3 ) ` ; 1 3 ) = ( ( 2 ^ ; 1 6 ) - 3 )
30 14 29 eqtri 
 |-  ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 0 ) ) = ( ( 2 ^ ; 1 6 ) - 3 )
31 8 30 eqtri 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` ( 0 + 1 ) ) = ( ( 2 ^ ; 1 6 ) - 3 )
32 4 31 eqtri 
 |-  ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 )