Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  0re Structured version   Visualization version   GIF version

Theorem 0re 10681
 Description: The number 0 is real. Remark: the first step could also be ax-icn 10634. See also 0reALT 11021. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022.)
Assertion
Ref Expression
0re 0 ∈ ℝ

Proof of Theorem 0re
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-1cn 10633 . 2 1 ∈ ℂ
2 cnre 10676 . 2 (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3 ax-rnegex 10646 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4 readdcl 10658 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5 eleq1 2839 . . . . . . 7 ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 248 . . . . . 6 ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
76rexlimdva 3208 . . . . 5 (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
83, 7mpd 15 . . . 4 (𝑥 ∈ ℝ → 0 ∈ ℝ)
98adantr 484 . . 3 ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
109rexlimiva 3205 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
111, 2, 10mp2b 10 1 0 ∈ ℝ