Theorem halfpm6th

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

	Ref	Expression
Assertion	halfpm6th	⊢ ( ( ( 1 / 2 ) − ( 1 / 6 ) ) = ( 1 / 3 ) ∧ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )

Proof

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