Metamath Proof Explorer


Theorem divmuldivd

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses div1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
divcld.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
divmuld.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
divmuldivd.4 โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„‚ )
divmuldivd.5 โŠข ( ๐œ‘ โ†’ ๐ต โ‰  0 )
divmuldivd.6 โŠข ( ๐œ‘ โ†’ ๐ท โ‰  0 )
Assertion divmuldivd ( ๐œ‘ โ†’ ( ( ๐ด / ๐ต ) ยท ( ๐ถ / ๐ท ) ) = ( ( ๐ด ยท ๐ถ ) / ( ๐ต ยท ๐ท ) ) )

Proof

Step Hyp Ref Expression
1 div1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
2 divcld.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
3 divmuld.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
4 divmuldivd.4 โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„‚ )
5 divmuldivd.5 โŠข ( ๐œ‘ โ†’ ๐ต โ‰  0 )
6 divmuldivd.6 โŠข ( ๐œ‘ โ†’ ๐ท โ‰  0 )
7 2 5 jca โŠข ( ๐œ‘ โ†’ ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) )
8 4 6 jca โŠข ( ๐œ‘ โ†’ ( ๐ท โˆˆ โ„‚ โˆง ๐ท โ‰  0 ) )
9 divmuldiv โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โˆง ( ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โˆง ( ๐ท โˆˆ โ„‚ โˆง ๐ท โ‰  0 ) ) ) โ†’ ( ( ๐ด / ๐ต ) ยท ( ๐ถ / ๐ท ) ) = ( ( ๐ด ยท ๐ถ ) / ( ๐ต ยท ๐ท ) ) )
10 1 3 7 8 9 syl22anc โŠข ( ๐œ‘ โ†’ ( ( ๐ด / ๐ต ) ยท ( ๐ถ / ๐ท ) ) = ( ( ๐ด ยท ๐ถ ) / ( ๐ต ยท ๐ท ) ) )