addinvcom

Description: A number commutes with its additive inverse. Compare remulinvcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Hypotheses	addinvcom.a	$⊢ φ \to A \in ℂ$
	addinvcom.b	$⊢ φ \to B \in ℂ$
	addinvcom.1	$⊢ φ \to A + B = 0$
Assertion	addinvcom	$⊢ φ \to B + A = 0$

Proof

Step	Hyp	Ref	Expression
1		addinvcom.a	$⊢ φ \to A \in ℂ$
2		addinvcom.b	$⊢ φ \to B \in ℂ$
3		addinvcom.1	$⊢ φ \to A + B = 0$
4		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
5		simpl	$⊢ (A + x = 0 \land x + A = 0) \to A + x = 0$
6	5	rgenw	$⊢ \forall x \in ℂ ((A + x = 0 \land x + A = 0) \to A + x = 0)$
7	6	a1i	$⊢ φ \to \forall x \in ℂ ((A + x = 0 \land x + A = 0) \to A + x = 0)$
8		sn-negex12	$⊢ A \in ℂ \to \exists x \in ℂ (A + x = 0 \land x + A = 0)$
9	1 8	syl	$⊢ φ \to \exists x \in ℂ (A + x = 0 \land x + A = 0)$
10		0cn	$⊢ 0 \in ℂ$
11		sn-subeu	$⊢ (A \in ℂ \land 0 \in ℂ) \to \exists! x \in ℂ A + x = 0$
12	1 10 11	sylancl	$⊢ φ \to \exists! x \in ℂ A + x = 0$
13		riotass2	$⊢ ((ℂ \subseteq ℂ \land \forall x \in ℂ ((A + x = 0 \land x + A = 0) \to A + x = 0)) \land (\exists x \in ℂ (A + x = 0 \land x + A = 0) \land \exists! x \in ℂ A + x = 0)) \to (ι x \in ℂ \| (A + x = 0 \land x + A = 0)) = (ι x \in ℂ \| A + x = 0)$
14	4 7 9 12 13	syl22anc	$⊢ φ \to (ι x \in ℂ \| (A + x = 0 \land x + A = 0)) = (ι x \in ℂ \| A + x = 0)$
15		oveq2	$⊢ x = B \to A + x = A + B$
16	15	eqeq1d	$⊢ x = B \to (A + x = 0 \leftrightarrow A + B = 0)$
17	16	riota2	$⊢ (B \in ℂ \land \exists! x \in ℂ A + x = 0) \to (A + B = 0 \leftrightarrow (ι x \in ℂ \| A + x = 0) = B)$
18	2 12 17	syl2anc	$⊢ φ \to (A + B = 0 \leftrightarrow (ι x \in ℂ \| A + x = 0) = B)$
19	3 18	mpbid	$⊢ φ \to (ι x \in ℂ \| A + x = 0) = B$
20	14 19	eqtrd	$⊢ φ \to (ι x \in ℂ \| (A + x = 0 \land x + A = 0)) = B$
21		reurmo	$⊢ \exists! x \in ℂ A + x = 0 \to \exists^{*} x \in ℂ A + x = 0$
22	5	rmoimi	$⊢ \exists^{} x \in ℂ A + x = 0 \to \exists^{} x \in ℂ (A + x = 0 \land x + A = 0)$
23	12 21 22	3syl	$⊢ φ \to \exists^{*} x \in ℂ (A + x = 0 \land x + A = 0)$
24		reu5	$⊢ \exists! x \in ℂ (A + x = 0 \land x + A = 0) \leftrightarrow (\exists x \in ℂ (A + x = 0 \land x + A = 0) \land \exists^{*} x \in ℂ (A + x = 0 \land x + A = 0))$
25	9 23 24	sylanbrc	$⊢ φ \to \exists! x \in ℂ (A + x = 0 \land x + A = 0)$
26		oveq1	$⊢ x = B \to x + A = B + A$
27	26	eqeq1d	$⊢ x = B \to (x + A = 0 \leftrightarrow B + A = 0)$
28	16 27	anbi12d	$⊢ x = B \to ((A + x = 0 \land x + A = 0) \leftrightarrow (A + B = 0 \land B + A = 0))$
29	28	riota2	$⊢ (B \in ℂ \land \exists! x \in ℂ (A + x = 0 \land x + A = 0)) \to ((A + B = 0 \land B + A = 0) \leftrightarrow (ι x \in ℂ \| (A + x = 0 \land x + A = 0)) = B)$
30	2 25 29	syl2anc	$⊢ φ \to ((A + B = 0 \land B + A = 0) \leftrightarrow (ι x \in ℂ \| (A + x = 0 \land x + A = 0)) = B)$
31	20 30	mpbird	$⊢ φ \to (A + B = 0 \land B + A = 0)$
32	31	simprd	$⊢ φ \to B + A = 0$

Metamath Proof Explorer

Theorem addinvcom

Proof