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		8cn	⊢ 8 ∈ ℂ
3		4cn	⊢ 4 ∈ ℂ
4		3cn	⊢ 3 ∈ ℂ
5		8re	⊢ 8 ∈ ℝ
6		8pos	⊢ 0 < 8
7	5 6	gt0ne0ii	⊢ 8 ≠ 0
8		3ne0	⊢ 3 ≠ 0
9	1 2 3 4 7 8	divmuldivi	⊢ ( ( 1 / 8 ) · ( 4 / 3 ) ) = ( ( 1 · 4 ) / ( 8 · 3 ) )
10	1 3	mulcomi	⊢ ( 1 · 4 ) = ( 4 · 1 )
11		2cn	⊢ 2 ∈ ℂ
12	3 11 4	mulassi	⊢ ( ( 4 · 2 ) · 3 ) = ( 4 · ( 2 · 3 ) )
13		4t2e8	⊢ ( 4 · 2 ) = 8
14	13	oveq1i	⊢ ( ( 4 · 2 ) · 3 ) = ( 8 · 3 )
15		2t3e6	⊢ ( 2 · 3 ) = 6
16	15	oveq2i	⊢ ( 4 · ( 2 · 3 ) ) = ( 4 · 6 )
17	12 14 16	3eqtr3i	⊢ ( 8 · 3 ) = ( 4 · 6 )
18	10 17	oveq12i	⊢ ( ( 1 · 4 ) / ( 8 · 3 ) ) = ( ( 4 · 1 ) / ( 4 · 6 ) )
19	9 18	eqtri	⊢ ( ( 1 / 8 ) · ( 4 / 3 ) ) = ( ( 4 · 1 ) / ( 4 · 6 ) )
20		6cn	⊢ 6 ∈ ℂ
21		6re	⊢ 6 ∈ ℝ
22		6pos	⊢ 0 < 6
23	21 22	gt0ne0ii	⊢ 6 ≠ 0
24		4ne0	⊢ 4 ≠ 0
25		divcan5	⊢ ( ( 1 ∈ ℂ ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 4 · 1 ) / ( 4 · 6 ) ) = ( 1 / 6 ) )
26	1 25	mp3an1	⊢ ( ( ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 4 · 1 ) / ( 4 · 6 ) ) = ( 1 / 6 ) )
27	20 23 3 24 26	mp4an	⊢ ( ( 4 · 1 ) / ( 4 · 6 ) ) = ( 1 / 6 )
28	19 27	eqtri	⊢ ( ( 1 / 8 ) · ( 4 / 3 ) ) = ( 1 / 6 )