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

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 8cn 
 |-  8 e. CC
3 4cn 
 |-  4 e. CC
4 3cn 
 |-  3 e. CC
5 8re 
 |-  8 e. RR
6 8pos 
 |-  0 < 8
7 5 6 gt0ne0ii 
 |-  8 =/= 0
8 3ne0 
 |-  3 =/= 0
9 1 2 3 4 7 8 divmuldivi 
 |-  ( ( 1 / 8 ) x. ( 4 / 3 ) ) = ( ( 1 x. 4 ) / ( 8 x. 3 ) )
10 1 3 mulcomi 
 |-  ( 1 x. 4 ) = ( 4 x. 1 )
11 2cn 
 |-  2 e. CC
12 3 11 4 mulassi 
 |-  ( ( 4 x. 2 ) x. 3 ) = ( 4 x. ( 2 x. 3 ) )
13 4t2e8 
 |-  ( 4 x. 2 ) = 8
14 13 oveq1i 
 |-  ( ( 4 x. 2 ) x. 3 ) = ( 8 x. 3 )
15 2t3e6 
 |-  ( 2 x. 3 ) = 6
16 15 oveq2i 
 |-  ( 4 x. ( 2 x. 3 ) ) = ( 4 x. 6 )
17 12 14 16 3eqtr3i 
 |-  ( 8 x. 3 ) = ( 4 x. 6 )
18 10 17 oveq12i 
 |-  ( ( 1 x. 4 ) / ( 8 x. 3 ) ) = ( ( 4 x. 1 ) / ( 4 x. 6 ) )
19 9 18 eqtri 
 |-  ( ( 1 / 8 ) x. ( 4 / 3 ) ) = ( ( 4 x. 1 ) / ( 4 x. 6 ) )
20 6cn 
 |-  6 e. CC
21 6re 
 |-  6 e. RR
22 6pos 
 |-  0 < 6
23 21 22 gt0ne0ii 
 |-  6 =/= 0
24 4ne0 
 |-  4 =/= 0
25 divcan5 
 |-  ( ( 1 e. CC /\ ( 6 e. CC /\ 6 =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( 4 x. 1 ) / ( 4 x. 6 ) ) = ( 1 / 6 ) )
26 1 25 mp3an1 
 |-  ( ( ( 6 e. CC /\ 6 =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( 4 x. 1 ) / ( 4 x. 6 ) ) = ( 1 / 6 ) )
27 20 23 3 24 26 mp4an 
 |-  ( ( 4 x. 1 ) / ( 4 x. 6 ) ) = ( 1 / 6 )
28 19 27 eqtri 
 |-  ( ( 1 / 8 ) x. ( 4 / 3 ) ) = ( 1 / 6 )