Description: Special case of ndvdsadd . If an integer D greater than 1 divides N , it does not divide N + 1 . (Contributed by Paul Chapman, 31-Mar-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ndvdsp1 | |- ( ( N e. ZZ /\ D e. NN /\ 1 < D ) -> ( D || N -> -. D || ( N + 1 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn | |- 1 e. NN |
|
| 2 | 1 | jctl | |- ( 1 < D -> ( 1 e. NN /\ 1 < D ) ) |
| 3 | ndvdsadd | |- ( ( N e. ZZ /\ D e. NN /\ ( 1 e. NN /\ 1 < D ) ) -> ( D || N -> -. D || ( N + 1 ) ) ) |
|
| 4 | 2 3 | syl3an3 | |- ( ( N e. ZZ /\ D e. NN /\ 1 < D ) -> ( D || N -> -. D || ( N + 1 ) ) ) |