Metamath Proof Explorer

Theorem xdivmul

Description: Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016)

Ref Expression
Assertion xdivmul 
|- ( ( A e. RR* /\ B e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> ( ( A /e C ) = B <-> ( C *e B ) = A ) )

Proof

Step Hyp Ref Expression
1 xdivval 
 |-  ( ( A e. RR* /\ C e. RR /\ C =/= 0 ) -> ( A /e C ) = ( iota_ x e. RR* ( C *e x ) = A ) )
2 1 3expb 
 |-  ( ( A e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> ( A /e C ) = ( iota_ x e. RR* ( C *e x ) = A ) )
3 2 3adant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> ( A /e C ) = ( iota_ x e. RR* ( C *e x ) = A ) )
4 3 eqeq1d 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> ( ( A /e C ) = B <-> ( iota_ x e. RR* ( C *e x ) = A ) = B ) )
5 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> B e. RR* )
6 xreceu 
 |-  ( ( A e. RR* /\ C e. RR /\ C =/= 0 ) -> E! x e. RR* ( C *e x ) = A )
7 6 3expb 
 |-  ( ( A e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> E! x e. RR* ( C *e x ) = A )
8 7 3adant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> E! x e. RR* ( C *e x ) = A )
9 oveq2 
 |-  ( x = B -> ( C *e x ) = ( C *e B ) )
10 9 eqeq1d 
 |-  ( x = B -> ( ( C *e x ) = A <-> ( C *e B ) = A ) )
11 10 riota2 
 |-  ( ( B e. RR* /\ E! x e. RR* ( C *e x ) = A ) -> ( ( C *e B ) = A <-> ( iota_ x e. RR* ( C *e x ) = A ) = B ) )
12 5 8 11 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> ( ( C *e B ) = A <-> ( iota_ x e. RR* ( C *e x ) = A ) = B ) )
13 4 12 bitr4d 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR /\ C =/= 0 ) ) -> ( ( A /e C ) = B <-> ( C *e B ) = A ) )