This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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