Theorem sn-msqgt0d

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

	Ref	Expression
Hypotheses	sn-msqgt0d.a	|- ( ph -> A e. RR )
	sn-msqgt0d.u	|- ( ph -> A =/= 0 )
Assertion	sn-msqgt0d	|- ( ph -> 0 < ( A x. A ) )

Proof

Step	Hyp	Ref	Expression
1		sn-msqgt0d.a	|- ( ph -> A e. RR )
2		sn-msqgt0d.u	|- ( ph -> A =/= 0 )
3	1	adantr	|- ( ( ph /\ A < 0 ) -> A e. RR )
4		simpr	|- ( ( ph /\ A < 0 ) -> A < 0 )
5	3 3 4 4	sn-mullt0d	|- ( ( ph /\ A < 0 ) -> 0 < ( A x. A ) )
6	1	adantr	|- ( ( ph /\ 0 < A ) -> A e. RR )
7		simpr	|- ( ( ph /\ 0 < A ) -> 0 < A )
8	6 6 7 7	mulgt0d	|- ( ( ph /\ 0 < A ) -> 0 < ( A x. A ) )
9		0red	|- ( ph -> 0 e. RR )
10	1 9	lttri2d	|- ( ph -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
11	2 10	mpbid	|- ( ph -> ( A < 0 \/ 0 < A ) )
12	5 8 11	mpjaodan	|- ( ph -> 0 < ( A x. A ) )