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

Metamath Proof Explorer

Theorem sqgt0

Description: The square of a nonzero real is positive. (Contributed by NM, 8-Sep-2007)

		Ref	Expression
	Assertion	sqgt0	$⊢ (A \in ℝ \land A \neq 0) \to 0 < A^{2}$

Step	Hyp	Ref	Expression
1		msqgt0	$⊢ (A \in ℝ \land A \neq 0) \to 0 < A A$
2		recn	$⊢ A \in ℝ \to A \in ℂ$
3		sqval	$⊢ A \in ℂ \to A^{2} = A A$
4	2 3	syl	$⊢ A \in ℝ \to A^{2} = A A$
5	4	adantr	$⊢ (A \in ℝ \land A \neq 0) \to A^{2} = A A$
6	1 5	breqtrrd	$⊢ (A \in ℝ \land A \neq 0) \to 0 < A^{2}$