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 \in [0, +∞] \land A \neq +∞) \to A \in ℝ$

Step	Hyp	Ref	Expression
1		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
2		0xr	$⊢ 0 \in ℝ^{*}$
3	2	a1i	$⊢ (A \in [0, +∞] \land A \neq +∞) \to 0 \in ℝ^{*}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5	4	a1i	$⊢ (A \in [0, +∞] \land A \neq +∞) \to +∞ \in ℝ^{*}$
6		eliccxr	$⊢ A \in [0, +∞] \to A \in ℝ^{*}$
7	6	adantr	$⊢ (A \in [0, +∞] \land A \neq +∞) \to A \in ℝ^{*}$
8	2	a1i	$⊢ A \in [0, +∞] \to 0 \in ℝ^{*}$
9	4	a1i	$⊢ A \in [0, +∞] \to +∞ \in ℝ^{*}$
10		id	$⊢ A \in [0, +∞] \to A \in [0, +∞]$
11		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land A \in [0, +∞]) \to 0 \leq A$
12	8 9 10 11	syl3anc	$⊢ A \in [0, +∞] \to 0 \leq A$
13	12	adantr	$⊢ (A \in [0, +∞] \land A \neq +∞) \to 0 \leq A$
14		pnfge	$⊢ A \in ℝ^{*} \to A \leq +∞$
15	6 14	syl	$⊢ A \in [0, +∞] \to A \leq +∞$
16	15	adantr	$⊢ (A \in [0, +∞] \land A \neq +∞) \to A \leq +∞$
17		simpr	$⊢ (A \in [0, +∞] \land A \neq +∞) \to A \neq +∞$
18	7 5 16 17	xrleneltd	$⊢ (A \in [0, +∞] \land A \neq +∞) \to A < +∞$
19	3 5 7 13 18	elicod	$⊢ (A \in [0, +∞] \land A \neq +∞) \to A \in [0, +∞)$
20	1 19	sselid	$⊢ (A \in [0, +∞] \land A \neq +∞) \to A \in ℝ$

Metamath Proof Explorer