Metamath Proof Explorer

Theorem ackval1

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

Ref Expression
Assertion ackval1 
|- ( Ack ` 1 ) = ( n e. NN0 |-> ( n + 2 ) )

Proof

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