Metamath Proof Explorer

Theorem dfrp2

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

Ref Expression
Assertion dfrp2 
|- RR+ = ( 0 (,) +oo )

Proof

Step Hyp Ref Expression
1 ltpnf 
 |-  ( x e. RR -> x < +oo )
2 1 adantr 
 |-  ( ( x e. RR /\ 0 < x ) -> x < +oo )
3 2 pm4.71i 
 |-  ( ( x e. RR /\ 0 < x ) <-> ( ( x e. RR /\ 0 < x ) /\ x < +oo ) )
4 df-3an 
 |-  ( ( x e. RR /\ 0 < x /\ x < +oo ) <-> ( ( x e. RR /\ 0 < x ) /\ x < +oo ) )
5 3 4 bitr4i 
 |-  ( ( x e. RR /\ 0 < x ) <-> ( x e. RR /\ 0 < x /\ x < +oo ) )
6 elrp 
 |-  ( x e. RR+ <-> ( x e. RR /\ 0 < x ) )
7 0xr 
 |-  0 e. RR*
8 pnfxr 
 |-  +oo e. RR*
9 elioo2 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( x e. ( 0 (,) +oo ) <-> ( x e. RR /\ 0 < x /\ x < +oo ) ) )
10 7 8 9 mp2an 
 |-  ( x e. ( 0 (,) +oo ) <-> ( x e. RR /\ 0 < x /\ x < +oo ) )
11 5 6 10 3bitr4i 
 |-  ( x e. RR+ <-> x e. ( 0 (,) +oo ) )
12 11 eqriv 
 |-  RR+ = ( 0 (,) +oo )