Description: Relationship between division and multiplication. (Contributed by NM, 8-May-1999) (Revised by Mario Carneiro, 17-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | divclz.1 | |- A e. CC |
|
divclz.2 | |- B e. CC |
||
divmulz.3 | |- C e. CC |
||
Assertion | divmulzi | |- ( B =/= 0 -> ( ( A / B ) = C <-> ( B x. C ) = A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divclz.1 | |- A e. CC |
|
2 | divclz.2 | |- B e. CC |
|
3 | divmulz.3 | |- C e. CC |
|
4 | divmul | |- ( ( A e. CC /\ C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = C <-> ( B x. C ) = A ) ) |
|
5 | 1 3 4 | mp3an12 | |- ( ( B e. CC /\ B =/= 0 ) -> ( ( A / B ) = C <-> ( B x. C ) = A ) ) |
6 | 2 5 | mpan | |- ( B =/= 0 -> ( ( A / B ) = C <-> ( B x. C ) = A ) ) |