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	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (P ∥ (K \mod N) \leftrightarrow P ∥ K)$

Proof

Step	Hyp	Ref	Expression
1		simpl3	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to K \in ℤ$
2	1	zred	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to K \in ℝ$
3		simpl2	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to N \in ℕ$
4	3	nnrpd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to N \in ℝ^{+}$
5		modval	$⊢ (K \in ℝ \land N \in ℝ^{+}) \to K \mod N = K - N ⌊\frac{K}{N}⌋$
6	2 4 5	syl2anc	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to K \mod N = K - N ⌊\frac{K}{N}⌋$
7	6	breq2d	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (P ∥ (K \mod N) \leftrightarrow P ∥ (K - N ⌊\frac{K}{N}⌋))$
8		simpl1	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to P \in ℕ$
9	8	nnzd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to P \in ℤ$
10	3	nnzd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to N \in ℤ$
11	2 3	nndivred	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to \frac{K}{N} \in ℝ$
12	11	flcld	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to ⌊\frac{K}{N}⌋ \in ℤ$
13		simpr	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to P ∥ N$
14	9 10 12 13	dvdsmultr1d	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to P ∥ N ⌊\frac{K}{N}⌋$
15	10 12	zmulcld	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to N ⌊\frac{K}{N}⌋ \in ℤ$
16	15	zcnd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to N ⌊\frac{K}{N}⌋ \in ℂ$
17	16	subid1d	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to N ⌊\frac{K}{N}⌋ - 0 = N ⌊\frac{K}{N}⌋$
18	14 17	breqtrrd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to P ∥ (N ⌊\frac{K}{N}⌋ - 0)$
19		0zd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to 0 \in ℤ$
20		moddvds	$⊢ (P \in ℕ \land N ⌊\frac{K}{N}⌋ \in ℤ \land 0 \in ℤ) \to (N ⌊\frac{K}{N}⌋ \mod P = 0 \mod P \leftrightarrow P ∥ (N ⌊\frac{K}{N}⌋ - 0))$
21	8 15 19 20	syl3anc	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (N ⌊\frac{K}{N}⌋ \mod P = 0 \mod P \leftrightarrow P ∥ (N ⌊\frac{K}{N}⌋ - 0))$
22	18 21	mpbird	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to N ⌊\frac{K}{N}⌋ \mod P = 0 \mod P$
23	22	eqeq2d	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (K \mod P = N ⌊\frac{K}{N}⌋ \mod P \leftrightarrow K \mod P = 0 \mod P)$
24		moddvds	$⊢ (P \in ℕ \land K \in ℤ \land N ⌊\frac{K}{N}⌋ \in ℤ) \to (K \mod P = N ⌊\frac{K}{N}⌋ \mod P \leftrightarrow P ∥ (K - N ⌊\frac{K}{N}⌋))$
25	8 1 15 24	syl3anc	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (K \mod P = N ⌊\frac{K}{N}⌋ \mod P \leftrightarrow P ∥ (K - N ⌊\frac{K}{N}⌋))$
26		moddvds	$⊢ (P \in ℕ \land K \in ℤ \land 0 \in ℤ) \to (K \mod P = 0 \mod P \leftrightarrow P ∥ (K - 0))$
27	8 1 19 26	syl3anc	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (K \mod P = 0 \mod P \leftrightarrow P ∥ (K - 0))$
28	23 25 27	3bitr3d	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (P ∥ (K - N ⌊\frac{K}{N}⌋) \leftrightarrow P ∥ (K - 0))$
29	1	zcnd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to K \in ℂ$
30	29	subid1d	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to K - 0 = K$
31	30	breq2d	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (P ∥ (K - 0) \leftrightarrow P ∥ K)$
32	7 28 31	3bitrd	$⊢ ((P \in ℕ \land N \in ℕ \land K \in ℤ) \land P ∥ N) \to (P ∥ (K \mod N) \leftrightarrow P ∥ K)$

Metamath Proof Explorer

Theorem dvdsmod

Proof