Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
sqn0rp
Next ⟩
nnsqcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
sqn0rp
Description:
The square of a nonzero real is a positive real.
(Contributed by
AV
, 5-Mar-2023)
Ref
Expression
Assertion
sqn0rp
⊢
A
∈
ℝ
∧
A
≠
0
→
A
2
∈
ℝ
+
Proof
Step
Hyp
Ref
Expression
1
resqcl
⊢
A
∈
ℝ
→
A
2
∈
ℝ
2
1
adantr
⊢
A
∈
ℝ
∧
A
≠
0
→
A
2
∈
ℝ
3
sqgt0
⊢
A
∈
ℝ
∧
A
≠
0
→
0
<
A
2
4
2
3
elrpd
⊢
A
∈
ℝ
∧
A
≠
0
→
A
2
∈
ℝ
+