Metamath Proof Explorer

Theorem sn-subeu

Description: negeu without ax-mulcom and complex number version of resubeu . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-subeu ⊢ A ∈ ℂ ∧ B ∈ ℂ → ∃! x ∈ ℂ A + x = B

Proof

Step Hyp Ref Expression
1 sn-negex ⊢ A ∈ ℂ → ∃ y ∈ ℂ A + y = 0
2 1 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → ∃ y ∈ ℂ A + y = 0
3 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 → y ∈ ℂ
4 simplr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 → B ∈ ℂ
5 3 4 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 → y + B ∈ ℂ
6 simplrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → A + y = 0
7 6 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → A + y + B = 0 + B
8 simplll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → A ∈ ℂ
9 simplrl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → y ∈ ℂ
10 simpllr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → B ∈ ℂ
11 8 9 10 addassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → A + y + B = A + y + B
12 sn-addlid ⊢ B ∈ ℂ → 0 + B = B
13 10 12 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → 0 + B = B
14 7 11 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 9 10 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 ∧ x ∈ ℂ → y + B ∈ ℂ
18 8 16 17 sn-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 5 20 21 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ y ∈ ℂ ∧ A + y = 0 → ∃! x ∈ ℂ A + x = B
23 2 22 rexlimddv ⊢ A ∈ ℂ ∧ B ∈ ℂ → ∃! x ∈ ℂ A + x = B