Metamath Proof Explorer


Theorem ackval0012

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

Ref Expression
Assertion ackval0012 Could not format assertion : No typesetting found for |- <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. with typecode |-

Proof

Step Hyp Ref Expression
1 ackval0 Could not format ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) : No typesetting found for |- ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) with typecode |-
2 oveq1 n = 0 n + 1 = 0 + 1
3 0p1e1 0 + 1 = 1
4 2 3 eqtrdi n = 0 n + 1 = 1
5 0nn0 0 0
6 5 a1i Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 0 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 0 e. NN0 ) with typecode |-
7 1nn0 1 0
8 7 a1i Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 1 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 1 e. NN0 ) with typecode |-
9 1 4 6 8 fvmptd3 Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 0 ) = 1 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 0 ) = 1 ) with typecode |-
10 oveq1 n = 1 n + 1 = 1 + 1
11 1p1e2 1 + 1 = 2
12 10 11 eqtrdi n = 1 n + 1 = 2
13 2nn0 2 0
14 13 a1i Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 2 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 2 e. NN0 ) with typecode |-
15 1 12 8 14 fvmptd3 Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 1 ) = 2 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 1 ) = 2 ) with typecode |-
16 oveq1 n = 2 n + 1 = 2 + 1
17 2p1e3 2 + 1 = 3
18 16 17 eqtrdi n = 2 n + 1 = 3
19 3nn0 3 0
20 19 a1i Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 3 e. NN0 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> 3 e. NN0 ) with typecode |-
21 1 18 14 20 fvmptd3 Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 2 ) = 3 ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> ( ( Ack ` 0 ) ` 2 ) = 3 ) with typecode |-
22 9 15 21 oteq123d Could not format ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. ) : No typesetting found for |- ( ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) -> <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. ) with typecode |-
23 1 22 ax-mp Could not format <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. : No typesetting found for |- <. ( ( Ack ` 0 ) ` 0 ) , ( ( Ack ` 0 ) ` 1 ) , ( ( Ack ` 0 ) ` 2 ) >. = <. 1 , 2 , 3 >. with typecode |-