modaddmulmod

Description: The sum of a real number and the product of a second real number modulo a positive real number and an integer equals the sum of the real number and the product of the other real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

		Ref	Expression
	Assertion	modaddmulmod	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (A + (B \mod M) C) \mod M = (A + B C) \mod M$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2	1	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to A \in ℂ$
3	2	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to A \in ℂ$
4		simpl2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to B \in ℝ$
5		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to M \in ℝ^{+}$
6	4 5	modcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to B \mod M \in ℝ$
7	6	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to B \mod M \in ℂ$
8		zcn	$⊢ C \in ℤ \to C \in ℂ$
9	8	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to C \in ℂ$
10	9	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to C \in ℂ$
11	7 10	mulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (B \mod M) C \in ℂ$
12	3 11	addcomd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to A + (B \mod M) C = (B \mod M) C + A$
13	12	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (A + (B \mod M) C) \mod M = ((B \mod M) C + A) \mod M$
14		zre	$⊢ C \in ℤ \to C \in ℝ$
15	14	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to C \in ℝ$
16	15	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to C \in ℝ$
17	6 16	remulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (B \mod M) C \in ℝ$
18		simpl	$⊢ (B \in ℝ \land C \in ℤ) \to B \in ℝ$
19	14	adantl	$⊢ (B \in ℝ \land C \in ℤ) \to C \in ℝ$
20	18 19	remulcld	$⊢ (B \in ℝ \land C \in ℤ) \to B C \in ℝ$
21	20	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to B C \in ℝ$
22	21	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to B C \in ℝ$
23	22 5	modcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to B C \mod M \in ℝ$
24		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to A \in ℝ$
25	24	anim1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (A \in ℝ \land M \in ℝ^{+})$
26		simpl3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to C \in ℤ$
27		modmulmod	$⊢ (B \in ℝ \land C \in ℤ \land M \in ℝ^{+}) \to (B \mod M) C \mod M = B C \mod M$
28	4 26 5 27	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (B \mod M) C \mod M = B C \mod M$
29		remulcl	$⊢ (B \in ℝ \land C \in ℝ) \to B C \in ℝ$
30	14 29	sylan2	$⊢ (B \in ℝ \land C \in ℤ) \to B C \in ℝ$
31	30	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to B C \in ℝ$
32		modabs2	$⊢ (B C \in ℝ \land M \in ℝ^{+}) \to (B C \mod M) \mod M = B C \mod M$
33	31 32	sylan	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (B C \mod M) \mod M = B C \mod M$
34	28 33	eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (B \mod M) C \mod M = (B C \mod M) \mod M$
35		modadd1	$⊢ (((B \mod M) C \in ℝ \land B C \mod M \in ℝ) \land (A \in ℝ \land M \in ℝ^{+}) \land (B \mod M) C \mod M = (B C \mod M) \mod M) \to ((B \mod M) C + A) \mod M = ((B C \mod M) + A) \mod M$
36	17 23 25 34 35	syl211anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to ((B \mod M) C + A) \mod M = ((B C \mod M) + A) \mod M$
37	31	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to B C \in ℝ$
38	24	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to A \in ℝ$
39		modaddmod	$⊢ (B C \in ℝ \land A \in ℝ \land M \in ℝ^{+}) \to ((B C \mod M) + A) \mod M = (B C + A) \mod M$
40	37 38 5 39	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to ((B C \mod M) + A) \mod M = (B C + A) \mod M$
41		recn	$⊢ B \in ℝ \to B \in ℂ$
42		mulcl	$⊢ (B \in ℂ \land C \in ℂ) \to B C \in ℂ$
43	41 8 42	syl2an	$⊢ (B \in ℝ \land C \in ℤ) \to B C \in ℂ$
44	43	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to B C \in ℂ$
45	44 2	addcomd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℤ) \to B C + A = A + B C$
46	45	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to B C + A = A + B C$
47	46	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (B C + A) \mod M = (A + B C) \mod M$
48	40 47	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to ((B C \mod M) + A) \mod M = (A + B C) \mod M$
49	13 36 48	3eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℤ) \land M \in ℝ^{+}) \to (A + (B \mod M) C) \mod M = (A + B C) \mod M$

Metamath Proof Explorer

Theorem modaddmulmod

Proof