Theorem halfthird

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

	Ref	Expression
Assertion	halfthird	⊢ ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2		3cn	⊢ 3 ∈ ℂ
3		2ne0	⊢ 2 ≠ 0
4		3ne0	⊢ 3 ≠ 0
5	1 2 3 4	subreci	⊢ ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( ( 3 − 2 ) / ( 2 · 3 ) )
6		ax-1cn	⊢ 1 ∈ ℂ
7		2p1e3	⊢ ( 2 + 1 ) = 3
8	2 1 6 7	subaddrii	⊢ ( 3 − 2 ) = 1
9		3t2e6	⊢ ( 3 · 2 ) = 6
10	2 1 9	mulcomli	⊢ ( 2 · 3 ) = 6
11	8 10	oveq12i	⊢ ( ( 3 − 2 ) / ( 2 · 3 ) ) = ( 1 / 6 )
12	5 11	eqtri	⊢ ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )