This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 1 / 8 ) · ( 4 / 3 ) ) = ( 1 / 6 )

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 8re ⊢ 8 ∈ ℝ
3 2 recni ⊢ 8 ∈ ℂ
4 4cn ⊢ 4 ∈ ℂ
5 3cn ⊢ 3 ∈ ℂ
6 8pos ⊢ 0 < 8
7 2 6 gt0ne0ii ⊢ 8 ≠ 0
8 3ne0 ⊢ 3 ≠ 0
9 1 3 4 5 7 8 divmuldivi ⊢ ( ( 1 / 8 ) · ( 4 / 3 ) ) = ( ( 1 · 4 ) / ( 8 · 3 ) )
10 1 4 mulcomi ⊢ ( 1 · 4 ) = ( 4 · 1 )
11 2cn ⊢ 2 ∈ ℂ
12 4 11 5 mul32i ⊢ ( ( 4 · 2 ) · 3 ) = ( ( 4 · 3 ) · 2 )
13 4t2e8 ⊢ ( 4 · 2 ) = 8
14 13 oveq1i ⊢ ( ( 4 · 2 ) · 3 ) = ( 8 · 3 )
15 12 14 eqtr3i ⊢ ( ( 4 · 3 ) · 2 ) = ( 8 · 3 )
16 4 5 11 mulassi ⊢ ( ( 4 · 3 ) · 2 ) = ( 4 · ( 3 · 2 ) )
17 15 16 eqtr3i ⊢ ( 8 · 3 ) = ( 4 · ( 3 · 2 ) )
18 3t2e6 ⊢ ( 3 · 2 ) = 6
19 18 oveq2i ⊢ ( 4 · ( 3 · 2 ) ) = ( 4 · 6 )
20 17 19 eqtri ⊢ ( 8 · 3 ) = ( 4 · 6 )
21 10 20 oveq12i ⊢ ( ( 1 · 4 ) / ( 8 · 3 ) ) = ( ( 4 · 1 ) / ( 4 · 6 ) )
22 9 21 eqtri ⊢ ( ( 1 / 8 ) · ( 4 / 3 ) ) = ( ( 4 · 1 ) / ( 4 · 6 ) )
23 6re ⊢ 6 ∈ ℝ
24 23 recni ⊢ 6 ∈ ℂ
25 6pos ⊢ 0 < 6
26 23 25 gt0ne0ii ⊢ 6 ≠ 0
27 4ne0 ⊢ 4 ≠ 0
28 divcan5 ⊢ ( ( 1 ∈ ℂ ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 4 · 1 ) / ( 4 · 6 ) ) = ( 1 / 6 ) )
29 1 28 mp3an1 ⊢ ( ( ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 4 · 1 ) / ( 4 · 6 ) ) = ( 1 / 6 ) )
30 24 26 4 27 29 mp4an ⊢ ( ( 4 · 1 ) / ( 4 · 6 ) ) = ( 1 / 6 )
31 22 30 eqtri ⊢ ( ( 1 / 8 ) · ( 4 / 3 ) ) = ( 1 / 6 )