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