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

Metamath Proof Explorer

Theorem ge0xrre

Description: A nonnegative extended real that is not +oo is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion ge0xrre ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → A ∈ ℝ

Proof

Step Hyp Ref Expression
1 rge0ssre ⊢ 0 +∞ ⊆ ℝ
2 0xr ⊢ 0 ∈ ℝ *
3 2 a1i ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → 0 ∈ ℝ *
4 pnfxr ⊢ +∞ ∈ ℝ *
5 4 a1i ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → +∞ ∈ ℝ *
6 eliccxr ⊢ A ∈ 0 +∞ → A ∈ ℝ *
7 6 adantr ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → A ∈ ℝ *
8 2 a1i ⊢ A ∈ 0 +∞ → 0 ∈ ℝ *
9 4 a1i ⊢ A ∈ 0 +∞ → +∞ ∈ ℝ *
10 id ⊢ A ∈ 0 +∞ → A ∈ 0 +∞
11 iccgelb ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ A ∈ 0 +∞ → 0 ≤ A
12 8 9 10 11 syl3anc ⊢ A ∈ 0 +∞ → 0 ≤ A
13 12 adantr ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → 0 ≤ A
14 pnfge ⊢ A ∈ ℝ * → A ≤ +∞
15 6 14 syl ⊢ A ∈ 0 +∞ → A ≤ +∞
16 15 adantr ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → A ≤ +∞
17 simpr ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → A ≠ +∞
18 7 5 16 17 xrleneltd ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → A < +∞
19 3 5 7 13 18 elicod ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → A ∈ 0 +∞
20 1 19 sselid ⊢ A ∈ 0 +∞ ∧ A ≠ +∞ → A ∈ ℝ