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

Metamath Proof Explorer

Theorem sn-negex2

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

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

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