Theorem zgt0ge1

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 ≤ 𝑍 ) )

Proof

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 ≤ 𝑍 ) )