Metamath Proof Explorer

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)$