negeu

Description: Existential uniqueness of negatives. Theorem I.2 of Apostol p. 18. (Contributed by NM, 22-Nov-1994) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	negeu	$⊢ (A \in ℂ \land B \in ℂ) \to \exists! x \in ℂ A + x = B$

Proof

Step	Hyp	Ref	Expression
1		cnegex	$⊢ A \in ℂ \to \exists y \in ℂ A + y = 0$
2	1	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to \exists y \in ℂ A + y = 0$
3		simpl	$⊢ (y \in ℂ \land A + y = 0) \to y \in ℂ$
4		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
5		addcl	$⊢ (y \in ℂ \land B \in ℂ) \to y + B \in ℂ$
6	3 4 5	syl2anr	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \to y + B \in ℂ$
7		simplrr	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A + y = 0$
8	7	oveq1d	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A + y + B = 0 + B$
9		simplll	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A \in ℂ$
10		simplrl	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to y \in ℂ$
11		simpllr	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to B \in ℂ$
12	9 10 11	addassd	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A + y + B = A + y + B$
13	11	addid2d	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to 0 + B = B$
14	8 12 13	3eqtr3rd	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to B = A + y + B$
15	14	eqeq2d	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to (A + x = B \leftrightarrow A + x = A + y + B)$
16		simpr	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to x \in ℂ$
17	10 11	addcld	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to y + B \in ℂ$
18	9 16 17	addcand	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to (A + x = A + y + B \leftrightarrow x = y + B)$
19	15 18	bitrd	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to (A + x = B \leftrightarrow x = y + B)$
20	19	ralrimiva	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \to \forall x \in ℂ (A + x = B \leftrightarrow x = y + B)$
21		reu6i	$⊢ (y + B \in ℂ \land \forall x \in ℂ (A + x = B \leftrightarrow x = y + B)) \to \exists! x \in ℂ A + x = B$
22	6 20 21	syl2anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \to \exists! x \in ℂ A + x = B$
23	2 22	rexlimddv	$⊢ (A \in ℂ \land B \in ℂ) \to \exists! x \in ℂ A + x = B$

Metamath Proof Explorer

Theorem negeu

Proof