# Metamath Proof Explorer

## 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}$