Theorem halfpm6th

Description: One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008)

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

Proof

Step	Hyp	Ref	Expression
1		3cn	$$⊢3\in ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		2cn	$$⊢2\in ℂ$$
4		3ne0	$$⊢3\ne 0$$
5		2ne0	$$⊢2\ne 0$$
6	1 1 2 3 4 5	divmuldivi	$$⊢\left(\frac{3}{3}\right)\left(\frac{1}{2}\right)=\frac{3\cdot 1}{3\cdot 2}$$
7	1 4	dividi	$$⊢\frac{3}{3}=1$$
8	7	oveq1i	$$⊢\left(\frac{3}{3}\right)\left(\frac{1}{2}\right)=1\left(\frac{1}{2}\right)$$
9		halfcn	$$⊢\frac{1}{2}\in ℂ$$
10	9	mulid2i	$$⊢1\left(\frac{1}{2}\right)=\frac{1}{2}$$
11	8 10	eqtri	$$⊢\left(\frac{3}{3}\right)\left(\frac{1}{2}\right)=\frac{1}{2}$$
12	1	mulid1i	$$⊢3\cdot 1=3$$
13		3t2e6	$$⊢3\cdot 2=6$$
14	12 13	oveq12i	$$⊢\frac{3\cdot 1}{3\cdot 2}=\frac{3}{6}$$
15	6 11 14	3eqtr3i	$$⊢\frac{1}{2}=\frac{3}{6}$$
16	15	oveq1i	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{6}\right)=\left(\frac{3}{6}\right)-\left(\frac{1}{6}\right)$$
17		6cn	$$⊢6\in ℂ$$
18		6re	$$⊢6\in ℝ$$
19		6pos	$$⊢0<6$$
20	18 19	gt0ne0ii	$$⊢6\ne 0$$
21	17 20	pm3.2i	$$⊢\left(6\in ℂ\wedge 6\ne 0\right)$$
22		divsubdir	$$⊢\left(3\in ℂ\wedge 1\in ℂ\wedge \left(6\in ℂ\wedge 6\ne 0\right)\right)\to \frac{3-1}{6}=\left(\frac{3}{6}\right)-\left(\frac{1}{6}\right)$$
23	1 2 21 22	mp3an	$$⊢\frac{3-1}{6}=\left(\frac{3}{6}\right)-\left(\frac{1}{6}\right)$$
24		3m1e2	$$⊢3-1=2$$
25	24	oveq1i	$$⊢\frac{3-1}{6}=\frac{2}{6}$$
26	3	mulid2i	$$⊢1\cdot 2=2$$
27	26 13	oveq12i	$$⊢\frac{1\cdot 2}{3\cdot 2}=\frac{2}{6}$$
28	3 5	dividi	$$⊢\frac{2}{2}=1$$
29	28	oveq2i	$$⊢\left(\frac{1}{3}\right)\left(\frac{2}{2}\right)=\left(\frac{1}{3}\right)\cdot 1$$
30	2 1 3 3 4 5	divmuldivi	$$⊢\left(\frac{1}{3}\right)\left(\frac{2}{2}\right)=\frac{1\cdot 2}{3\cdot 2}$$
31	1 4	reccli	$$⊢\frac{1}{3}\in ℂ$$
32	31	mulid1i	$$⊢\left(\frac{1}{3}\right)\cdot 1=\frac{1}{3}$$
33	29 30 32	3eqtr3i	$$⊢\frac{1\cdot 2}{3\cdot 2}=\frac{1}{3}$$
34	25 27 33	3eqtr2i	$$⊢\frac{3-1}{6}=\frac{1}{3}$$
35	16 23 34	3eqtr2i	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{6}\right)=\frac{1}{3}$$
36	1 2 17 20	divdiri	$$⊢\frac{3+1}{6}=\left(\frac{3}{6}\right)+\left(\frac{1}{6}\right)$$
37		df-4	$$⊢4=3+1$$
38	37	oveq1i	$$⊢\frac{4}{6}=\frac{3+1}{6}$$
39	15	oveq1i	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)=\left(\frac{3}{6}\right)+\left(\frac{1}{6}\right)$$
40	36 38 39	3eqtr4ri	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)=\frac{4}{6}$$
41		2t2e4	$$⊢2\cdot 2=4$$
42	41 13	oveq12i	$$⊢\frac{2\cdot 2}{3\cdot 2}=\frac{4}{6}$$
43	28	oveq2i	$$⊢\left(\frac{2}{3}\right)\left(\frac{2}{2}\right)=\left(\frac{2}{3}\right)\cdot 1$$
44	3 1 3 3 4 5	divmuldivi	$$⊢\left(\frac{2}{3}\right)\left(\frac{2}{2}\right)=\frac{2\cdot 2}{3\cdot 2}$$
45	3 1 4	divcli	$$⊢\frac{2}{3}\in ℂ$$
46	45	mulid1i	$$⊢\left(\frac{2}{3}\right)\cdot 1=\frac{2}{3}$$
47	43 44 46	3eqtr3i	$$⊢\frac{2\cdot 2}{3\cdot 2}=\frac{2}{3}$$
48	40 42 47	3eqtr2i	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)=\frac{2}{3}$$
49	35 48	pm3.2i	$$⊢\left(\left(\frac{1}{2}\right)-\left(\frac{1}{6}\right)=\frac{1}{3}\wedge \left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)=\frac{2}{3}\right)$$