Theorem 5recm6rec

Description: One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017)

	Ref	Expression
Assertion	5recm6rec	|- ( ( 1 / 5 ) - ( 1 / 6 ) ) = ( 1 / ; 3 0 )

Proof

Step	Hyp	Ref	Expression
1		5cn	|- 5 e. CC
2		6cn	|- 6 e. CC
3		5re	|- 5 e. RR
4		5pos	|- 0 < 5
5	3 4	gt0ne0ii	|- 5 =/= 0
6		6re	|- 6 e. RR
7		6pos	|- 0 < 6
8	6 7	gt0ne0ii	|- 6 =/= 0
9	1 2 5 8	subreci	|- ( ( 1 / 5 ) - ( 1 / 6 ) ) = ( ( 6 - 5 ) / ( 5 x. 6 ) )
10		ax-1cn	|- 1 e. CC
11		5p1e6	|- ( 5 + 1 ) = 6
12	2 1 10 11	subaddrii	|- ( 6 - 5 ) = 1
13		6t5e30	|- ( 6 x. 5 ) = ; 3 0
14	2 1 13	mulcomli	|- ( 5 x. 6 ) = ; 3 0
15	12 14	oveq12i	|- ( ( 6 - 5 ) / ( 5 x. 6 ) ) = ( 1 / ; 3 0 )
16	9 15	eqtri	|- ( ( 1 / 5 ) - ( 1 / 6 ) ) = ( 1 / ; 3 0 )