8th4div3

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

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

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 \neq 0$
8		3ne0	$⊢ 3 \neq 0$
9	1 3 4 5 7 8	divmuldivi	$⊢ (\frac{1}{8}) (\frac{4}{3}) = \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 = 4 3 \cdot 2$
17	15 16	eqtr3i	$⊢ 8 \cdot 3 = 4 3 \cdot 2$
18		3t2e6	$⊢ 3 \cdot 2 = 6$
19	18	oveq2i	$⊢ 4 3 \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	$⊢ (\frac{1}{8}) (\frac{4}{3}) = \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 \neq 0$
27		4ne0	$⊢ 4 \neq 0$
28		divcan5	$⊢ (1 \in ℂ \land (6 \in ℂ \land 6 \neq 0) \land (4 \in ℂ \land 4 \neq 0)) \to \frac{4 \cdot 1}{4 \cdot 6} = \frac{1}{6}$
29	1 28	mp3an1	$⊢ ((6 \in ℂ \land 6 \neq 0) \land (4 \in ℂ \land 4 \neq 0)) \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	$⊢ (\frac{1}{8}) (\frac{4}{3}) = \frac{1}{6}$

Metamath Proof Explorer