addcan

Description: Cancellation law for addition. Theorem I.1 of Apostol p. 18. (Contributed by NM, 22-Nov-1994) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	addcan	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to (A + B = A + C \leftrightarrow B = C)$

Proof

Step	Hyp	Ref	Expression
1		cnegex2	$⊢ A \in ℂ \to \exists x \in ℂ x + A = 0$
2	1	3ad2ant1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to \exists x \in ℂ x + A = 0$
3		oveq2	$⊢ A + B = A + C \to x + A + B = x + A + C$
4		simprr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x + A = 0$
5	4	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x + A + B = 0 + B$
6		simprl	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x \in ℂ$
7		simpl1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to A \in ℂ$
8		simpl2	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to B \in ℂ$
9	6 7 8	addassd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x + A + B = x + A + B$
10		addlid	$⊢ B \in ℂ \to 0 + B = B$
11	8 10	syl	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to 0 + B = B$
12	5 9 11	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x + A + B = B$
13	4	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x + A + C = 0 + C$
14		simpl3	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to C \in ℂ$
15	6 7 14	addassd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x + A + C = x + A + C$
16		addlid	$⊢ C \in ℂ \to 0 + C = C$
17	14 16	syl	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to 0 + C = C$
18	13 15 17	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to x + A + C = C$
19	12 18	eqeq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to (x + A + B = x + A + C \leftrightarrow B = C)$
20	3 19	imbitrid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to (A + B = A + C \to B = C)$
21		oveq2	$⊢ B = C \to A + B = A + C$
22	20 21	impbid1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (x \in ℂ \land x + A = 0)) \to (A + B = A + C \leftrightarrow B = C)$
23	2 22	rexlimddv	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to (A + B = A + C \leftrightarrow B = C)$

Metamath Proof Explorer

Theorem addcan

Proof