Theorem sn-msqgt0d

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

	Ref	Expression
Hypotheses	sn-msqgt0d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	sn-msqgt0d.u	⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion	sn-msqgt0d	⊢ ( 𝜑 → 0 < ( 𝐴 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sn-msqgt0d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		sn-msqgt0d.u	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 < 0 )
5	3 3 4 4	sn-mullt0d	⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 0 < ( 𝐴 · 𝐴 ) )
6	1	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
7		simpr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < 𝐴 )
8	6 6 7 7	mulgt0d	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < ( 𝐴 · 𝐴 ) )
9		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
10	1 9	lttri2d	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ↔ ( 𝐴 < 0 ∨ 0 < 𝐴 ) ) )
11	2 10	mpbid	⊢ ( 𝜑 → ( 𝐴 < 0 ∨ 0 < 𝐴 ) )
12	5 8 11	mpjaodan	⊢ ( 𝜑 → 0 < ( 𝐴 · 𝐴 ) )