Description: Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | eluz2b3 | |- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz2b2 | |- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) ) |
|
2 | nngt1ne1 | |- ( N e. NN -> ( 1 < N <-> N =/= 1 ) ) |
|
3 | 2 | pm5.32i | |- ( ( N e. NN /\ 1 < N ) <-> ( N e. NN /\ N =/= 1 ) ) |
4 | 1 3 | bitri | |- ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) ) |