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	$⊢ (A \in ℝ \land A \neq 0) \to 0 < A A$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ A \in ℝ \to A \in ℝ$
2		0red	$⊢ A \in ℝ \to 0 \in ℝ$
3	1 2	lttri2d	$⊢ A \in ℝ \to (A \neq 0 \leftrightarrow (A < 0 \lor 0 < A))$
4	3	biimpa	$⊢ (A \in ℝ \land A \neq 0) \to (A < 0 \lor 0 < A)$
5		mullt0	$⊢ ((A \in ℝ \land A < 0) \land (A \in ℝ \land A < 0)) \to 0 < A A$
6	5	anidms	$⊢ (A \in ℝ \land A < 0) \to 0 < A A$
7		mulgt0	$⊢ ((A \in ℝ \land 0 < A) \land (A \in ℝ \land 0 < A)) \to 0 < A A$
8	7	anidms	$⊢ (A \in ℝ \land 0 < A) \to 0 < A A$
9	6 8	jaodan	$⊢ (A \in ℝ \land (A < 0 \lor 0 < A)) \to 0 < A A$
10	4 9	syldan	$⊢ (A \in ℝ \land A \neq 0) \to 0 < A A$