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 )