Database
REAL AND COMPLEX NUMBERS
Order sets
Positive reals (as a subset of complex numbers)
rprene0d
Next ⟩
rpcnne0d
Metamath Proof Explorer
Ascii
Unicode
Theorem
rprene0d
Description:
A positive real is a nonzero real number.
(Contributed by
Mario Carneiro
, 28-May-2016)
Ref
Expression
Hypothesis
rpred.1
⊢
φ
→
A
∈
ℝ
+
Assertion
rprene0d
⊢
φ
→
A
∈
ℝ
∧
A
≠
0
Proof
Step
Hyp
Ref
Expression
1
rpred.1
⊢
φ
→
A
∈
ℝ
+
2
1
rpred
⊢
φ
→
A
∈
ℝ
3
1
rpne0d
⊢
φ
→
A
≠
0
4
2
3
jca
⊢
φ
→
A
∈
ℝ
∧
A
≠
0