Metamath Proof Explorer

Theorem ackval41

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

Ref Expression
Assertion ackval41 
|- ( ( Ack ` 4 ) ` 1 ) = ; ; ; ; 6 5 5 3 3

Proof

Step Hyp Ref Expression
1 ackval41a 
 |-  ( ( Ack ` 4 ) ` 1 ) = ( ( 2 ^ ; 1 6 ) - 3 )
2 6nn0 
 |-  6 e. NN0
3 5nn0 
 |-  5 e. NN0
4 2 3 deccl 
 |-  ; 6 5 e. NN0
5 4 3 deccl 
 |-  ; ; 6 5 5 e. NN0
6 3nn0 
 |-  3 e. NN0
7 5 6 deccl 
 |-  ; ; ; 6 5 5 3 e. NN0
8 2exp16 
 |-  ( 2 ^ ; 1 6 ) = ; ; ; ; 6 5 5 3 6
9 3p1e4 
 |-  ( 3 + 1 ) = 4
10 eqid 
 |-  ; ; ; 6 5 5 3 = ; ; ; 6 5 5 3
11 5 6 9 10 decsuc 
 |-  ( ; ; ; 6 5 5 3 + 1 ) = ; ; ; 6 5 5 4
12 3cn 
 |-  3 e. CC
13 gbpart6 
 |-  6 = ( 3 + 3 )
14 12 12 13 mvrraddi 
 |-  ( 6 - 3 ) = 3
15 7 2 6 8 11 14 decsubi 
 |-  ( ( 2 ^ ; 1 6 ) - 3 ) = ; ; ; ; 6 5 5 3 3
16 1 15 eqtri 
 |-  ( ( Ack ` 4 ) ` 1 ) = ; ; ; ; 6 5 5 3 3