Theorem sgnpbi

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

	Ref	Expression
Assertion	sgnpbi	⊢ ( 𝐴 ∈ ℝ* → ( ( 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		0ne1	⊢ 0 ≠ 1
9	8	neii	⊢ ¬ 0 = 1
10	9	pm2.21i	⊢ ( 0 = 1 → 0 < 𝐴 )
11	10	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 = 0 ) → ( 0 = 1 → 0 < 𝐴 ) )
12		simp2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ∧ 1 = 1 ) → 0 < 𝐴 )
13	12	3expia	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 1 = 1 → 0 < 𝐴 ) )
14		neg1rr	⊢ - 1 ∈ ℝ
15		neg1lt0	⊢ - 1 < 0
16		0lt1	⊢ 0 < 1
17		0re	⊢ 0 ∈ ℝ
18		1re	⊢ 1 ∈ ℝ
19	14 17 18	lttri	⊢ ( ( - 1 < 0 ∧ 0 < 1 ) → - 1 < 1 )
20	15 16 19	mp2an	⊢ - 1 < 1
21	14 20	gtneii	⊢ 1 ≠ - 1
22	21	nesymi	⊢ ¬ - 1 = 1
23	22	pm2.21i	⊢ ( - 1 = 1 → 0 < 𝐴 )
24	23	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( - 1 = 1 → 0 < 𝐴 ) )
25	1 3 5 7 11 13 24	sgn3da	⊢ ( 𝐴 ∈ ℝ* → ( ( sgn ‘ 𝐴 ) = 1 → 0 < 𝐴 ) )
26	25	imp	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( sgn ‘ 𝐴 ) = 1 ) → 0 < 𝐴 )
27		sgnp	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( sgn ‘ 𝐴 ) = 1 )
28	26 27	impbida	⊢ ( 𝐴 ∈ ℝ* → ( ( sgn ‘ 𝐴 ) = 1 ↔ 0 < 𝐴 ) )