Metamath Proof Explorer

Theorem ndvdsadd

Description: Corollary of the division algorithm. If an integer D greater than 1 divides N , then it does not divide any of N + 1 , N + 2 ... N + ( D - 1 ) . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion ndvdsadd 
|- ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D || N -> -. D || ( N + K ) ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( K e. NN -> K e. RR )
2 nnre 
 |-  ( D e. NN -> D e. RR )
3 posdif 
 |-  ( ( K e. RR /\ D e. RR ) -> ( K < D <-> 0 < ( D - K ) ) )
4 1 2 3 syl2anr 
 |-  ( ( D e. NN /\ K e. NN ) -> ( K < D <-> 0 < ( D - K ) ) )
5 4 pm5.32i 
 |-  ( ( ( D e. NN /\ K e. NN ) /\ K < D ) <-> ( ( D e. NN /\ K e. NN ) /\ 0 < ( D - K ) ) )
6 nnz 
 |-  ( D e. NN -> D e. ZZ )
7 nnz 
 |-  ( K e. NN -> K e. ZZ )
8 zsubcl 
 |-  ( ( D e. ZZ /\ K e. ZZ ) -> ( D - K ) e. ZZ )
9 6 7 8 syl2an 
 |-  ( ( D e. NN /\ K e. NN ) -> ( D - K ) e. ZZ )
10 elnnz 
 |-  ( ( D - K ) e. NN <-> ( ( D - K ) e. ZZ /\ 0 < ( D - K ) ) )
11 10 biimpri 
 |-  ( ( ( D - K ) e. ZZ /\ 0 < ( D - K ) ) -> ( D - K ) e. NN )
12 9 11 sylan 
 |-  ( ( ( D e. NN /\ K e. NN ) /\ 0 < ( D - K ) ) -> ( D - K ) e. NN )
13 5 12 sylbi 
 |-  ( ( ( D e. NN /\ K e. NN ) /\ K < D ) -> ( D - K ) e. NN )
14 13 anasss 
 |-  ( ( D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D - K ) e. NN )
15 nngt0 
 |-  ( K e. NN -> 0 < K )
16 ltsubpos 
 |-  ( ( K e. RR /\ D e. RR ) -> ( 0 < K <-> ( D - K ) < D ) )
17 1 2 16 syl2an 
 |-  ( ( K e. NN /\ D e. NN ) -> ( 0 < K <-> ( D - K ) < D ) )
18 17 biimpd 
 |-  ( ( K e. NN /\ D e. NN ) -> ( 0 < K -> ( D - K ) < D ) )
19 18 expcom 
 |-  ( D e. NN -> ( K e. NN -> ( 0 < K -> ( D - K ) < D ) ) )
20 15 19 mpdi 
 |-  ( D e. NN -> ( K e. NN -> ( D - K ) < D ) )
21 20 imp 
 |-  ( ( D e. NN /\ K e. NN ) -> ( D - K ) < D )
22 21 adantrr 
 |-  ( ( D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D - K ) < D )
23 14 22 jca 
 |-  ( ( D e. NN /\ ( K e. NN /\ K < D ) ) -> ( ( D - K ) e. NN /\ ( D - K ) < D ) )
24 23 3adant1 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( ( D - K ) e. NN /\ ( D - K ) < D ) )
25 ndvdssub 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( ( D - K ) e. NN /\ ( D - K ) < D ) ) -> ( D || N -> -. D || ( N - ( D - K ) ) ) )
26 24 25 syld3an3 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D || N -> -. D || ( N - ( D - K ) ) ) )
27 zaddcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N + K ) e. ZZ )
28 7 27 sylan2 
 |-  ( ( N e. ZZ /\ K e. NN ) -> ( N + K ) e. ZZ )
29 dvdssubr 
 |-  ( ( D e. ZZ /\ ( N + K ) e. ZZ ) -> ( D || ( N + K ) <-> D || ( ( N + K ) - D ) ) )
30 6 28 29 syl2an 
 |-  ( ( D e. NN /\ ( N e. ZZ /\ K e. NN ) ) -> ( D || ( N + K ) <-> D || ( ( N + K ) - D ) ) )
31 30 an12s 
 |-  ( ( N e. ZZ /\ ( D e. NN /\ K e. NN ) ) -> ( D || ( N + K ) <-> D || ( ( N + K ) - D ) ) )
32 31 3impb 
 |-  ( ( N e. ZZ /\ D e. NN /\ K e. NN ) -> ( D || ( N + K ) <-> D || ( ( N + K ) - D ) ) )
33 zcn 
 |-  ( N e. ZZ -> N e. CC )
34 nncn 
 |-  ( D e. NN -> D e. CC )
35 nncn 
 |-  ( K e. NN -> K e. CC )
36 subsub3 
 |-  ( ( N e. CC /\ D e. CC /\ K e. CC ) -> ( N - ( D - K ) ) = ( ( N + K ) - D ) )
37 33 34 35 36 syl3an 
 |-  ( ( N e. ZZ /\ D e. NN /\ K e. NN ) -> ( N - ( D - K ) ) = ( ( N + K ) - D ) )
38 37 breq2d 
 |-  ( ( N e. ZZ /\ D e. NN /\ K e. NN ) -> ( D || ( N - ( D - K ) ) <-> D || ( ( N + K ) - D ) ) )
39 32 38 bitr4d 
 |-  ( ( N e. ZZ /\ D e. NN /\ K e. NN ) -> ( D || ( N + K ) <-> D || ( N - ( D - K ) ) ) )
40 39 notbid 
 |-  ( ( N e. ZZ /\ D e. NN /\ K e. NN ) -> ( -. D || ( N + K ) <-> -. D || ( N - ( D - K ) ) ) )
41 40 3adant3r 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( -. D || ( N + K ) <-> -. D || ( N - ( D - K ) ) ) )
42 26 41 sylibrd 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D || N -> -. D || ( N + K ) ) )