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

Proof

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