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 < ( 𝐴 · 𝐴 ) )