Theorem halfthird

Description: Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015)

	Ref	Expression
Assertion	halfthird	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{3}\right)=\frac{1}{6}$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		3cn	$$⊢3\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4		3ne0	$$⊢3\ne 0$$
5	1 2 3 4	subreci	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{3}\right)=\frac{3-2}{2\cdot 3}$$
6		ax-1cn	$$⊢1\in ℂ$$
7		2p1e3	$$⊢2+1=3$$
8	2 1 6 7	subaddrii	$$⊢3-2=1$$
9		3t2e6	$$⊢3\cdot 2=6$$
10	2 1 9	mulcomli	$$⊢2\cdot 3=6$$
11	8 10	oveq12i	$$⊢\frac{3-2}{2\cdot 3}=\frac{1}{6}$$
12	5 11	eqtri	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{3}\right)=\frac{1}{6}$$