Theorem eluz2b1

Description: Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012)

	Ref	Expression
Assertion	eluz2b1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2	1	eluz1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
3		1z	⊢ 1 ∈ ℤ
4		zltp1le	⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 < 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 ) )
5	3 4	mpan	⊢ ( 𝑁 ∈ ℤ → ( 1 < 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 ) )
6		df-2	⊢ 2 = ( 1 + 1 )
7	6	breq1i	⊢ ( 2 ≤ 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 )
8	5 7	bitr4di	⊢ ( 𝑁 ∈ ℤ → ( 1 < 𝑁 ↔ 2 ≤ 𝑁 ) )
9	8	pm5.32i	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
10	2 9	bitr4i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )