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

Metamath Proof Explorer

Theorem 0re

Description: The number 0 is real. Remark: the first step could also be ax-icn . See also 0reALT . (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)

Ref Expression
Assertion 0re 0 ∈ ℝ

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 cnre ⊢ ( 1 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 1 = ( 𝑥 + ( i · 𝑦 ) ) )
3 ax-rnegex ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑧 ∈ ℝ ( 𝑥 + 𝑧 ) = 0 )
4 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑥 + 𝑧 ) ∈ ℝ )
5 eleq1 ⊢ ( ( 𝑥 + 𝑧 ) = 0 → ( ( 𝑥 + 𝑧 ) ∈ ℝ ↔ 0 ∈ ℝ ) )
6 4 5 syl5ibcom ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑥 + 𝑧 ) = 0 → 0 ∈ ℝ ) )
7 6 rexlimdva ⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ ( 𝑥 + 𝑧 ) = 0 → 0 ∈ ℝ ) )
8 3 7 mpd ⊢ ( 𝑥 ∈ ℝ → 0 ∈ ℝ )
9 8 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ ∃ 𝑦 ∈ ℝ 1 = ( 𝑥 + ( i · 𝑦 ) ) ) → 0 ∈ ℝ )
10 9 rexlimiva ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 1 = ( 𝑥 + ( i · 𝑦 ) ) → 0 ∈ ℝ )
11 1 2 10 mp2b ⊢ 0 ∈ ℝ