Theorem 5recm6rec

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

	Ref	Expression
Assertion	5recm6rec	$$⊢\left(\frac{1}{5}\right)-\left(\frac{1}{6}\right)=\frac{1}{30}$$

Proof

Step	Hyp	Ref	Expression
1		5cn	$$⊢5\in ℂ$$
2		6cn	$$⊢6\in ℂ$$
3		5re	$$⊢5\in ℝ$$
4		5pos	$$⊢0<5$$
5	3 4	gt0ne0ii	$$⊢5\ne 0$$
6		6re	$$⊢6\in ℝ$$
7		6pos	$$⊢0<6$$
8	6 7	gt0ne0ii	$$⊢6\ne 0$$
9	1 2 5 8	subreci	$$⊢\left(\frac{1}{5}\right)-\left(\frac{1}{6}\right)=\frac{6-5}{5\cdot 6}$$
10		ax-1cn	$$⊢1\in ℂ$$
11		5p1e6	$$⊢5+1=6$$
12	2 1 10 11	subaddrii	$$⊢6-5=1$$
13		6t5e30	$$⊢6\cdot 5=30$$
14	2 1 13	mulcomli	$$⊢5\cdot 6=30$$
15	12 14	oveq12i	$$⊢\frac{6-5}{5\cdot 6}=\frac{1}{30}$$
16	9 15	eqtri	$$⊢\left(\frac{1}{5}\right)-\left(\frac{1}{6}\right)=\frac{1}{30}$$