Metamath Proof Explorer

Theorem ackval3

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

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

Proof

Step Hyp Ref Expression
1 df-3 
 |-  3 = ( 2 + 1 )
2 1 fveq2i 
 |-  ( Ack ` 3 ) = ( Ack ` ( 2 + 1 ) )
3 2nn0 
 |-  2 e. NN0
4 ackvalsuc1mpt 
 |-  ( 2 e. NN0 -> ( Ack ` ( 2 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) )
5 3 4 ax-mp 
 |-  ( Ack ` ( 2 + 1 ) ) = ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) )
6 peano2nn0 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
7 3nn0 
 |-  3 e. NN0
8 ackval2 
 |-  ( Ack ` 2 ) = ( i e. NN0 |-> ( ( 2 x. i ) + 3 ) )
9 8 itcovalt2 
 |-  ( ( ( n + 1 ) e. NN0 /\ 3 e. NN0 ) -> ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) )
10 6 7 9 sylancl 
 |-  ( n e. NN0 -> ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) = ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) )
11 10 fveq1d 
 |-  ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ` 1 ) )
12 eqidd 
 |-  ( n e. NN0 -> ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) = ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) )
13 oveq1 
 |-  ( i = 1 -> ( i + 3 ) = ( 1 + 3 ) )
14 3cn 
 |-  3 e. CC
15 ax-1cn 
 |-  1 e. CC
16 3p1e4 
 |-  ( 3 + 1 ) = 4
17 14 15 16 addcomli 
 |-  ( 1 + 3 ) = 4
18 13 17 eqtrdi 
 |-  ( i = 1 -> ( i + 3 ) = 4 )
19 18 oveq1d 
 |-  ( i = 1 -> ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) = ( 4 x. ( 2 ^ ( n + 1 ) ) ) )
20 19 oveq1d 
 |-  ( i = 1 -> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) = ( ( 4 x. ( 2 ^ ( n + 1 ) ) ) - 3 ) )
21 20 adantl 
 |-  ( ( n e. NN0 /\ i = 1 ) -> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) = ( ( 4 x. ( 2 ^ ( n + 1 ) ) ) - 3 ) )
22 1nn0 
 |-  1 e. NN0
23 22 a1i 
 |-  ( n e. NN0 -> 1 e. NN0 )
24 ovexd 
 |-  ( n e. NN0 -> ( ( 4 x. ( 2 ^ ( n + 1 ) ) ) - 3 ) e. _V )
25 12 21 23 24 fvmptd 
 |-  ( n e. NN0 -> ( ( i e. NN0 |-> ( ( ( i + 3 ) x. ( 2 ^ ( n + 1 ) ) ) - 3 ) ) ` 1 ) = ( ( 4 x. ( 2 ^ ( n + 1 ) ) ) - 3 ) )
26 sq2 
 |-  ( 2 ^ 2 ) = 4
27 26 eqcomi 
 |-  4 = ( 2 ^ 2 )
28 27 a1i 
 |-  ( n e. NN0 -> 4 = ( 2 ^ 2 ) )
29 28 oveq1d 
 |-  ( n e. NN0 -> ( 4 x. ( 2 ^ ( n + 1 ) ) ) = ( ( 2 ^ 2 ) x. ( 2 ^ ( n + 1 ) ) ) )
30 2cnd 
 |-  ( n e. NN0 -> 2 e. CC )
31 3 a1i 
 |-  ( n e. NN0 -> 2 e. NN0 )
32 30 6 31 expaddd 
 |-  ( n e. NN0 -> ( 2 ^ ( 2 + ( n + 1 ) ) ) = ( ( 2 ^ 2 ) x. ( 2 ^ ( n + 1 ) ) ) )
33 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
34 1cnd 
 |-  ( n e. NN0 -> 1 e. CC )
35 30 33 34 add12d 
 |-  ( n e. NN0 -> ( 2 + ( n + 1 ) ) = ( n + ( 2 + 1 ) ) )
36 2p1e3 
 |-  ( 2 + 1 ) = 3
37 36 oveq2i 
 |-  ( n + ( 2 + 1 ) ) = ( n + 3 )
38 35 37 eqtrdi 
 |-  ( n e. NN0 -> ( 2 + ( n + 1 ) ) = ( n + 3 ) )
39 38 oveq2d 
 |-  ( n e. NN0 -> ( 2 ^ ( 2 + ( n + 1 ) ) ) = ( 2 ^ ( n + 3 ) ) )
40 29 32 39 3eqtr2d 
 |-  ( n e. NN0 -> ( 4 x. ( 2 ^ ( n + 1 ) ) ) = ( 2 ^ ( n + 3 ) ) )
41 40 oveq1d 
 |-  ( n e. NN0 -> ( ( 4 x. ( 2 ^ ( n + 1 ) ) ) - 3 ) = ( ( 2 ^ ( n + 3 ) ) - 3 ) )
42 11 25 41 3eqtrd 
 |-  ( n e. NN0 -> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) = ( ( 2 ^ ( n + 3 ) ) - 3 ) )
43 42 mpteq2ia 
 |-  ( n e. NN0 |-> ( ( ( IterComp ` ( Ack ` 2 ) ) ` ( n + 1 ) ) ` 1 ) ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) )
44 2 5 43 3eqtri 
 |-  ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) )