Database
REAL AND COMPLEX NUMBERS
Order sets
Positive reals (as a subset of complex numbers)
ralrp
Next ⟩
rexrp
Metamath Proof Explorer
Ascii
Unicode
Theorem
ralrp
Description:
Quantification over positive reals.
(Contributed by
NM
, 12-Feb-2008)
Ref
Expression
Assertion
ralrp
⊢
∀
x
∈
ℝ
+
φ
↔
∀
x
∈
ℝ
0
<
x
→
φ
Proof
Step
Hyp
Ref
Expression
1
elrp
⊢
x
∈
ℝ
+
↔
x
∈
ℝ
∧
0
<
x
2
1
imbi1i
⊢
x
∈
ℝ
+
→
φ
↔
x
∈
ℝ
∧
0
<
x
→
φ
3
impexp
⊢
x
∈
ℝ
∧
0
<
x
→
φ
↔
x
∈
ℝ
→
0
<
x
→
φ
4
2
3
bitri
⊢
x
∈
ℝ
+
→
φ
↔
x
∈
ℝ
→
0
<
x
→
φ
5
4
ralbii2
⊢
∀
x
∈
ℝ
+
φ
↔
∀
x
∈
ℝ
0
<
x
→
φ