Theorem 8th4div3

Description: An eighth of four thirds is a sixth. (Contributed by Paul Chapman, 24-Nov-2007)

	Ref	Expression
Assertion	8th4div3	$$⊢\left(\frac{1}{8}\right)\left(\frac{4}{3}\right)=\frac{1}{6}$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		8cn	$$⊢8\in ℂ$$
3		4cn	$$⊢4\in ℂ$$
4		3cn	$$⊢3\in ℂ$$
5		8re	$$⊢8\in ℝ$$
6		8pos	$$⊢0<8$$
7	5 6	gt0ne0ii	$$⊢8\ne 0$$
8		3ne0	$$⊢3\ne 0$$
9	1 2 3 4 7 8	divmuldivi	$$⊢\left(\frac{1}{8}\right)\left(\frac{4}{3}\right)=\frac{1\cdot 4}{8\cdot 3}$$
10	1 3	mulcomi	$$⊢1\cdot 4=4\cdot 1$$
11		2cn	$$⊢2\in ℂ$$
12	3 11 4	mulassi	$$⊢4\cdot 2\cdot 3=42\cdot 3$$
13		4t2e8	$$⊢4\cdot 2=8$$
14	13	oveq1i	$$⊢4\cdot 2\cdot 3=8\cdot 3$$
15		2t3e6	$$⊢2\cdot 3=6$$
16	15	oveq2i	$$⊢42\cdot 3=4\cdot 6$$
17	12 14 16	3eqtr3i	$$⊢8\cdot 3=4\cdot 6$$
18	10 17	oveq12i	$$⊢\frac{1\cdot 4}{8\cdot 3}=\frac{4\cdot 1}{4\cdot 6}$$
19	9 18	eqtri	$$⊢\left(\frac{1}{8}\right)\left(\frac{4}{3}\right)=\frac{4\cdot 1}{4\cdot 6}$$
20		6cn	$$⊢6\in ℂ$$
21		6re	$$⊢6\in ℝ$$
22		6pos	$$⊢0<6$$
23	21 22	gt0ne0ii	$$⊢6\ne 0$$
24		4ne0	$$⊢4\ne 0$$
25		divcan5	$$⊢\left(1\in ℂ\wedge \left(6\in ℂ\wedge 6\ne 0\right)\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{4\cdot 1}{4\cdot 6}=\frac{1}{6}$$
26	1 25	mp3an1	$$⊢\left(\left(6\in ℂ\wedge 6\ne 0\right)\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{4\cdot 1}{4\cdot 6}=\frac{1}{6}$$
27	20 23 3 24 26	mp4an	$$⊢\frac{4\cdot 1}{4\cdot 6}=\frac{1}{6}$$
28	19 27	eqtri	$$⊢\left(\frac{1}{8}\right)\left(\frac{4}{3}\right)=\frac{1}{6}$$