Description: An integer greater than 0 is greater than or equal to 1 . (Contributed by AV, 14-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | zgt0ge1 | ⊢ ( 𝑍 ∈ ℤ → ( 0 < 𝑍 ↔ 1 ≤ 𝑍 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0z | ⊢ 0 ∈ ℤ | |
2 | zltp1le | ⊢ ( ( 0 ∈ ℤ ∧ 𝑍 ∈ ℤ ) → ( 0 < 𝑍 ↔ ( 0 + 1 ) ≤ 𝑍 ) ) | |
3 | 1 2 | mpan | ⊢ ( 𝑍 ∈ ℤ → ( 0 < 𝑍 ↔ ( 0 + 1 ) ≤ 𝑍 ) ) |
4 | 0p1e1 | ⊢ ( 0 + 1 ) = 1 | |
5 | 4 | a1i | ⊢ ( 𝑍 ∈ ℤ → ( 0 + 1 ) = 1 ) |
6 | 5 | breq1d | ⊢ ( 𝑍 ∈ ℤ → ( ( 0 + 1 ) ≤ 𝑍 ↔ 1 ≤ 𝑍 ) ) |
7 | 3 6 | bitrd | ⊢ ( 𝑍 ∈ ℤ → ( 0 < 𝑍 ↔ 1 ≤ 𝑍 ) ) |