muladdmodid

Description: The sum of a positive real number less than an upper bound and the product of an integer and the upper bound is the positive real number modulo the upper bound. (Contributed by AV, 5-Jul-2020)

		Ref	Expression
	Assertion	muladdmodid	$⊢ (N \in ℤ \land M \in ℝ^{+} \land A \in [0, M)) \to (N \cdot M + A) \mod M = A$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ M \in ℝ^{+} \to 0 \in ℝ$
2		rpxr	$⊢ M \in ℝ^{+} \to M \in ℝ^{*}$
3		elico2	$⊢ (0 \in ℝ \land M \in ℝ^{*}) \to (A \in [0, M) \leftrightarrow (A \in ℝ \land 0 \leq A \land A < M))$
4	1 2 3	syl2anc	$⊢ M \in ℝ^{+} \to (A \in [0, M) \leftrightarrow (A \in ℝ \land 0 \leq A \land A < M))$
5	4	adantl	$⊢ (N \in ℤ \land M \in ℝ^{+}) \to (A \in [0, M) \leftrightarrow (A \in ℝ \land 0 \leq A \land A < M))$
6		zcn	$⊢ N \in ℤ \to N \in ℂ$
7		rpcn	$⊢ M \in ℝ^{+} \to M \in ℂ$
8		mulcl	$⊢ (N \in ℂ \land M \in ℂ) \to N \cdot M \in ℂ$
9	6 7 8	syl2an	$⊢ (N \in ℤ \land M \in ℝ^{+}) \to N \cdot M \in ℂ$
10	9	adantr	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to N \cdot M \in ℂ$
11		recn	$⊢ A \in ℝ \to A \in ℂ$
12	11	3ad2ant1	$⊢ (A \in ℝ \land 0 \leq A \land A < M) \to A \in ℂ$
13	12	adantl	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to A \in ℂ$
14	10 13	addcomd	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to N \cdot M + A = A + N \cdot M$
15	14	oveq1d	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to (N \cdot M + A) \mod M = (A + N \cdot M) \mod M$
16		simp1	$⊢ (A \in ℝ \land 0 \leq A \land A < M) \to A \in ℝ$
17	16	adantl	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to A \in ℝ$
18		simpr	$⊢ (N \in ℤ \land M \in ℝ^{+}) \to M \in ℝ^{+}$
19	18	adantr	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to M \in ℝ^{+}$
20		simpll	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to N \in ℤ$
21		modcyc	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to (A + N \cdot M) \mod M = A \mod M$
22	17 19 20 21	syl3anc	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to (A + N \cdot M) \mod M = A \mod M$
23	18 16	anim12ci	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to (A \in ℝ \land M \in ℝ^{+})$
24		3simpc	$⊢ (A \in ℝ \land 0 \leq A \land A < M) \to (0 \leq A \land A < M)$
25	24	adantl	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to (0 \leq A \land A < M)$
26		modid	$⊢ ((A \in ℝ \land M \in ℝ^{+}) \land (0 \leq A \land A < M)) \to A \mod M = A$
27	23 25 26	syl2anc	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to A \mod M = A$
28	15 22 27	3eqtrd	$⊢ ((N \in ℤ \land M \in ℝ^{+}) \land (A \in ℝ \land 0 \leq A \land A < M)) \to (N \cdot M + A) \mod M = A$
29	28	ex	$⊢ (N \in ℤ \land M \in ℝ^{+}) \to ((A \in ℝ \land 0 \leq A \land A < M) \to (N \cdot M + A) \mod M = A)$
30	5 29	sylbid	$⊢ (N \in ℤ \land M \in ℝ^{+}) \to (A \in [0, M) \to (N \cdot M + A) \mod M = A)$
31	30	3impia	$⊢ (N \in ℤ \land M \in ℝ^{+} \land A \in [0, M)) \to (N \cdot M + A) \mod M = A$

Metamath Proof Explorer

Theorem muladdmodid

Proof