Metamath Proof Explorer

Theorem ackval2

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

Ref Expression
Assertion ackval2 
|- ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) )

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1 fveq2i 
 |-  ( Ack ` 2 ) = ( Ack ` ( 1 + 1 ) )
3 1nn0 
 |-  1 e. NN0
4 ackvalsuc1mpt 
 |-  ( 1 e. NN0 -> ( Ack ` ( 1 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) )
5 3 4 ax-mp 
 |-  ( Ack ` ( 1 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) )
6 peano2nn0 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
7 2nn0 
 |-  2 e. NN0
8 ackval1 
 |-  ( Ack ` 1 ) = ( i e. NN0 |-> ( i + 2 ) )
9 8 itcovalpc 
 |-  ( ( ( n + 1 ) e. NN0 /\ 2 e. NN0 ) -> ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) )
10 6 7 9 sylancl 
 |-  ( n e. NN0 -> ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) )
11 10 fveq1d 
 |-  ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ` 1 ) )
12 eqidd 
 |-  ( n e. NN0 -> ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) = ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) )
13 oveq1 
 |-  ( i = 1 -> ( i + ( 2 x. ( n + 1 ) ) ) = ( 1 + ( 2 x. ( n + 1 ) ) ) )
14 13 adantl 
 |-  ( ( n e. NN0 /\ i = 1 ) -> ( i + ( 2 x. ( n + 1 ) ) ) = ( 1 + ( 2 x. ( n + 1 ) ) ) )
15 3 a1i 
 |-  ( n e. NN0 -> 1 e. NN0 )
16 ovexd 
 |-  ( n e. NN0 -> ( 1 + ( 2 x. ( n + 1 ) ) ) e. _V )
17 12 14 15 16 fvmptd 
 |-  ( n e. NN0 -> ( ( i e. NN0 |-> ( i + ( 2 x. ( n + 1 ) ) ) ) ` 1 ) = ( 1 + ( 2 x. ( n + 1 ) ) ) )
18 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
19 1cnd 
 |-  ( n e. CC -> 1 e. CC )
20 2cnd 
 |-  ( n e. CC -> 2 e. CC )
21 peano2cn 
 |-  ( n e. CC -> ( n + 1 ) e. CC )
22 20 21 mulcld 
 |-  ( n e. CC -> ( 2 x. ( n + 1 ) ) e. CC )
23 19 22 addcomd 
 |-  ( n e. CC -> ( 1 + ( 2 x. ( n + 1 ) ) ) = ( ( 2 x. ( n + 1 ) ) + 1 ) )
24 id 
 |-  ( n e. CC -> n e. CC )
25 20 24 19 adddid 
 |-  ( n e. CC -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
26 25 oveq1d 
 |-  ( n e. CC -> ( ( 2 x. ( n + 1 ) ) + 1 ) = ( ( ( 2 x. n ) + ( 2 x. 1 ) ) + 1 ) )
27 20 24 mulcld 
 |-  ( n e. CC -> ( 2 x. n ) e. CC )
28 20 19 mulcld 
 |-  ( n e. CC -> ( 2 x. 1 ) e. CC )
29 27 28 19 addassd 
 |-  ( n e. CC -> ( ( ( 2 x. n ) + ( 2 x. 1 ) ) + 1 ) = ( ( 2 x. n ) + ( ( 2 x. 1 ) + 1 ) ) )
30 2t1e2 
 |-  ( 2 x. 1 ) = 2
31 30 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
32 2p1e3 
 |-  ( 2 + 1 ) = 3
33 31 32 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
34 33 a1i 
 |-  ( n e. CC -> ( ( 2 x. 1 ) + 1 ) = 3 )
35 34 oveq2d 
 |-  ( n e. CC -> ( ( 2 x. n ) + ( ( 2 x. 1 ) + 1 ) ) = ( ( 2 x. n ) + 3 ) )
36 29 35 eqtrd 
 |-  ( n e. CC -> ( ( ( 2 x. n ) + ( 2 x. 1 ) ) + 1 ) = ( ( 2 x. n ) + 3 ) )
37 23 26 36 3eqtrd 
 |-  ( n e. CC -> ( 1 + ( 2 x. ( n + 1 ) ) ) = ( ( 2 x. n ) + 3 ) )
38 18 37 syl 
 |-  ( n e. NN0 -> ( 1 + ( 2 x. ( n + 1 ) ) ) = ( ( 2 x. n ) + 3 ) )
39 11 17 38 3eqtrd 
 |-  ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( 2 x. n ) + 3 ) )
40 39 mpteq2ia 
 |-  ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 1 ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) )
41 2 5 40 3eqtri 
 |-  ( Ack ` 2 ) = ( n e. NN0 |-> ( ( 2 x. n ) + 3 ) )