Theorem elre0re

Description: Specialized version of 0red without using ax-1cn and ax-cnre . (Contributed by Steven Nguyen, 28-Jan-2023)

	Ref	Expression
Assertion	elre0re	$$⊢A\in ℝ\to 0\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ax-rnegex	$$⊢A\in ℝ\to \exists x\in ℝA+x=0$$
2		readdcl	$$⊢\left(A\in ℝ\wedge x\in ℝ\right)\to A+x\in ℝ$$
3		eleq1	$$⊢A+x=0\to \left(A+x\in ℝ\leftrightarrow 0\in ℝ\right)$$
4	2 3	syl5ibcom	$$⊢\left(A\in ℝ\wedge x\in ℝ\right)\to \left(A+x=0\to 0\in ℝ\right)$$
5	4	rexlimdva	$$⊢A\in ℝ\to \left(\exists x\in ℝA+x=0\to 0\in ℝ\right)$$
6	1 5	mpd	$$⊢A\in ℝ\to 0\in ℝ$$