Theorem elre0re 41175

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

Assertion

Ref	Expression
elre0re	⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)

Proof of Theorem elre0re

Dummy variable 𝑥 is distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  (class class class)co 7409  ℝcr 11109  0cc0 11110   + caddc 11113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-addrcl 11171  ax-rnegex 11181

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-rex 3072

This theorem is referenced by:  rernegcl  41244  renegadd  41245  reneg0addlid  41247  resubeulem1  41248  resubeulem2  41249  resubeu  41250  remul02  41278  remul01  41280  readdrid  41282  resubid1  41283  renegneg  41284  renegid2  41286  sn-it0e0  41288  relt0neg2  41318