Metamath Proof Explorer

Theorem dvdsmod

Description: Any number K whose mod base N is divisible by a divisor P of the base is also divisible by P . This means that primes will also be relatively prime to the base when reduced mod N for any base. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion dvdsmod ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝑃 ∥ ( 𝐾 mod 𝑁 ) ↔ 𝑃 ∥ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝐾 ∈ ℤ )
2 1 zred ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝐾 ∈ ℝ )
3 simpl2 ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
4 3 nnrpd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑁 ∈ ℝ+ )
5 modval ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 𝐾 mod 𝑁 ) = ( 𝐾 − ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ) )
6 2 4 5 syl2anc ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝐾 mod 𝑁 ) = ( 𝐾 − ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ) )
7 6 breq2d ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝑃 ∥ ( 𝐾 mod 𝑁 ) ↔ 𝑃 ∥ ( 𝐾 − ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ) ) )
8 simpl1 ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑃 ∈ ℕ )
9 8 nnzd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑃 ∈ ℤ )
10 3 nnzd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
11 2 3 nndivred ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝐾 / 𝑁 ) ∈ ℝ )
12 11 flcld ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ∈ ℤ )
13 simpr ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑃 ∥ 𝑁 )
14 9 10 12 13 dvdsmultr1d ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑃 ∥ ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) )
15 10 12 zmulcld ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ∈ ℤ )
16 15 zcnd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ∈ ℂ )
17 16 subid1d ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) − 0 ) = ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) )
18 14 17 breqtrrd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝑃 ∥ ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) − 0 ) )
19 0zd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 0 ∈ ℤ )
20 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) mod 𝑃 ) = ( 0 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) − 0 ) ) )
21 8 15 19 20 syl3anc ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) mod 𝑃 ) = ( 0 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) − 0 ) ) )
22 18 21 mpbird ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) mod 𝑃 ) = ( 0 mod 𝑃 ) )
23 22 eqeq2d ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( ( 𝐾 mod 𝑃 ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) mod 𝑃 ) ↔ ( 𝐾 mod 𝑃 ) = ( 0 mod 𝑃 ) ) )
24 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ∈ ℤ ) → ( ( 𝐾 mod 𝑃 ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( 𝐾 − ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ) ) )
25 8 1 15 24 syl3anc ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( ( 𝐾 mod 𝑃 ) = ( ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) mod 𝑃 ) ↔ 𝑃 ∥ ( 𝐾 − ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ) ) )
26 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( 𝐾 mod 𝑃 ) = ( 0 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝐾 − 0 ) ) )
27 8 1 19 26 syl3anc ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( ( 𝐾 mod 𝑃 ) = ( 0 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝐾 − 0 ) ) )
28 23 25 27 3bitr3d ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝑃 ∥ ( 𝐾 − ( 𝑁 · ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ) ) ↔ 𝑃 ∥ ( 𝐾 − 0 ) ) )
29 1 zcnd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → 𝐾 ∈ ℂ )
30 29 subid1d ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝐾 − 0 ) = 𝐾 )
31 30 breq2d ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝑃 ∥ ( 𝐾 − 0 ) ↔ 𝑃 ∥ 𝐾 ) )
32 7 28 31 3bitrd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) ∧ 𝑃 ∥ 𝑁 ) → ( 𝑃 ∥ ( 𝐾 mod 𝑁 ) ↔ 𝑃 ∥ 𝐾 ) )