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 ∈ ℂ
2		6cn	⊢ 6 ∈ ℂ
3		5re	⊢ 5 ∈ ℝ
4		5pos	⊢ 0 < 5
5	3 4	gt0ne0ii	⊢ 5 ≠ 0
6		6re	⊢ 6 ∈ ℝ
7		6pos	⊢ 0 < 6
8	6 7	gt0ne0ii	⊢ 6 ≠ 0
9	1 2 5 8	subreci	⊢ ( ( 1 / 5 ) − ( 1 / 6 ) ) = ( ( 6 − 5 ) / ( 5 · 6 ) )
10		ax-1cn	⊢ 1 ∈ ℂ
11		5p1e6	⊢ ( 5 + 1 ) = 6
12	2 1 10 11	subaddrii	⊢ ( 6 − 5 ) = 1
13		6t5e30	⊢ ( 6 · 5 ) = ; 3 0
14	2 1 13	mulcomli	⊢ ( 5 · 6 ) = ; 3 0
15	12 14	oveq12i	⊢ ( ( 6 − 5 ) / ( 5 · 6 ) ) = ( 1 / ; 3 0 )
16	9 15	eqtri	⊢ ( ( 1 / 5 ) − ( 1 / 6 ) ) = ( 1 / ; 3 0 )