Metamath Proof Explorer

Theorem sgnnbi

Description: Negative signum. (Contributed by Thierry Arnoux, 2-Oct-2018)

Ref Expression
Assertion sgnnbi ⊢ A ∈ ℝ * → sgn ⁡ A = − 1 ↔ A < 0

Proof

Step Hyp Ref Expression
1 id ⊢ A ∈ ℝ * → A ∈ ℝ *
2 eqeq1 ⊢ sgn ⁡ A = 0 → sgn ⁡ A = − 1 ↔ 0 = − 1
3 2 imbi1d ⊢ sgn ⁡ A = 0 → sgn ⁡ A = − 1 → A < 0 ↔ 0 = − 1 → A < 0
4 eqeq1 ⊢ sgn ⁡ A = 1 → sgn ⁡ A = − 1 ↔ 1 = − 1
5 4 imbi1d ⊢ sgn ⁡ A = 1 → sgn ⁡ A = − 1 → A < 0 ↔ 1 = − 1 → A < 0
6 eqeq1 ⊢ sgn ⁡ A = − 1 → sgn ⁡ A = − 1 ↔ − 1 = − 1
7 6 imbi1d ⊢ sgn ⁡ A = − 1 → sgn ⁡ A = − 1 → A < 0 ↔ − 1 = − 1 → A < 0
8 neg1ne0 ⊢ − 1 ≠ 0
9 8 nesymi ⊢ ¬ 0 = − 1
10 9 pm2.21i ⊢ 0 = − 1 → A < 0
11 10 a1i ⊢ A ∈ ℝ * ∧ A = 0 → 0 = − 1 → A < 0
12 neg1rr ⊢ − 1 ∈ ℝ
13 neg1lt0 ⊢ − 1 < 0
14 0lt1 ⊢ 0 < 1
15 0re ⊢ 0 ∈ ℝ
16 1re ⊢ 1 ∈ ℝ
17 12 15 16 lttri ⊢ − 1 < 0 ∧ 0 < 1 → − 1 < 1
18 13 14 17 mp2an ⊢ − 1 < 1
19 12 18 gtneii ⊢ 1 ≠ − 1
20 19 neii ⊢ ¬ 1 = − 1
21 20 pm2.21i ⊢ 1 = − 1 → A < 0
22 21 a1i ⊢ A ∈ ℝ * ∧ 0 < A → 1 = − 1 → A < 0
23 simp2 ⊢ A ∈ ℝ * ∧ A < 0 ∧ − 1 = − 1 → A < 0
24 23 3expia ⊢ A ∈ ℝ * ∧ A < 0 → − 1 = − 1 → A < 0
25 1 3 5 7 11 22 24 sgn3da ⊢ A ∈ ℝ * → sgn ⁡ A = − 1 → A < 0
26 25 imp ⊢ A ∈ ℝ * ∧ sgn ⁡ A = − 1 → A < 0
27 sgnn ⊢ A ∈ ℝ * ∧ A < 0 → sgn ⁡ A = − 1
28 26 27 impbida ⊢ A ∈ ℝ * → sgn ⁡ A = − 1 ↔ A < 0