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 N2N1<N

Proof

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