Metamath Proof Explorer


Theorem ackval1012

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

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

Proof

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