Theorem sn-msqgt0d

Description: A nonzero square is positive. (Contributed by SN, 1-Dec-2025)

	Ref	Expression
Hypotheses	sn-msqgt0d.a	$$⊢\phi \to A\in ℝ$$
	sn-msqgt0d.u	$$⊢\phi \to A\ne 0$$
Assertion	sn-msqgt0d	$$⊢\phi \to 0<AA$$

Proof

Step	Hyp	Ref	Expression
1		sn-msqgt0d.a	$$⊢\phi \to A\in ℝ$$
2		sn-msqgt0d.u	$$⊢\phi \to A\ne 0$$
3	1	adantr	$$⊢\left(\phi \wedge A<0\right)\to A\in ℝ$$
4		simpr	$$⊢\left(\phi \wedge A<0\right)\to A<0$$
5	3 3 4 4	sn-mullt0d	$$⊢\left(\phi \wedge A<0\right)\to 0<AA$$
6	1	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A\in ℝ$$
7		simpr	$$⊢\left(\phi \wedge 0<A\right)\to 0<A$$
8	6 6 7 7	mulgt0d	$$⊢\left(\phi \wedge 0<A\right)\to 0<AA$$
9		0red	$$⊢\phi \to 0\in ℝ$$
10	1 9	lttri2d	$$⊢\phi \to \left(A\ne 0\leftrightarrow \left(A<0\vee 0<A\right)\right)$$
11	2 10	mpbid	$$⊢\phi \to \left(A<0\vee 0<A\right)$$
12	5 8 11	mpjaodan	$$⊢\phi \to 0<AA$$