# Metamath Proof Explorer

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 ${⊢}\left({N}\in ℤ\wedge {D}\in ℕ\wedge \left({K}\in ℕ\wedge {K}<{D}\right)\right)\to \left({D}\parallel {N}\to ¬{D}\parallel \left({N}+{K}\right)\right)$

### Proof

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