Step |
Hyp |
Ref |
Expression |
1 |
|
2t2e4 |
⊢ ( 2 · 2 ) = 4 |
2 |
1
|
eqcomi |
⊢ 4 = ( 2 · 2 ) |
3 |
2
|
oveq1i |
⊢ ( 4 ↑ 2 ) = ( ( 2 · 2 ) ↑ 2 ) |
4 |
|
2cn |
⊢ 2 ∈ ℂ |
5 |
4 4
|
sqmuli |
⊢ ( ( 2 · 2 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) |
6 |
4
|
sqvali |
⊢ ( 2 ↑ 2 ) = ( 2 · 2 ) |
7 |
|
sq2 |
⊢ ( 2 ↑ 2 ) = 4 |
8 |
6 7
|
oveq12i |
⊢ ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) = ( ( 2 · 2 ) · 4 ) |
9 |
|
4cn |
⊢ 4 ∈ ℂ |
10 |
4 4 9
|
mulassi |
⊢ ( ( 2 · 2 ) · 4 ) = ( 2 · ( 2 · 4 ) ) |
11 |
|
4t2e8 |
⊢ ( 4 · 2 ) = 8 |
12 |
9 4 11
|
mulcomli |
⊢ ( 2 · 4 ) = 8 |
13 |
12
|
oveq2i |
⊢ ( 2 · ( 2 · 4 ) ) = ( 2 · 8 ) |
14 |
8 10 13
|
3eqtri |
⊢ ( ( 2 ↑ 2 ) · ( 2 ↑ 2 ) ) = ( 2 · 8 ) |
15 |
3 5 14
|
3eqtri |
⊢ ( 4 ↑ 2 ) = ( 2 · 8 ) |