Theorem dfrp2

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

	Ref	Expression
Assertion	dfrp2	⊢ ℝ+ = ( 0 (,) +∞ )

Proof

Step	Hyp	Ref	Expression
1		ltpnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
2	1	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) → 𝑥 < +∞ )
3	2	pm4.71i	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ 𝑥 < +∞ ) )
4		df-3an	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ∧ 𝑥 < +∞ ) ↔ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ 𝑥 < +∞ ) )
5	3 4	bitr4i	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ∧ 𝑥 < +∞ ) )
6		elrp	⊢ ( 𝑥 ∈ ℝ+ ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
7		0xr	⊢ 0 ∈ ℝ*
8		pnfxr	⊢ +∞ ∈ ℝ*
9		elioo2	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 0 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ∧ 𝑥 < +∞ ) ) )
10	7 8 9	mp2an	⊢ ( 𝑥 ∈ ( 0 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ∧ 𝑥 < +∞ ) )
11	5 6 10	3bitr4i	⊢ ( 𝑥 ∈ ℝ+ ↔ 𝑥 ∈ ( 0 (,) +∞ ) )
12	11	eqriv	⊢ ℝ+ = ( 0 (,) +∞ )