Metamath Proof Explorer

Theorem ackval42

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

Ref Expression
Assertion ackval42 
|- ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 )

Proof

Step Hyp Ref Expression
1 df-4 
 |-  4 = ( 3 + 1 )
2 1 fveq2i 
 |-  ( Ack ` 4 ) = ( Ack ` ( 3 + 1 ) )
3 df-2 
 |-  2 = ( 1 + 1 )
4 2 3 fveq12i 
 |-  ( ( Ack ` 4 ) ` 2 ) = ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) )
5 3nn0 
 |-  3 e. NN0
6 1nn0 
 |-  1 e. NN0
7 ackvalsucsucval 
 |-  ( ( 3 e. NN0 /\ 1 e. NN0 ) -> ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) )
8 5 6 7 mp2an 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` ( 1 + 1 ) ) = ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) )
9 3p1e4 
 |-  ( 3 + 1 ) = 4
10 9 fveq2i 
 |-  ( Ack ` ( 3 + 1 ) ) = ( Ack ` 4 )
11 10 fveq1i 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` 1 ) = ( ( Ack ` 4 ) ` 1 )
12 ackval41a 
 |-  ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 )
13 11 12 eqtri 
 |-  ( ( Ack ` ( 3 + 1 ) ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 )
14 13 fveq2i 
 |-  ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) = ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) )
15 2cn 
 |-  2 e. CC
16 6nn0 
 |-  6 e. NN0
17 6 16 deccl 
 |-  ; 1 6 e. NN0
18 expcl 
 |-  ( ( 2 e. CC /\ ; 1 6 e. NN0 ) -> ( 2 ^ ; 1 6 ) e. CC )
19 15 17 18 mp2an 
 |-  ( 2 ^ ; 1 6 ) e. CC
20 3cn 
 |-  3 e. CC
21 ackval3 
 |-  ( Ack ` 3 ) = ( n e. NN0 |-> ( ( 2 ^ ( n + 3 ) ) - 3 ) )
22 oveq1 
 |-  ( n = ( ( 2 ^ ; 1 6 ) - 3 ) -> ( n + 3 ) = ( ( ( 2 ^ ; 1 6 ) - 3 ) + 3 ) )
23 npcan 
 |-  ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) -> ( ( ( 2 ^ ; 1 6 ) - 3 ) + 3 ) = ( 2 ^ ; 1 6 ) )
24 22 23 sylan9eqr 
 |-  ( ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) /\ n = ( ( 2 ^ ; 1 6 ) - 3 ) ) -> ( n + 3 ) = ( 2 ^ ; 1 6 ) )
25 24 oveq2d 
 |-  ( ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) /\ n = ( ( 2 ^ ; 1 6 ) - 3 ) ) -> ( 2 ^ ( n + 3 ) ) = ( 2 ^ ( 2 ^ ; 1 6 ) ) )
26 25 oveq1d 
 |-  ( ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) /\ n = ( ( 2 ^ ; 1 6 ) - 3 ) ) -> ( ( 2 ^ ( n + 3 ) ) - 3 ) = ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) )
27 3re 
 |-  3 e. RR
28 4re 
 |-  4 e. RR
29 3lt4 
 |-  3 < 4
30 27 28 29 ltleii 
 |-  3 <_ 4
31 sq2 
 |-  ( 2 ^ 2 ) = 4
32 30 31 breqtrri 
 |-  3 <_ ( 2 ^ 2 )
33 2re 
 |-  2 e. RR
34 1le2 
 |-  1 <_ 2
35 17 nn0zi 
 |-  ; 1 6 e. ZZ
36 1nn 
 |-  1 e. NN
37 2nn0 
 |-  2 e. NN0
38 9re 
 |-  9 e. RR
39 2lt9 
 |-  2 < 9
40 33 38 39 ltleii 
 |-  2 <_ 9
41 36 16 37 40 declei 
 |-  2 <_ ; 1 6
42 2z 
 |-  2 e. ZZ
43 42 eluz1i 
 |-  ( ; 1 6 e. ( ZZ>= ` 2 ) <-> ( ; 1 6 e. ZZ /\ 2 <_ ; 1 6 ) )
44 35 41 43 mpbir2an 
 |-  ; 1 6 e. ( ZZ>= ` 2 )
45 leexp2a 
 |-  ( ( 2 e. RR /\ 1 <_ 2 /\ ; 1 6 e. ( ZZ>= ` 2 ) ) -> ( 2 ^ 2 ) <_ ( 2 ^ ; 1 6 ) )
46 33 34 44 45 mp3an 
 |-  ( 2 ^ 2 ) <_ ( 2 ^ ; 1 6 )
47 4nn0 
 |-  4 e. NN0
48 31 47 eqeltri 
 |-  ( 2 ^ 2 ) e. NN0
49 48 nn0rei 
 |-  ( 2 ^ 2 ) e. RR
50 37 17 nn0expcli 
 |-  ( 2 ^ ; 1 6 ) e. NN0
51 50 nn0rei 
 |-  ( 2 ^ ; 1 6 ) e. RR
52 27 49 51 letri 
 |-  ( ( 3 <_ ( 2 ^ 2 ) /\ ( 2 ^ 2 ) <_ ( 2 ^ ; 1 6 ) ) -> 3 <_ ( 2 ^ ; 1 6 ) )
53 32 46 52 mp2an 
 |-  3 <_ ( 2 ^ ; 1 6 )
54 nn0sub 
 |-  ( ( 3 e. NN0 /\ ( 2 ^ ; 1 6 ) e. NN0 ) -> ( 3 <_ ( 2 ^ ; 1 6 ) <-> ( ( 2 ^ ; 1 6 ) - 3 ) e. NN0 ) )
55 5 50 54 mp2an 
 |-  ( 3 <_ ( 2 ^ ; 1 6 ) <-> ( ( 2 ^ ; 1 6 ) - 3 ) e. NN0 )
56 53 55 mpbi 
 |-  ( ( 2 ^ ; 1 6 ) - 3 ) e. NN0
57 56 a1i 
 |-  ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) -> ( ( 2 ^ ; 1 6 ) - 3 ) e. NN0 )
58 ovexd 
 |-  ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) -> ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) e. _V )
59 21 26 57 58 fvmptd2 
 |-  ( ( ( 2 ^ ; 1 6 ) e. CC /\ 3 e. CC ) -> ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) = ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) )
60 19 20 59 mp2an 
 |-  ( ( Ack ` 3 ) ` ( ( 2 ^ ; 1 6 ) - 3 ) ) = ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 )
61 2exp16 
 |-  ( 2 ^ ; 1 6 ) = ; ; ; ; 6 5 5 3 6
62 61 oveq2i 
 |-  ( 2 ^ ( 2 ^ ; 1 6 ) ) = ( 2 ^ ; ; ; ; 6 5 5 3 6 )
63 62 oveq1i 
 |-  ( ( 2 ^ ( 2 ^ ; 1 6 ) ) - 3 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 )
64 14 60 63 3eqtri 
 |-  ( ( Ack ` 3 ) ` ( ( Ack ` ( 3 + 1 ) ) ` 1 ) ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 )
65 4 8 64 3eqtri 
 |-  ( ( Ack ` 4 ) ` 2 ) = ( ( 2 ^ ; ; ; ; 6 5 5 3 6 ) - 3 )