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

Metamath Proof Explorer

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 ) )