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	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ax-rnegex	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )
2		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 + 𝑥 ) ∈ ℝ )
3		eleq1	⊢ ( ( 𝐴 + 𝑥 ) = 0 → ( ( 𝐴 + 𝑥 ) ∈ ℝ ↔ 0 ∈ ℝ ) )
4	2 3	syl5ibcom	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 + 𝑥 ) = 0 → 0 ∈ ℝ ) )
5	4	rexlimdva	⊢ ( 𝐴 ∈ ℝ → ( ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 → 0 ∈ ℝ ) )
6	1 5	mpd	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )