Theorem halfpm6th

Description: One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008) (Proof shortened by SN, 22-Oct-2025)

	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		3ne0	⊢ 3 ≠ 0
3	1 2	reccli	⊢ ( 1 / 3 ) ∈ ℂ
4		6cn	⊢ 6 ∈ ℂ
5		6re	⊢ 6 ∈ ℝ
6		6pos	⊢ 0 < 6
7	5 6	gt0ne0ii	⊢ 6 ≠ 0
8	4 7	reccli	⊢ ( 1 / 6 ) ∈ ℂ
9		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
10	3 9	pncan3i	⊢ ( ( 1 / 3 ) + ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( 1 / 2 )
11		halfthird	⊢ ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )
12	11	oveq2i	⊢ ( ( 1 / 3 ) + ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( ( 1 / 3 ) + ( 1 / 6 ) )
13	10 12	eqtr3i	⊢ ( 1 / 2 ) = ( ( 1 / 3 ) + ( 1 / 6 ) )
14	3 8 13	mvrraddi	⊢ ( ( 1 / 2 ) − ( 1 / 6 ) ) = ( 1 / 3 )
15	11	oveq2i	⊢ ( ( 1 / 2 ) + ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( ( 1 / 2 ) + ( 1 / 6 ) )
16	9 9 3	addsubassi	⊢ ( ( ( 1 / 2 ) + ( 1 / 2 ) ) − ( 1 / 3 ) ) = ( ( 1 / 2 ) + ( ( 1 / 2 ) − ( 1 / 3 ) ) )
17		2cn	⊢ 2 ∈ ℂ
18	17 1 2	divcli	⊢ ( 2 / 3 ) ∈ ℂ
19		ax-1cn	⊢ 1 ∈ ℂ
20		2halves	⊢ ( 1 ∈ ℂ → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
21	19 20	ax-mp	⊢ ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
22		2p1e3	⊢ ( 2 + 1 ) = 3
23	22	oveq1i	⊢ ( ( 2 + 1 ) / 3 ) = ( 3 / 3 )
24	1 2	dividi	⊢ ( 3 / 3 ) = 1
25	23 24	eqtri	⊢ ( ( 2 + 1 ) / 3 ) = 1
26	17 19 1 2	divdiri	⊢ ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
27	21 25 26	3eqtr2i	⊢ ( ( 1 / 2 ) + ( 1 / 2 ) ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
28	18 3 27	mvrraddi	⊢ ( ( ( 1 / 2 ) + ( 1 / 2 ) ) − ( 1 / 3 ) ) = ( 2 / 3 )
29	16 28	eqtr3i	⊢ ( ( 1 / 2 ) + ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( 2 / 3 )
30	15 29	eqtr3i	⊢ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 )
31	14 30	pm3.2i	⊢ ( ( ( 1 / 2 ) − ( 1 / 6 ) ) = ( 1 / 3 ) ∧ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )