Metamath Proof Explorer


Theorem sn-negex2

Description: Proof of cnegex2 without ax-mulcom . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-negex2 ( 𝐴 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( 𝑏 + 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 sn-negex12 ( 𝐴 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) )
2 simpr ( ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) → ( 𝑏 + 𝐴 ) = 0 )
3 2 reximi ( ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) → ∃ 𝑏 ∈ ℂ ( 𝑏 + 𝐴 ) = 0 )
4 1 3 syl ( 𝐴 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( 𝑏 + 𝐴 ) = 0 )