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 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) ) → ( 𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ ( 𝑁 + 𝐾 ) ) )

Proof

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