Metamath Proof Explorer


Theorem 2t6m3t4e0

Description: 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019)

Ref Expression
Assertion 2t6m3t4e0 ( ( 2 · 6 ) − ( 3 · 4 ) ) = 0

Proof

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