Theorem sgnnbi

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

	Ref	Expression
Assertion	sgnnbi	⊢ ( 𝐴 ∈ ℝ* → ( ( sgn ‘ 𝐴 ) = - 1 ↔ 𝐴 < 0 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ∈ ℝ* )
2		eqeq1	⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( ( sgn ‘ 𝐴 ) = - 1 ↔ 0 = - 1 ) )
3	2	imbi1d	⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( ( ( sgn ‘ 𝐴 ) = - 1 → 𝐴 < 0 ) ↔ ( 0 = - 1 → 𝐴 < 0 ) ) )
4		eqeq1	⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( ( sgn ‘ 𝐴 ) = - 1 ↔ 1 = - 1 ) )
5	4	imbi1d	⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( ( ( sgn ‘ 𝐴 ) = - 1 → 𝐴 < 0 ) ↔ ( 1 = - 1 → 𝐴 < 0 ) ) )
6		eqeq1	⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( ( sgn ‘ 𝐴 ) = - 1 ↔ - 1 = - 1 ) )
7	6	imbi1d	⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( ( ( sgn ‘ 𝐴 ) = - 1 → 𝐴 < 0 ) ↔ ( - 1 = - 1 → 𝐴 < 0 ) ) )
8		neg1ne0	⊢ - 1 ≠ 0
9	8	nesymi	⊢ ¬ 0 = - 1
10	9	pm2.21i	⊢ ( 0 = - 1 → 𝐴 < 0 )
11	10	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 = 0 ) → ( 0 = - 1 → 𝐴 < 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 → 𝐴 < 0 )
22	21	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 1 = - 1 → 𝐴 < 0 ) )
23		simp2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ∧ - 1 = - 1 ) → 𝐴 < 0 )
24	23	3expia	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( - 1 = - 1 → 𝐴 < 0 ) )
25	1 3 5 7 11 22 24	sgn3da	⊢ ( 𝐴 ∈ ℝ* → ( ( sgn ‘ 𝐴 ) = - 1 → 𝐴 < 0 ) )
26	25	imp	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( sgn ‘ 𝐴 ) = - 1 ) → 𝐴 < 0 )
27		sgnn	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( sgn ‘ 𝐴 ) = - 1 )
28	26 27	impbida	⊢ ( 𝐴 ∈ ℝ* → ( ( sgn ‘ 𝐴 ) = - 1 ↔ 𝐴 < 0 ) )