sn-subeu

Description: negeu without ax-mulcom and complex number version of resubeu . (Contributed by SN, 5-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sn-negex	$⊢ 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		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \to y \in ℂ$
4		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \to B \in ℂ$
5	3 4	addcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \to y + B \in ℂ$
6		simplrr	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A + y = 0$
7	6	oveq1d	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A + y + B = 0 + B$
8		simplll	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A \in ℂ$
9		simplrl	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to y \in ℂ$
10		simpllr	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to B \in ℂ$
11	8 9 10	addassd	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to A + y + B = A + y + B$
12		sn-addlid	$⊢ B \in ℂ \to 0 + B = B$
13	10 12	syl	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to 0 + B = B$
14	7 11 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	9 10	addcld	$⊢ (((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land A + y = 0)) \land x \in ℂ) \to y + B \in ℂ$
18	8 16 17	sn-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	5 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 sn-subeu

Proof