Step |
Hyp |
Ref |
Expression |
1 |
|
6cn |
⊢ 6 ∈ ℂ |
2 |
1
|
2timesi |
⊢ ( 2 · 6 ) = ( 6 + 6 ) |
3 |
|
2p2e4 |
⊢ ( 2 + 2 ) = 4 |
4 |
3
|
eqcomi |
⊢ 4 = ( 2 + 2 ) |
5 |
4
|
oveq2i |
⊢ ( 3 · 4 ) = ( 3 · ( 2 + 2 ) ) |
6 |
|
3cn |
⊢ 3 ∈ ℂ |
7 |
|
2cn |
⊢ 2 ∈ ℂ |
8 |
6 7 7
|
adddii |
⊢ ( 3 · ( 2 + 2 ) ) = ( ( 3 · 2 ) + ( 3 · 2 ) ) |
9 |
|
3t2e6 |
⊢ ( 3 · 2 ) = 6 |
10 |
9 9
|
oveq12i |
⊢ ( ( 3 · 2 ) + ( 3 · 2 ) ) = ( 6 + 6 ) |
11 |
5 8 10
|
3eqtri |
⊢ ( 3 · 4 ) = ( 6 + 6 ) |
12 |
2 11
|
oveq12i |
⊢ ( ( 2 · 6 ) − ( 3 · 4 ) ) = ( ( 6 + 6 ) − ( 6 + 6 ) ) |
13 |
1 1
|
addcli |
⊢ ( 6 + 6 ) ∈ ℂ |
14 |
13
|
subidi |
⊢ ( ( 6 + 6 ) − ( 6 + 6 ) ) = 0 |
15 |
12 14
|
eqtri |
⊢ ( ( 2 · 6 ) − ( 3 · 4 ) ) = 0 |