dfrp2

Description: Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020)

		Ref	Expression
	Assertion	dfrp2	$⊢ ℝ^{+} = (0, +∞)$

Step	Hyp	Ref	Expression
1		ltpnf	$⊢ x \in ℝ \to x < +∞$
2	1	adantr	$⊢ (x \in ℝ \land 0 < x) \to x < +∞$
3	2	pm4.71i	$⊢ (x \in ℝ \land 0 < x) \leftrightarrow ((x \in ℝ \land 0 < x) \land x < +∞)$
4		df-3an	$⊢ (x \in ℝ \land 0 < x \land x < +∞) \leftrightarrow ((x \in ℝ \land 0 < x) \land x < +∞)$
5	3 4	bitr4i	$⊢ (x \in ℝ \land 0 < x) \leftrightarrow (x \in ℝ \land 0 < x \land x < +∞)$
6		elrp	$⊢ x \in ℝ^{+} \leftrightarrow (x \in ℝ \land 0 < x)$
7		0xr	$⊢ 0 \in ℝ^{*}$
8		pnfxr	$⊢ +∞ \in ℝ^{*}$
9		elioo2	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (x \in (0, +∞) \leftrightarrow (x \in ℝ \land 0 < x \land x < +∞))$
10	7 8 9	mp2an	$⊢ x \in (0, +∞) \leftrightarrow (x \in ℝ \land 0 < x \land x < +∞)$
11	5 6 10	3bitr4i	$⊢ x \in ℝ^{+} \leftrightarrow x \in (0, +∞)$
12	11	eqriv	$⊢ ℝ^{+} = (0, +∞)$

Metamath Proof Explorer