Metamath Proof Explorer


Theorem addinvcom

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

Ref Expression
Hypotheses addinvcom.a φ A
addinvcom.b φ B
addinvcom.1 φ A + B = 0
Assertion addinvcom φ B + A = 0

Proof

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