modremain

Description: The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021)

		Ref	Expression
	Assertion	modremain	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (N \mod D = R \leftrightarrow \exists z \in ℤ z D + R = N)$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$⊢ N \mod D = R \leftrightarrow R = N \mod D$
2		divalgmodcl	$⊢ (N \in ℤ \land D \in ℕ \land R \in ℕ_{0}) \to (R = N \mod D \leftrightarrow (R < D \land D ∥ (N - R)))$
3	2	3adant3r	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (R = N \mod D \leftrightarrow (R < D \land D ∥ (N - R)))$
4		ibar	$⊢ R < D \to (D ∥ (N - R) \leftrightarrow (R < D \land D ∥ (N - R)))$
5	4	adantl	$⊢ (R \in ℕ_{0} \land R < D) \to (D ∥ (N - R) \leftrightarrow (R < D \land D ∥ (N - R)))$
6	5	3ad2ant3	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (D ∥ (N - R) \leftrightarrow (R < D \land D ∥ (N - R)))$
7		nnz	$⊢ D \in ℕ \to D \in ℤ$
8	7	3ad2ant2	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to D \in ℤ$
9		simp1	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to N \in ℤ$
10		nn0z	$⊢ R \in ℕ_{0} \to R \in ℤ$
11	10	adantr	$⊢ (R \in ℕ_{0} \land R < D) \to R \in ℤ$
12	11	3ad2ant3	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to R \in ℤ$
13	9 12	zsubcld	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to N - R \in ℤ$
14		divides	$⊢ (D \in ℤ \land N - R \in ℤ) \to (D ∥ (N - R) \leftrightarrow \exists z \in ℤ z D = N - R)$
15	8 13 14	syl2anc	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (D ∥ (N - R) \leftrightarrow \exists z \in ℤ z D = N - R)$
16		eqcom	$⊢ z D = N - R \leftrightarrow N - R = z D$
17		zcn	$⊢ N \in ℤ \to N \in ℂ$
18	17	3ad2ant1	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to N \in ℂ$
19	18	adantr	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to N \in ℂ$
20		nn0cn	$⊢ R \in ℕ_{0} \to R \in ℂ$
21	20	adantr	$⊢ (R \in ℕ_{0} \land R < D) \to R \in ℂ$
22	21	3ad2ant3	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to R \in ℂ$
23	22	adantr	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to R \in ℂ$
24		simpr	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to z \in ℤ$
25	8	adantr	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to D \in ℤ$
26	24 25	zmulcld	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to z D \in ℤ$
27	26	zcnd	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to z D \in ℂ$
28	19 23 27	subadd2d	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to (N - R = z D \leftrightarrow z D + R = N)$
29	16 28	bitrid	$⊢ ((N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \land z \in ℤ) \to (z D = N - R \leftrightarrow z D + R = N)$
30	29	rexbidva	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (\exists z \in ℤ z D = N - R \leftrightarrow \exists z \in ℤ z D + R = N)$
31	15 30	bitrd	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (D ∥ (N - R) \leftrightarrow \exists z \in ℤ z D + R = N)$
32	3 6 31	3bitr2d	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (R = N \mod D \leftrightarrow \exists z \in ℤ z D + R = N)$
33	1 32	bitrid	$⊢ (N \in ℤ \land D \in ℕ \land (R \in ℕ_{0} \land R < D)) \to (N \mod D = R \leftrightarrow \exists z \in ℤ z D + R = N)$

Metamath Proof Explorer

Theorem modremain

Proof