Description: The square of a nonzero real is a positive real. (Contributed by AV, 5-Mar-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | sqn0rp | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ∈ ℝ+ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resqcl | ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ ) | |
2 | 1 | adantr | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ∈ ℝ ) |
3 | sqgt0 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 ↑ 2 ) ) | |
4 | 2 3 | elrpd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ∈ ℝ+ ) |