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 ∈ ℤ ∧ D ∈ ℕ ∧ K ∈ ℕ ∧ K < D → D ∥ N → ¬ D ∥ N + K

Proof

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