Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0re | Structured version Visualization version GIF version |
Description: 0 is a real number. See also 0reALT 10378. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
0re | ⊢ 0 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 10039 | . 2 ⊢ 1 ∈ ℝ | |
2 | ax-rnegex 10007 | . 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0) | |
3 | readdcl 10019 | . . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ) | |
4 | 1, 3 | mpan 706 | . . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ) |
5 | eleq1 2689 | . . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ)) | |
6 | 4, 5 | syl5ibcom 235 | . . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ)) |
7 | 6 | rexlimiv 3027 | . 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ) |
8 | 1, 2, 7 | mp2b 10 | 1 ⊢ 0 ∈ ℝ |
Copyright terms: Public domain | W3C validator |