Description: Alternate proof of nn0ge2m1nn : If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 , a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn . (Contributed by Alexander van der Vekens, 1-Aug-2018) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nn0ge2m1nnALT | |- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2z | |- 2 e. ZZ |
|
| 2 | 1 | a1i | |- ( ( N e. NN0 /\ 2 <_ N ) -> 2 e. ZZ ) |
| 3 | nn0z | |- ( N e. NN0 -> N e. ZZ ) |
|
| 4 | 3 | adantr | |- ( ( N e. NN0 /\ 2 <_ N ) -> N e. ZZ ) |
| 5 | simpr | |- ( ( N e. NN0 /\ 2 <_ N ) -> 2 <_ N ) |
|
| 6 | eluz2 | |- ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) ) |
|
| 7 | 2 4 5 6 | syl3anbrc | |- ( ( N e. NN0 /\ 2 <_ N ) -> N e. ( ZZ>= ` 2 ) ) |
| 8 | uz2m1nn | |- ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN ) |
|
| 9 | 7 8 | syl | |- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN ) |