Step |
Hyp |
Ref |
Expression |
1 |
|
ackval42 |
⊢ ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( 2 ↑ ; ; ; ; 6 5 5 3 6 ) − 3 ) |
2 |
|
sq2 |
⊢ ( 2 ↑ 2 ) = 4 |
3 |
2
|
oveq2i |
⊢ ( 2 ↑ ( 2 ↑ 2 ) ) = ( 2 ↑ 4 ) |
4 |
|
2exp4 |
⊢ ( 2 ↑ 4 ) = ; 1 6 |
5 |
3 4
|
eqtri |
⊢ ( 2 ↑ ( 2 ↑ 2 ) ) = ; 1 6 |
6 |
5
|
oveq2i |
⊢ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) = ( 2 ↑ ; 1 6 ) |
7 |
|
2exp16 |
⊢ ( 2 ↑ ; 1 6 ) = ; ; ; ; 6 5 5 3 6 |
8 |
6 7
|
eqtr2i |
⊢ ; ; ; ; 6 5 5 3 6 = ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) |
9 |
8
|
oveq2i |
⊢ ( 2 ↑ ; ; ; ; 6 5 5 3 6 ) = ( 2 ↑ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) ) |
10 |
9
|
oveq1i |
⊢ ( ( 2 ↑ ; ; ; ; 6 5 5 3 6 ) − 3 ) = ( ( 2 ↑ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) ) − 3 ) |
11 |
1 10
|
eqtri |
⊢ ( ( Ack ‘ 4 ) ‘ 2 ) = ( ( 2 ↑ ( 2 ↑ ( 2 ↑ ( 2 ↑ 2 ) ) ) ) − 3 ) |