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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
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 < ( 𝐴 · 𝐴 ) )