This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divcan8d

Description: A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses divcan8d.a 
|- ( ph -> A e. CC )
divcan8d.b 
|- ( ph -> B e. CC )
divcan8d.a0 
|- ( ph -> A =/= 0 )
divcan8d.b0 
|- ( ph -> B =/= 0 )
Assertion divcan8d 
|- ( ph -> ( B / ( A x. B ) ) = ( 1 / A ) )

Proof

Step Hyp Ref Expression
1 divcan8d.a 
 |-  ( ph -> A e. CC )
2 divcan8d.b 
 |-  ( ph -> B e. CC )
3 divcan8d.a0 
 |-  ( ph -> A =/= 0 )
4 divcan8d.b0 
 |-  ( ph -> B =/= 0 )
5 1 2 mulcld 
 |-  ( ph -> ( A x. B ) e. CC )
6 1 2 3 4 mulne0d 
 |-  ( ph -> ( A x. B ) =/= 0 )
7 1 2 6 mulne0bbd 
 |-  ( ph -> B =/= 0 )
8 2 5 2 6 7 divcan7d 
 |-  ( ph -> ( ( B / B ) / ( ( A x. B ) / B ) ) = ( B / ( A x. B ) ) )
9 8 eqcomd 
 |-  ( ph -> ( B / ( A x. B ) ) = ( ( B / B ) / ( ( A x. B ) / B ) ) )
10 2 4 dividd 
 |-  ( ph -> ( B / B ) = 1 )
11 1 2 4 divcan4d 
 |-  ( ph -> ( ( A x. B ) / B ) = A )
12 10 11 oveq12d 
 |-  ( ph -> ( ( B / B ) / ( ( A x. B ) / B ) ) = ( 1 / A ) )
13 eqidd 
 |-  ( ph -> ( 1 / A ) = ( 1 / A ) )
14 9 12 13 3eqtrd 
 |-  ( ph -> ( B / ( A x. B ) ) = ( 1 / A ) )