Theorem 2t6m3t4e0

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

	Ref	Expression
Assertion	2t6m3t4e0	$$⊢2\cdot 6-3\cdot 4=0$$

Proof

Step	Hyp	Ref	Expression
1		6cn	$$⊢6\in ℂ$$
2	1	2timesi	$$⊢2\cdot 6=6+6$$
3		2p2e4	$$⊢2+2=4$$
4	3	eqcomi	$$⊢4=2+2$$
5	4	oveq2i	$$⊢3\cdot 4=3\left(2+2\right)$$
6		3cn	$$⊢3\in ℂ$$
7		2cn	$$⊢2\in ℂ$$
8	6 7 7	adddii	$$⊢3\left(2+2\right)=3\cdot 2+3\cdot 2$$
9		3t2e6	$$⊢3\cdot 2=6$$
10	9 9	oveq12i	$$⊢3\cdot 2+3\cdot 2=6+6$$
11	5 8 10	3eqtri	$$⊢3\cdot 4=6+6$$
12	2 11	oveq12i	$$⊢2\cdot 6-3\cdot 4=6+6-\left(6+6\right)$$
13	1 1	addcli	$$⊢6+6\in ℂ$$
14	13	subidi	$$⊢6+6-\left(6+6\right)=0$$
15	12 14	eqtri	$$⊢2\cdot 6-3\cdot 4=0$$