Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
sqgt0i
Next ⟩
sqge0i
Metamath Proof Explorer
Ascii
Unicode
Theorem
sqgt0i
Description:
The square of a nonzero real is positive.
(Contributed by
NM
, 17-Sep-1999)
Ref
Expression
Hypothesis
resqcl.1
⊢
A
∈
ℝ
Assertion
sqgt0i
⊢
A
≠
0
→
0
<
A
2
Proof
Step
Hyp
Ref
Expression
1
resqcl.1
⊢
A
∈
ℝ
2
sqgt0
⊢
A
∈
ℝ
∧
A
≠
0
→
0
<
A
2
3
1
2
mpan
⊢
A
≠
0
→
0
<
A
2