Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
sqgt0
Next ⟩
sqn0rp
Metamath Proof Explorer
Ascii
Unicode
Theorem
sqgt0
Description:
The square of a nonzero real is positive.
(Contributed by
NM
, 8-Sep-2007)
Ref
Expression
Assertion
sqgt0
⊢
A
∈
ℝ
∧
A
≠
0
→
0
<
A
2
Proof
Step
Hyp
Ref
Expression
1
msqgt0
⊢
A
∈
ℝ
∧
A
≠
0
→
0
<
A
⁢
A
2
recn
⊢
A
∈
ℝ
→
A
∈
ℂ
3
sqval
⊢
A
∈
ℂ
→
A
2
=
A
⁢
A
4
2
3
syl
⊢
A
∈
ℝ
→
A
2
=
A
⁢
A
5
4
adantr
⊢
A
∈
ℝ
∧
A
≠
0
→
A
2
=
A
⁢
A
6
1
5
breqtrrd
⊢
A
∈
ℝ
∧
A
≠
0
→
0
<
A
2