Metamath Proof Explorer


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 N 2 N 1 < N

Proof

Step Hyp Ref Expression
1 2z 2
2 1 eluz1i N 2 N 2 N
3 1z 1
4 zltp1le 1 N 1 < N 1 + 1 N
5 3 4 mpan N 1 < N 1 + 1 N
6 df-2 2 = 1 + 1
7 6 breq1i 2 N 1 + 1 N
8 5 7 syl6bbr N 1 < N 2 N
9 8 pm5.32i N 1 < N N 2 N
10 2 9 bitr4i N 2 N 1 < N