mulcand

Description: Cancellation law for multiplication. Theorem I.7 of Apostol p. 18. (Contributed by NM, 26-Jan-1995) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	mulcand.1	$⊢ φ \to A \in ℂ$
	mulcand.2	$⊢ φ \to B \in ℂ$
	mulcand.3	$⊢ φ \to C \in ℂ$
	mulcand.4	$⊢ φ \to C \neq 0$
Assertion	mulcand	$⊢ φ \to (C A = C B \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		mulcand.1	$⊢ φ \to A \in ℂ$
2		mulcand.2	$⊢ φ \to B \in ℂ$
3		mulcand.3	$⊢ φ \to C \in ℂ$
4		mulcand.4	$⊢ φ \to C \neq 0$
5		recex	$⊢ (C \in ℂ \land C \neq 0) \to \exists x \in ℂ C x = 1$
6	3 4 5	syl2anc	$⊢ φ \to \exists x \in ℂ C x = 1$
7		oveq2	$⊢ C A = C B \to x C A = x C B$
8		simprl	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x \in ℂ$
9	3	adantr	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to C \in ℂ$
10	8 9	mulcomd	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C = C x$
11		simprr	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to C x = 1$
12	10 11	eqtrd	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C = 1$
13	12	oveq1d	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C A = 1 A$
14	1	adantr	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to A \in ℂ$
15	8 9 14	mulassd	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C A = x C A$
16	14	mullidd	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to 1 A = A$
17	13 15 16	3eqtr3d	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C A = A$
18	12	oveq1d	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C B = 1 B$
19	2	adantr	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to B \in ℂ$
20	8 9 19	mulassd	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C B = x C B$
21	19	mullidd	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to 1 B = B$
22	18 20 21	3eqtr3d	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to x C B = B$
23	17 22	eqeq12d	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to (x C A = x C B \leftrightarrow A = B)$
24	7 23	imbitrid	$⊢ (φ \land (x \in ℂ \land C x = 1)) \to (C A = C B \to A = B)$
25	6 24	rexlimddv	$⊢ φ \to (C A = C B \to A = B)$
26		oveq2	$⊢ A = B \to C A = C B$
27	25 26	impbid1	$⊢ φ \to (C A = C B \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem mulcand

Proof