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 Could not format assertion : No typesetting found for |- <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. with typecode |-

Proof

Step Hyp Ref Expression
1 ackval3 Could not format ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) : No typesetting found for |- ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) with typecode |-
2 oveq1 n = 0 n + 3 = 0 + 3
3 3cn 3
4 3 addid2i 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
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 0
17 16 a1i Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 0 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 0 e. NN0 ) with typecode |-
18 5nn0 5 0
19 18 a1i Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 5 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 5 e. NN0 ) with typecode |-
20 1 15 17 19 fvmptd3 Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 0 ) = 5 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 0 ) = 5 ) with typecode |-
21 oveq1 n = 1 n + 3 = 1 + 3
22 ax-1cn 1
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 = 16
29 28 oveq1i 2 4 3 = 16 3
30 1nn0 1 0
31 3nn0 3 0
32 30 31 deccl 13 0
33 32 nn0cni 13
34 eqid 13 = 13
35 3p3e6 3 + 3 = 6
36 30 31 31 34 35 decaddi 13 + 3 = 16
37 36 eqcomi 16 = 13 + 3
38 33 3 37 mvrraddi 16 3 = 13
39 29 38 eqtri 2 4 3 = 13
40 27 39 eqtrdi n = 1 2 n + 3 3 = 13
41 30 a1i Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 1 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 1 e. NN0 ) with typecode |-
42 32 a1i Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 1 3 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 1 3 e. NN0 ) with typecode |-
43 1 40 41 42 fvmptd3 Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 1 ) = ; 1 3 ) with typecode |-
44 oveq1 n = 2 n + 3 = 2 + 3
45 2cn 2
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 = 32
52 51 oveq1i 2 5 3 = 32 3
53 2nn0 2 0
54 9nn0 9 0
55 53 54 deccl 29 0
56 55 nn0cni 29
57 eqid 29 = 29
58 2p1e3 2 + 1 = 3
59 9p3e12 9 + 3 = 12
60 53 54 31 57 58 53 59 decaddci 29 + 3 = 32
61 60 eqcomi 32 = 29 + 3
62 56 3 61 mvrraddi 32 3 = 29
63 52 62 eqtri 2 5 3 = 29
64 50 63 eqtrdi n = 2 2 n + 3 3 = 29
65 53 a1i Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 2 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> 2 e. NN0 ) with typecode |-
66 55 a1i Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 2 9 e. NN0 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ; 2 9 e. NN0 ) with typecode |-
67 1 64 65 66 fvmptd3 Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 2 ) = ; 2 9 ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> ( ( Ack ` 3 ) ` 2 ) = ; 2 9 ) with typecode |-
68 20 43 67 oteq123d Could not format ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. ) : No typesetting found for |- ( ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) ) -> <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. ) with typecode |-
69 1 68 ax-mp Could not format <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. : No typesetting found for |- <. ( ( Ack ` 3 ) ` 0 ) , ( ( Ack ` 3 ) ` 1 ) , ( ( Ack ` 3 ) ` 2 ) >. = <. 5 , ; 1 3 , ; 2 9 >. with typecode |-