Metamath Proof Explorer


Theorem sqgt0d

Description: The square of a nonzero real is positive. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses resqcld.1 ( 𝜑𝐴 ∈ ℝ )
sqgt0d.2 ( 𝜑𝐴 ≠ 0 )
Assertion sqgt0d ( 𝜑 → 0 < ( 𝐴 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 resqcld.1 ( 𝜑𝐴 ∈ ℝ )
2 sqgt0d.2 ( 𝜑𝐴 ≠ 0 )
3 sqgt0 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 ↑ 2 ) )
4 1 2 3 syl2anc ( 𝜑 → 0 < ( 𝐴 ↑ 2 ) )