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		8re	$$⊢8\in ℝ$$
3	2	recni	$$⊢8\in ℂ$$
4		4cn	$$⊢4\in ℂ$$
5		3cn	$$⊢3\in ℂ$$
6		8pos	$$⊢0<8$$
7	2 6	gt0ne0ii	$$⊢8\ne 0$$
8		3ne0	$$⊢3\ne 0$$
9	1 3 4 5 7 8	divmuldivi	$$⊢\left(\frac{1}{8}\right)\left(\frac{4}{3}\right)=\frac{1\cdot 4}{8\cdot 3}$$
10	1 4	mulcomi	$$⊢1\cdot 4=4\cdot 1$$
11		2cn	$$⊢2\in ℂ$$
12	4 11 5	mul32i	$$⊢4\cdot 2\cdot 3=4\cdot 3\cdot 2$$
13		4t2e8	$$⊢4\cdot 2=8$$
14	13	oveq1i	$$⊢4\cdot 2\cdot 3=8\cdot 3$$
15	12 14	eqtr3i	$$⊢4\cdot 3\cdot 2=8\cdot 3$$
16	4 5 11	mulassi	$$⊢4\cdot 3\cdot 2=43\cdot 2$$
17	15 16	eqtr3i	$$⊢8\cdot 3=43\cdot 2$$
18		3t2e6	$$⊢3\cdot 2=6$$
19	18	oveq2i	$$⊢43\cdot 2=4\cdot 6$$
20	17 19	eqtri	$$⊢8\cdot 3=4\cdot 6$$
21	10 20	oveq12i	$$⊢\frac{1\cdot 4}{8\cdot 3}=\frac{4\cdot 1}{4\cdot 6}$$
22	9 21	eqtri	$$⊢\left(\frac{1}{8}\right)\left(\frac{4}{3}\right)=\frac{4\cdot 1}{4\cdot 6}$$
23		6re	$$⊢6\in ℝ$$
24	23	recni	$$⊢6\in ℂ$$
25		6pos	$$⊢0<6$$
26	23 25	gt0ne0ii	$$⊢6\ne 0$$
27		4ne0	$$⊢4\ne 0$$
28		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}$$
29	1 28	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}$$
30	24 26 4 27 29	mp4an	$$⊢\frac{4\cdot 1}{4\cdot 6}=\frac{1}{6}$$
31	22 30	eqtri	$$⊢\left(\frac{1}{8}\right)\left(\frac{4}{3}\right)=\frac{1}{6}$$