Metamath Proof Explorer


Theorem 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 B ∃! x A + x = B

Proof

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