This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-negex

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

		Ref	Expression
	Assertion	sn-negex	$⊢ A \in ℂ \to \exists b \in ℂ A + b = 0$

Step	Hyp	Ref	Expression
1		sn-negex12	$⊢ A \in ℂ \to \exists b \in ℂ (A + b = 0 \land b + A = 0)$
2		simpl	$⊢ (A + b = 0 \land b + A = 0) \to A + b = 0$
3	2	reximi	$⊢ \exists b \in ℂ (A + b = 0 \land b + A = 0) \to \exists b \in ℂ A + b = 0$
4	1 3	syl	$⊢ A \in ℂ \to \exists b \in ℂ A + b = 0$