Theorem sgn0bi

Description: Zero signum. (Contributed by Thierry Arnoux, 10-Oct-2018)

	Ref	Expression
Assertion	sgn0bi	⊢ ( 𝐴 ∈ ℝ* → ( ( sgn ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ∈ ℝ* )
2		eqeq1	⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( ( sgn ‘ 𝐴 ) = 0 ↔ 0 = 0 ) )
3	2	bibi1d	⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( ( ( sgn ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) ↔ ( 0 = 0 ↔ 𝐴 = 0 ) ) )
4		eqeq1	⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( ( sgn ‘ 𝐴 ) = 0 ↔ 1 = 0 ) )
5	4	bibi1d	⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( ( ( sgn ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) ↔ ( 1 = 0 ↔ 𝐴 = 0 ) ) )
6		eqeq1	⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( ( sgn ‘ 𝐴 ) = 0 ↔ - 1 = 0 ) )
7	6	bibi1d	⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( ( ( sgn ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) ↔ ( - 1 = 0 ↔ 𝐴 = 0 ) ) )
8		simpr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 = 0 ) → 𝐴 = 0 )
9	8	eqcomd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 = 0 ) → 0 = 𝐴 )
10	9	eqeq1d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 = 0 ) → ( 0 = 0 ↔ 𝐴 = 0 ) )
11		ax-1ne0	⊢ 1 ≠ 0
12	11	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 1 ≠ 0 )
13	12	neneqd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ¬ 1 = 0 )
14		simpr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 0 < 𝐴 )
15	14	gt0ne0d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
16	15	neneqd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ¬ 𝐴 = 0 )
17	13 16	2falsed	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 1 = 0 ↔ 𝐴 = 0 ) )
18		1cnd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → 1 ∈ ℂ )
19	11	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → 1 ≠ 0 )
20	18 19	negne0d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → - 1 ≠ 0 )
21	20	neneqd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ¬ - 1 = 0 )
22		simpr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → 𝐴 < 0 )
23	22	lt0ne0d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → 𝐴 ≠ 0 )
24	23	neneqd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ¬ 𝐴 = 0 )
25	21 24	2falsed	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( - 1 = 0 ↔ 𝐴 = 0 ) )
26	1 3 5 7 10 17 25	sgn3da	⊢ ( 𝐴 ∈ ℝ* → ( ( sgn ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )