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

Metamath Proof Explorer

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 (,) +∞ )