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