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