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 ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐴 ≠ +∞ ) → 𝐴 ∈ ℝ )

Proof

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