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 ⊢ φ → A ∈ ℝ
sn-msqgt0d.u ⊢ φ → A ≠ 0
Assertion sn-msqgt0d ⊢ φ → 0 < A ⁢ A

Proof

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