Metamath Proof Explorer


Theorem div23

Description: A commutative/associative law for division. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion div23 ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ด ยท ๐ต ) / ๐ถ ) = ( ( ๐ด / ๐ถ ) ยท ๐ต ) )

Proof

Step Hyp Ref Expression
1 mulcom โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท ๐ต ) = ( ๐ต ยท ๐ด ) )
2 1 oveq1d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ต ) / ๐ถ ) = ( ( ๐ต ยท ๐ด ) / ๐ถ ) )
3 2 3adant3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ด ยท ๐ต ) / ๐ถ ) = ( ( ๐ต ยท ๐ด ) / ๐ถ ) )
4 divass โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ต ยท ๐ด ) / ๐ถ ) = ( ๐ต ยท ( ๐ด / ๐ถ ) ) )
5 4 3com12 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ต ยท ๐ด ) / ๐ถ ) = ( ๐ต ยท ( ๐ด / ๐ถ ) ) )
6 simp2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ๐ต โˆˆ โ„‚ )
7 divcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) โ†’ ( ๐ด / ๐ถ ) โˆˆ โ„‚ )
8 7 3expb โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ๐ด / ๐ถ ) โˆˆ โ„‚ )
9 8 3adant2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ๐ด / ๐ถ ) โˆˆ โ„‚ )
10 6 9 mulcomd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ๐ต ยท ( ๐ด / ๐ถ ) ) = ( ( ๐ด / ๐ถ ) ยท ๐ต ) )
11 3 5 10 3eqtrd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0 ) ) โ†’ ( ( ๐ด ยท ๐ต ) / ๐ถ ) = ( ( ๐ด / ๐ถ ) ยท ๐ต ) )