divalgmod

Description: The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor (compare divalg2 and divalgb ). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by AV, 21-Aug-2021)

		Ref	Expression
	Assertion	divalgmod	$⊢ (N \in ℤ \land D \in ℕ) \to (R = N \mod D \leftrightarrow (R \in ℕ_{0} \land (R < D \land D ∥ (N - R))))$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ N \mod D \in V$
2	1	snid	$⊢ N \mod D \in \{N \mod D\}$
3		eleq1	$⊢ R = N \mod D \to (R \in \{N \mod D\} \leftrightarrow N \mod D \in \{N \mod D\})$
4	2 3	mpbiri	$⊢ R = N \mod D \to R \in \{N \mod D\}$
5		elsni	$⊢ R \in \{N \mod D\} \to R = N \mod D$
6	4 5	impbii	$⊢ R = N \mod D \leftrightarrow R \in \{N \mod D\}$
7		zre	$⊢ N \in ℤ \to N \in ℝ$
8		nnrp	$⊢ D \in ℕ \to D \in ℝ^{+}$
9		modlt	$⊢ (N \in ℝ \land D \in ℝ^{+}) \to N \mod D < D$
10	7 8 9	syl2an	$⊢ (N \in ℤ \land D \in ℕ) \to N \mod D < D$
11		nnre	$⊢ D \in ℕ \to D \in ℝ$
12		nnne0	$⊢ D \in ℕ \to D \neq 0$
13		redivcl	$⊢ (N \in ℝ \land D \in ℝ \land D \neq 0) \to \frac{N}{D} \in ℝ$
14	7 11 12 13	syl3an	$⊢ (N \in ℤ \land D \in ℕ \land D \in ℕ) \to \frac{N}{D} \in ℝ$
15	14	3anidm23	$⊢ (N \in ℤ \land D \in ℕ) \to \frac{N}{D} \in ℝ$
16	15	flcld	$⊢ (N \in ℤ \land D \in ℕ) \to ⌊\frac{N}{D}⌋ \in ℤ$
17		nnz	$⊢ D \in ℕ \to D \in ℤ$
18	17	adantl	$⊢ (N \in ℤ \land D \in ℕ) \to D \in ℤ$
19		zmodcl	$⊢ (N \in ℤ \land D \in ℕ) \to N \mod D \in ℕ_{0}$
20	19	nn0zd	$⊢ (N \in ℤ \land D \in ℕ) \to N \mod D \in ℤ$
21		zsubcl	$⊢ (N \in ℤ \land N \mod D \in ℤ) \to N - (N \mod D) \in ℤ$
22	20 21	syldan	$⊢ (N \in ℤ \land D \in ℕ) \to N - (N \mod D) \in ℤ$
23		nncn	$⊢ D \in ℕ \to D \in ℂ$
24	23	adantl	$⊢ (N \in ℤ \land D \in ℕ) \to D \in ℂ$
25	16	zcnd	$⊢ (N \in ℤ \land D \in ℕ) \to ⌊\frac{N}{D}⌋ \in ℂ$
26	24 25	mulcomd	$⊢ (N \in ℤ \land D \in ℕ) \to D ⌊\frac{N}{D}⌋ = ⌊\frac{N}{D}⌋ D$
27		modval	$⊢ (N \in ℝ \land D \in ℝ^{+}) \to N \mod D = N - D ⌊\frac{N}{D}⌋$
28	7 8 27	syl2an	$⊢ (N \in ℤ \land D \in ℕ) \to N \mod D = N - D ⌊\frac{N}{D}⌋$
29	19	nn0cnd	$⊢ (N \in ℤ \land D \in ℕ) \to N \mod D \in ℂ$
30		zmulcl	$⊢ (D \in ℤ \land ⌊\frac{N}{D}⌋ \in ℤ) \to D ⌊\frac{N}{D}⌋ \in ℤ$
31	17 16 30	syl2an2	$⊢ (N \in ℤ \land D \in ℕ) \to D ⌊\frac{N}{D}⌋ \in ℤ$
32	31	zcnd	$⊢ (N \in ℤ \land D \in ℕ) \to D ⌊\frac{N}{D}⌋ \in ℂ$
33		zcn	$⊢ N \in ℤ \to N \in ℂ$
34	33	adantr	$⊢ (N \in ℤ \land D \in ℕ) \to N \in ℂ$
35	29 32 34	subexsub	$⊢ (N \in ℤ \land D \in ℕ) \to (N \mod D = N - D ⌊\frac{N}{D}⌋ \leftrightarrow D ⌊\frac{N}{D}⌋ = N - (N \mod D))$
36	28 35	mpbid	$⊢ (N \in ℤ \land D \in ℕ) \to D ⌊\frac{N}{D}⌋ = N - (N \mod D)$
37	26 36	eqtr3d	$⊢ (N \in ℤ \land D \in ℕ) \to ⌊\frac{N}{D}⌋ D = N - (N \mod D)$
38		dvds0lem	$⊢ ((⌊\frac{N}{D}⌋ \in ℤ \land D \in ℤ \land N - (N \mod D) \in ℤ) \land ⌊\frac{N}{D}⌋ D = N - (N \mod D)) \to D ∥ (N - (N \mod D))$
39	16 18 22 37 38	syl31anc	$⊢ (N \in ℤ \land D \in ℕ) \to D ∥ (N - (N \mod D))$
40		divalg2	$⊢ (N \in ℤ \land D \in ℕ) \to \exists! z \in ℕ_{0} (z < D \land D ∥ (N - z))$
41		breq1	$⊢ z = N \mod D \to (z < D \leftrightarrow N \mod D < D)$
42		oveq2	$⊢ z = N \mod D \to N - z = N - (N \mod D)$
43	42	breq2d	$⊢ z = N \mod D \to (D ∥ (N - z) \leftrightarrow D ∥ (N - (N \mod D)))$
44	41 43	anbi12d	$⊢ z = N \mod D \to ((z < D \land D ∥ (N - z)) \leftrightarrow (N \mod D < D \land D ∥ (N - (N \mod D))))$
45	44	riota2	$⊢ (N \mod D \in ℕ_{0} \land \exists! z \in ℕ_{0} (z < D \land D ∥ (N - z))) \to ((N \mod D < D \land D ∥ (N - (N \mod D))) \leftrightarrow (ι z \in ℕ_{0} \| (z < D \land D ∥ (N - z))) = N \mod D)$
46	19 40 45	syl2anc	$⊢ (N \in ℤ \land D \in ℕ) \to ((N \mod D < D \land D ∥ (N - (N \mod D))) \leftrightarrow (ι z \in ℕ_{0} \| (z < D \land D ∥ (N - z))) = N \mod D)$
47	10 39 46	mpbi2and	$⊢ (N \in ℤ \land D \in ℕ) \to (ι z \in ℕ_{0} \| (z < D \land D ∥ (N - z))) = N \mod D$
48	47	eqcomd	$⊢ (N \in ℤ \land D \in ℕ) \to N \mod D = (ι z \in ℕ_{0} \| (z < D \land D ∥ (N - z)))$
49	48	sneqd	$⊢ (N \in ℤ \land D \in ℕ) \to \{N \mod D\} = \{(ι z \in ℕ_{0} \| (z < D \land D ∥ (N - z)))\}$
50		snriota	$⊢ \exists! z \in ℕ_{0} (z < D \land D ∥ (N - z)) \to \{z \in ℕ_{0} \| (z < D \land D ∥ (N - z))\} = \{(ι z \in ℕ_{0} \| (z < D \land D ∥ (N - z)))\}$
51	40 50	syl	$⊢ (N \in ℤ \land D \in ℕ) \to \{z \in ℕ_{0} \| (z < D \land D ∥ (N - z))\} = \{(ι z \in ℕ_{0} \| (z < D \land D ∥ (N - z)))\}$
52	49 51	eqtr4d	$⊢ (N \in ℤ \land D \in ℕ) \to \{N \mod D\} = \{z \in ℕ_{0} \| (z < D \land D ∥ (N - z))\}$
53	52	eleq2d	$⊢ (N \in ℤ \land D \in ℕ) \to (R \in \{N \mod D\} \leftrightarrow R \in \{z \in ℕ_{0} \| (z < D \land D ∥ (N - z))\})$
54	6 53	bitrid	$⊢ (N \in ℤ \land D \in ℕ) \to (R = N \mod D \leftrightarrow R \in \{z \in ℕ_{0} \| (z < D \land D ∥ (N - z))\})$
55		breq1	$⊢ z = R \to (z < D \leftrightarrow R < D)$
56		oveq2	$⊢ z = R \to N - z = N - R$
57	56	breq2d	$⊢ z = R \to (D ∥ (N - z) \leftrightarrow D ∥ (N - R))$
58	55 57	anbi12d	$⊢ z = R \to ((z < D \land D ∥ (N - z)) \leftrightarrow (R < D \land D ∥ (N - R)))$
59	58	elrab	$⊢ R \in \{z \in ℕ_{0} \| (z < D \land D ∥ (N - z))\} \leftrightarrow (R \in ℕ_{0} \land (R < D \land D ∥ (N - R)))$
60	54 59	bitrdi	$⊢ (N \in ℤ \land D \in ℕ) \to (R = N \mod D \leftrightarrow (R \in ℕ_{0} \land (R < D \land D ∥ (N - R))))$

Metamath Proof Explorer

Theorem divalgmod

Proof