This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem msqgt0

Description: A nonzero square is positive. Theorem I.20 of Apostol p. 20. (Contributed by NM, 6-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion msqgt0 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
2 0red ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
3 1 2 lttri2d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≠ 0 ↔ ( 𝐴 < 0 ∨ 0 < 𝐴 ) ) )
4 3 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 < 0 ∨ 0 < 𝐴 ) )
5 mullt0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) ) → 0 < ( 𝐴 · 𝐴 ) )
6 5 anidms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → 0 < ( 𝐴 · 𝐴 ) )
7 mulgt0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → 0 < ( 𝐴 · 𝐴 ) )
8 7 anidms ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 · 𝐴 ) )
9 6 8 jaodan ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 < 0 ∨ 0 < 𝐴 ) ) → 0 < ( 𝐴 · 𝐴 ) )
10 4 9 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 · 𝐴 ) )