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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 cnegex ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑦 ∈ ℂ ( 𝐴 + 𝑦 ) = 0 )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ∃ 𝑦 ∈ ℂ ( 𝐴 + 𝑦 ) = 0 )
3 simpl ⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) → 𝑦 ∈ ℂ )
4 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
5 addcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑦 + 𝐵 ) ∈ ℂ )
6 3 4 5 syl2anr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) → ( 𝑦 + 𝐵 ) ∈ ℂ )
7 simplrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( 𝐴 + 𝑦 ) = 0 )
8 7 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 + 𝑦 ) + 𝐵 ) = ( 0 + 𝐵 ) )
9 simplll ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
10 simplrl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → 𝑦 ∈ ℂ )
11 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
12 9 10 11 addassd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 + 𝑦 ) + 𝐵 ) = ( 𝐴 + ( 𝑦 + 𝐵 ) ) )
13 11 addid2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( 0 + 𝐵 ) = 𝐵 )
14 8 12 13 3eqtr3rd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → 𝐵 = ( 𝐴 + ( 𝑦 + 𝐵 ) ) )
15 14 eqeq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 + 𝑥 ) = 𝐵 ↔ ( 𝐴 + 𝑥 ) = ( 𝐴 + ( 𝑦 + 𝐵 ) ) ) )
16 simpr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
17 10 11 addcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( 𝑦 + 𝐵 ) ∈ ℂ )
18 9 16 17 addcand ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 + 𝑥 ) = ( 𝐴 + ( 𝑦 + 𝐵 ) ) ↔ 𝑥 = ( 𝑦 + 𝐵 ) ) )
19 15 18 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 + 𝑥 ) = 𝐵 ↔ 𝑥 = ( 𝑦 + 𝐵 ) ) )
20 19 ralrimiva ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) → ∀ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 𝐵 ↔ 𝑥 = ( 𝑦 + 𝐵 ) ) )
21 reu6i ⊢ ( ( ( 𝑦 + 𝐵 ) ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) = 𝐵 ↔ 𝑥 = ( 𝑦 + 𝐵 ) ) ) → ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 𝐵 )
22 6 20 21 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐴 + 𝑦 ) = 0 ) ) → ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 𝐵 )
23 2 22 rexlimddv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ∃! 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 𝐵 )