Metamath Proof Explorer


Theorem ndvdssub

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

Proof

Step Hyp Ref Expression
1 nnnn0 ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
2 nnne0 ( 𝐾 ∈ ℕ → 𝐾 ≠ 0 )
3 1 2 jca ( 𝐾 ∈ ℕ → ( 𝐾 ∈ ℕ0𝐾 ≠ 0 ) )
4 df-ne ( 𝐾 ≠ 0 ↔ ¬ 𝐾 = 0 )
5 4 anbi2i ( ( 𝐾 < 𝐷𝐾 ≠ 0 ) ↔ ( 𝐾 < 𝐷 ∧ ¬ 𝐾 = 0 ) )
6 divalg2 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) )
7 breq1 ( 𝑟 = 𝑥 → ( 𝑟 < 𝐷𝑥 < 𝐷 ) )
8 oveq2 ( 𝑟 = 𝑥 → ( 𝑁𝑟 ) = ( 𝑁𝑥 ) )
9 8 breq2d ( 𝑟 = 𝑥 → ( 𝐷 ∥ ( 𝑁𝑟 ) ↔ 𝐷 ∥ ( 𝑁𝑥 ) ) )
10 7 9 anbi12d ( 𝑟 = 𝑥 → ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ↔ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) )
11 10 reu4 ( ∃! 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ↔ ( ∃ 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ∀ 𝑟 ∈ ℕ0𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) ) )
12 6 11 sylib ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑟 ∈ ℕ0 ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ∀ 𝑟 ∈ ℕ0𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) ) )
13 nngt0 ( 𝐷 ∈ ℕ → 0 < 𝐷 )
14 13 3ad2ant2 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → 0 < 𝐷 )
15 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
16 15 subid1d ( 𝑁 ∈ ℤ → ( 𝑁 − 0 ) = 𝑁 )
17 16 breq2d ( 𝑁 ∈ ℤ → ( 𝐷 ∥ ( 𝑁 − 0 ) ↔ 𝐷𝑁 ) )
18 17 biimpar ( ( 𝑁 ∈ ℤ ∧ 𝐷𝑁 ) → 𝐷 ∥ ( 𝑁 − 0 ) )
19 18 3adant2 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → 𝐷 ∥ ( 𝑁 − 0 ) )
20 14 19 jca ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) )
21 20 3expa ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) → ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) )
22 21 anim1ci ( ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) ∧ ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ) → ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) ) )
23 0nn0 0 ∈ ℕ0
24 breq1 ( 𝑥 = 0 → ( 𝑥 < 𝐷 ↔ 0 < 𝐷 ) )
25 oveq2 ( 𝑥 = 0 → ( 𝑁𝑥 ) = ( 𝑁 − 0 ) )
26 25 breq2d ( 𝑥 = 0 → ( 𝐷 ∥ ( 𝑁𝑥 ) ↔ 𝐷 ∥ ( 𝑁 − 0 ) ) )
27 24 26 anbi12d ( 𝑥 = 0 → ( ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ↔ ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) ) )
28 27 anbi2d ( 𝑥 = 0 → ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) ↔ ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) ) ) )
29 eqeq2 ( 𝑥 = 0 → ( 𝑟 = 𝑥𝑟 = 0 ) )
30 28 29 imbi12d ( 𝑥 = 0 → ( ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) ↔ ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) ) → 𝑟 = 0 ) ) )
31 30 rspcv ( 0 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) ) → 𝑟 = 0 ) ) )
32 23 31 ax-mp ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 0 < 𝐷𝐷 ∥ ( 𝑁 − 0 ) ) ) → 𝑟 = 0 ) )
33 22 32 syl5 ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) ∧ ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ) → 𝑟 = 0 ) )
34 33 expd ( ∀ 𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) → ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) )
35 34 ralimi ( ∀ 𝑟 ∈ ℕ0𝑥 ∈ ℕ0 ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ∧ ( 𝑥 < 𝐷𝐷 ∥ ( 𝑁𝑥 ) ) ) → 𝑟 = 𝑥 ) → ∀ 𝑟 ∈ ℕ0 ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) → ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) )
36 12 35 simpl2im ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∀ 𝑟 ∈ ℕ0 ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) → ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) )
37 r19.21v ( ∀ 𝑟 ∈ ℕ0 ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) → ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) ↔ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) )
38 36 37 sylib ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝐷𝑁 ) → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) )
39 38 expd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷𝑁 → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) ) )
40 39 pm2.43i ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷𝑁 → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ) )
41 40 3impia ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) )
42 breq1 ( 𝑟 = 𝐾 → ( 𝑟 < 𝐷𝐾 < 𝐷 ) )
43 oveq2 ( 𝑟 = 𝐾 → ( 𝑁𝑟 ) = ( 𝑁𝐾 ) )
44 43 breq2d ( 𝑟 = 𝐾 → ( 𝐷 ∥ ( 𝑁𝑟 ) ↔ 𝐷 ∥ ( 𝑁𝐾 ) ) )
45 42 44 anbi12d ( 𝑟 = 𝐾 → ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) ↔ ( 𝐾 < 𝐷𝐷 ∥ ( 𝑁𝐾 ) ) ) )
46 eqeq1 ( 𝑟 = 𝐾 → ( 𝑟 = 0 ↔ 𝐾 = 0 ) )
47 45 46 imbi12d ( 𝑟 = 𝐾 → ( ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) ↔ ( ( 𝐾 < 𝐷𝐷 ∥ ( 𝑁𝐾 ) ) → 𝐾 = 0 ) ) )
48 47 rspcv ( 𝐾 ∈ ℕ0 → ( ∀ 𝑟 ∈ ℕ0 ( ( 𝑟 < 𝐷𝐷 ∥ ( 𝑁𝑟 ) ) → 𝑟 = 0 ) → ( ( 𝐾 < 𝐷𝐷 ∥ ( 𝑁𝐾 ) ) → 𝐾 = 0 ) ) )
49 41 48 syl5com ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 𝐾 ∈ ℕ0 → ( ( 𝐾 < 𝐷𝐷 ∥ ( 𝑁𝐾 ) ) → 𝐾 = 0 ) ) )
50 pm4.14 ( ( ( 𝐾 < 𝐷𝐷 ∥ ( 𝑁𝐾 ) ) → 𝐾 = 0 ) ↔ ( ( 𝐾 < 𝐷 ∧ ¬ 𝐾 = 0 ) → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) )
51 49 50 syl6ib ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 𝐾 ∈ ℕ0 → ( ( 𝐾 < 𝐷 ∧ ¬ 𝐾 = 0 ) → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) )
52 5 51 syl7bi ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 𝐾 ∈ ℕ0 → ( ( 𝐾 < 𝐷𝐾 ≠ 0 ) → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) )
53 52 exp4a ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 𝐾 ∈ ℕ0 → ( 𝐾 < 𝐷 → ( 𝐾 ≠ 0 → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) ) )
54 53 com23 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 𝐾 < 𝐷 → ( 𝐾 ∈ ℕ0 → ( 𝐾 ≠ 0 → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) ) )
55 54 imp4a ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 𝐾 < 𝐷 → ( ( 𝐾 ∈ ℕ0𝐾 ≠ 0 ) → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) )
56 3 55 syl7 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( 𝐾 < 𝐷 → ( 𝐾 ∈ ℕ → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) )
57 56 impcomd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷𝑁 ) → ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) )
58 57 3expia ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷𝑁 → ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) )
59 58 com23 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) → ( 𝐷𝑁 → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) ) )
60 59 3impia ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝐾 ∈ ℕ ∧ 𝐾 < 𝐷 ) ) → ( 𝐷𝑁 → ¬ 𝐷 ∥ ( 𝑁𝐾 ) ) )