Metamath Proof Explorer

Theorem ackval3012

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

Ref Expression
Assertion ackval3012 
|- <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >.

Proof

Step Hyp Ref Expression
1 ackval3 
 |-  ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) )
2 oveq1 
 |-  ( n = 0 -> ( n + 3 ) = ( 0 + 3 ) )
3 3cn 
 |-  3 e. CC
4 3 addlidi 
 |-  ( 0 + 3 ) = 3
5 2 4 eqtrdi 
 |-  ( n = 0 -> ( n + 3 ) = 3 )
6 5 oveq2d 
 |-  ( n = 0 -> ( 2 ^ ( n + 3 ) ) = ( 2 ^ 3 ) )
7 6 oveq1d 
 |-  ( n = 0 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ( ( 2 ^ 3 ) - 3 ) )
8 cu2 
 |-  ( 2 ^ 3 ) = 8
9 8 oveq1i 
 |-  ( ( 2 ^ 3 ) - 3 ) = ( 8 - 3 )
10 5cn 
 |-  5 e. CC
11 5p3e8 
 |-  ( 5 + 3 ) = 8
12 11 eqcomi 
 |-  8 = ( 5 + 3 )
13 10 3 12 mvrraddi 
 |-  ( 8 - 3 ) = 5
14 9 13 eqtri 
 |-  ( ( 2 ^ 3 ) - 3 ) = 5
15 7 14 eqtrdi 
 |-  ( n = 0 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = 5 )
16 0nn0 
 |-  0 e. NN0
17 16 a1i 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 0 e. NN0 )
18 5nn0 
 |-  5 e. NN0
19 18 a1i 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 5 e. NN0 )
20 1 15 17 19 fvmptd3 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 0 ) = 5 )
21 oveq1 
 |-  ( n = 1 -> ( n + 3 ) = ( 1 + 3 ) )
22 ax-1cn 
 |-  1 e. CC
23 3p1e4 
 |-  ( 3 + 1 ) = 4
24 3 22 23 addcomli 
 |-  ( 1 + 3 ) = 4
25 21 24 eqtrdi 
 |-  ( n = 1 -> ( n + 3 ) = 4 )
26 25 oveq2d 
 |-  ( n = 1 -> ( 2 ^ ( n + 3 ) ) = ( 2 ^ 4 ) )
27 26 oveq1d 
 |-  ( n = 1 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ( ( 2 ^ 4 ) - 3 ) )
28 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
29 28 oveq1i 
 |-  ( ( 2 ^ 4 ) - 3 ) = ( ; 1 6 - 3 )
30 1nn0 
 |-  1 e. NN0
31 3nn0 
 |-  3 e. NN0
32 30 31 deccl 
 |-  ; 1 3 e. NN0
33 32 nn0cni 
 |-  ; 1 3 e. CC
34 eqid 
 |-  ; 1 3 = ; 1 3
35 3p3e6 
 |-  ( 3 + 3 ) = 6
36 30 31 31 34 35 decaddi 
 |-  ( ; 1 3 + 3 ) = ; 1 6
37 36 eqcomi 
 |-  ; 1 6 = ( ; 1 3 + 3 )
38 33 3 37 mvrraddi 
 |-  ( ; 1 6 - 3 ) = ; 1 3
39 29 38 eqtri 
 |-  ( ( 2 ^ 4 ) - 3 ) = ; 1 3
40 27 39 eqtrdi 
 |-  ( n = 1 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ; 1 3 )
41 30 a1i 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 1 e. NN0 )
42 32 a1i 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 1 3 e. NN0 )
43 1 40 41 42 fvmptd3 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 )
44 oveq1 
 |-  ( n = 2 -> ( n + 3 ) = ( 2 + 3 ) )
45 2cn 
 |-  2 e. CC
46 3p2e5 
 |-  ( 3 + 2 ) = 5
47 3 45 46 addcomli 
 |-  ( 2 + 3 ) = 5
48 44 47 eqtrdi 
 |-  ( n = 2 -> ( n + 3 ) = 5 )
49 48 oveq2d 
 |-  ( n = 2 -> ( 2 ^ ( n + 3 ) ) = ( 2 ^ 5 ) )
50 49 oveq1d 
 |-  ( n = 2 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ( ( 2 ^ 5 ) - 3 ) )
51 2exp5 
 |-  ( 2 ^ 5 ) = ; 3 2
52 51 oveq1i 
 |-  ( ( 2 ^ 5 ) - 3 ) = ( ; 3 2 - 3 )
53 2nn0 
 |-  2 e. NN0
54 9nn0 
 |-  9 e. NN0
55 53 54 deccl 
 |-  ; 2 9 e. NN0
56 55 nn0cni 
 |-  ; 2 9 e. CC
57 eqid 
 |-  ; 2 9 = ; 2 9
58 2p1e3 
 |-  ( 2 + 1 ) = 3
59 9p3e12 
 |-  ( 9 + 3 ) = ; 1 2
60 53 54 31 57 58 53 59 decaddci 
 |-  ( ; 2 9 + 3 ) = ; 3 2
61 60 eqcomi 
 |-  ; 3 2 = ( ; 2 9 + 3 )
62 56 3 61 mvrraddi 
 |-  ( ; 3 2 - 3 ) = ; 2 9
63 52 62 eqtri 
 |-  ( ( 2 ^ 5 ) - 3 ) = ; 2 9
64 50 63 eqtrdi 
 |-  ( n = 2 -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ; 2 9 )
65 53 a1i 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 2 e. NN0 )
66 55 a1i 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 2 9 e. NN0 )
67 1 64 65 66 fvmptd3 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 2 ) = ; 2 9 )
68 20 43 67 oteq123d 
 |-  ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. )
69 1 68 ax-mp 
 |-  <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >.