# 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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \exists !{x}\in ℂ\phantom{\rule{.4em}{0ex}}{A}+{x}={B}$

### Proof

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