Metamath Proof Explorer


Theorem sn-negex

Description: Proof of cnegex without ax-mulcom . (Contributed by SN, 30-Apr-2024)

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

Proof

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