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=0n+1=0+1
3 0p1e1 0+1=1
4 2 3 eqtrdi n=0n+1=1
5 0nn0 00
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 10
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=1n+1=1+1
11 1p1e2 1+1=2
12 10 11 eqtrdi n=1n+1=2
13 2nn0 20
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=2n+1=2+1
17 2p1e3 2+1=3
18 16 17 eqtrdi n=2n+1=3
19 3nn0 30
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 |-