Description: A number is positive iff its half is positive. (Contributed by NM, 10-Apr-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | halfpos2 | ⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ 0 < ( 𝐴 / 2 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re | ⊢ 2 ∈ ℝ | |
2 | 2pos | ⊢ 0 < 2 | |
3 | gt0div | ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 ) → ( 0 < 𝐴 ↔ 0 < ( 𝐴 / 2 ) ) ) | |
4 | 1 2 3 | mp3an23 | ⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ 0 < ( 𝐴 / 2 ) ) ) |