Metamath Proof Explorer

Theorem sgnpbi

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

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

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 → 0 < A ↔ 0 = 1 → 0 < A
4 eqeq1 ⊢ sgn ⁡ A = 1 → sgn ⁡ A = 1 ↔ 1 = 1
5 4 imbi1d ⊢ sgn ⁡ A = 1 → sgn ⁡ A = 1 → 0 < A ↔ 1 = 1 → 0 < A
6 eqeq1 ⊢ sgn ⁡ A = − 1 → sgn ⁡ A = 1 ↔ − 1 = 1
7 6 imbi1d ⊢ sgn ⁡ A = − 1 → sgn ⁡ A = 1 → 0 < A ↔ − 1 = 1 → 0 < A
8 0ne1 ⊢ 0 ≠ 1
9 8 neii ⊢ ¬ 0 = 1
10 9 pm2.21i ⊢ 0 = 1 → 0 < A
11 10 a1i ⊢ A ∈ ℝ * ∧ A = 0 → 0 = 1 → 0 < A
12 simp2 ⊢ A ∈ ℝ * ∧ 0 < A ∧ 1 = 1 → 0 < A
13 12 3expia ⊢ A ∈ ℝ * ∧ 0 < A → 1 = 1 → 0 < A
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 < A
24 23 a1i ⊢ A ∈ ℝ * ∧ A < 0 → − 1 = 1 → 0 < A
25 1 3 5 7 11 13 24 sgn3da ⊢ A ∈ ℝ * → sgn ⁡ A = 1 → 0 < A
26 25 imp ⊢ A ∈ ℝ * ∧ sgn ⁡ A = 1 → 0 < A
27 sgnp ⊢ A ∈ ℝ * ∧ 0 < A → sgn ⁡ A = 1
28 26 27 impbida ⊢ A ∈ ℝ * → sgn ⁡ A = 1 ↔ 0 < A