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 e. CC
2		3cn	|- 3 e. CC
3		2ne0	|- 2 =/= 0
4		3ne0	|- 3 =/= 0
5	1 2 3 4	subreci	|- ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( ( 3 - 2 ) / ( 2 x. 3 ) )
6		ax-1cn	|- 1 e. CC
7		2p1e3	|- ( 2 + 1 ) = 3
8	2 1 6 7	subaddrii	|- ( 3 - 2 ) = 1
9		3t2e6	|- ( 3 x. 2 ) = 6
10	2 1 9	mulcomli	|- ( 2 x. 3 ) = 6
11	8 10	oveq12i	|- ( ( 3 - 2 ) / ( 2 x. 3 ) ) = ( 1 / 6 )
12	5 11	eqtri	|- ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 )