Metamath Proof Explorer

Theorem ackval2012

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

Ref Expression
Assertion ackval2012 
|- <. ( ( Ack ` 2 ) ` 0 ) , ( ( Ack ` 2 ) ` 1 ) , ( ( Ack ` 2 ) ` 2 ) >. = <. 3 , 5 , 7 >.

Proof

Step Hyp Ref Expression
1 ackval2 
 |-  ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) )
2 oveq2 
 |-  ( n = 0 -> ( 2 x. n ) = ( 2 x. 0 ) )
3 2 oveq1d 
 |-  ( n = 0 -> ( ( 2 x. n ) + 3 ) = ( ( 2 x. 0 ) + 3 ) )
4 2t0e0 
 |-  ( 2 x. 0 ) = 0
5 4 oveq1i 
 |-  ( ( 2 x. 0 ) + 3 ) = ( 0 + 3 )
6 3cn 
 |-  3 e. CC
7 6 addid2i 
 |-  ( 0 + 3 ) = 3
8 5 7 eqtri 
 |-  ( ( 2 x. 0 ) + 3 ) = 3
9 3 8 eqtrdi 
 |-  ( n = 0 -> ( ( 2 x. n ) + 3 ) = 3 )
10 0nn0 
 |-  0 e. NN0
11 10 a1i 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 0 e. NN0 )
12 3nn0 
 |-  3 e. NN0
13 12 a1i 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 3 e. NN0 )
14 1 9 11 13 fvmptd3 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 0 ) = 3 )
15 oveq2 
 |-  ( n = 1 -> ( 2 x. n ) = ( 2 x. 1 ) )
16 15 oveq1d 
 |-  ( n = 1 -> ( ( 2 x. n ) + 3 ) = ( ( 2 x. 1 ) + 3 ) )
17 2t1e2 
 |-  ( 2 x. 1 ) = 2
18 17 oveq1i 
 |-  ( ( 2 x. 1 ) + 3 ) = ( 2 + 3 )
19 2cn 
 |-  2 e. CC
20 3p2e5 
 |-  ( 3 + 2 ) = 5
21 6 19 20 addcomli 
 |-  ( 2 + 3 ) = 5
22 18 21 eqtri 
 |-  ( ( 2 x. 1 ) + 3 ) = 5
23 16 22 eqtrdi 
 |-  ( n = 1 -> ( ( 2 x. n ) + 3 ) = 5 )
24 1nn0 
 |-  1 e. NN0
25 24 a1i 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 1 e. NN0 )
26 5nn0 
 |-  5 e. NN0
27 26 a1i 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 5 e. NN0 )
28 1 23 25 27 fvmptd3 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 1 ) = 5 )
29 oveq2 
 |-  ( n = 2 -> ( 2 x. n ) = ( 2 x. 2 ) )
30 29 oveq1d 
 |-  ( n = 2 -> ( ( 2 x. n ) + 3 ) = ( ( 2 x. 2 ) + 3 ) )
31 2t2e4 
 |-  ( 2 x. 2 ) = 4
32 31 oveq1i 
 |-  ( ( 2 x. 2 ) + 3 ) = ( 4 + 3 )
33 4p3e7 
 |-  ( 4 + 3 ) = 7
34 32 33 eqtri 
 |-  ( ( 2 x. 2 ) + 3 ) = 7
35 30 34 eqtrdi 
 |-  ( n = 2 -> ( ( 2 x. n ) + 3 ) = 7 )
36 2nn0 
 |-  2 e. NN0
37 36 a1i 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 2 e. NN0 )
38 7nn0 
 |-  7 e. NN0
39 38 a1i 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> 7 e. NN0 )
40 1 35 37 39 fvmptd3 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> ( ( Ack ` 2 ) ` 2 ) = 7 )
41 14 28 40 oteq123d 
 |-  ( ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) ) -> <. ( ( Ack ` 2 ) ` 0 ) , ( ( Ack ` 2 ) ` 1 ) , ( ( Ack ` 2 ) ` 2 ) >. = <. 3 , 5 , 7 >. )
42 1 41 ax-mp 
 |-  <. ( ( Ack ` 2 ) ` 0 ) , ( ( Ack ` 2 ) ` 1 ) , ( ( Ack ` 2 ) ` 2 ) >. = <. 3 , 5 , 7 >.