Description: Cancellation law for multiplication (full theorem form). Theorem I.7 of Apostol p. 18. (Contributed by NM, 29-Jan-1995) (Revised by Mario Carneiro, 27-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mulcan | |- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) = ( C x. B ) <-> A = B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1 | |- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC ) |
|
| 2 | simp2 | |- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC ) |
|
| 3 | simp3l | |- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC ) |
|
| 4 | simp3r | |- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C =/= 0 ) |
|
| 5 | 1 2 3 4 | mulcand | |- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) = ( C x. B ) <-> A = B ) ) |