moddi

Description: Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008)

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

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
2	1	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A \in ℂ$
3		recn	$⊢ B \in ℝ \to B \in ℂ$
4	3	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to B \in ℂ$
5		rpre	$⊢ C \in ℝ^{+} \to C \in ℝ$
6	5	adantl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to C \in ℝ$
7		refldivcl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℝ$
8	6 7	remulcld	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{B}{C}⌋ \in ℝ$
9	8	recnd	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{B}{C}⌋ \in ℂ$
10	9	3adant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to C ⌊\frac{B}{C}⌋ \in ℂ$
11	2 4 10	subdid	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A (B - C ⌊\frac{B}{C}⌋) = A B - A C ⌊\frac{B}{C}⌋$
12		rpcnne0	$⊢ C \in ℝ^{+} \to (C \in ℂ \land C \neq 0)$
13	12	3ad2ant3	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to (C \in ℂ \land C \neq 0)$
14		rpcnne0	$⊢ A \in ℝ^{+} \to (A \in ℂ \land A \neq 0)$
15	14	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to (A \in ℂ \land A \neq 0)$
16		divcan5	$⊢ (B \in ℂ \land (C \in ℂ \land C \neq 0) \land (A \in ℂ \land A \neq 0)) \to \frac{A B}{A C} = \frac{B}{C}$
17	4 13 15 16	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to \frac{A B}{A C} = \frac{B}{C}$
18	17	fveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{A B}{A C}⌋ = ⌊\frac{B}{C}⌋$
19	18	oveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A C ⌊\frac{A B}{A C}⌋ = A C ⌊\frac{B}{C}⌋$
20		rpcn	$⊢ C \in ℝ^{+} \to C \in ℂ$
21	20	3ad2ant3	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to C \in ℂ$
22		rerpdivcl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to \frac{B}{C} \in ℝ$
23		reflcl	$⊢ \frac{B}{C} \in ℝ \to ⌊\frac{B}{C}⌋ \in ℝ$
24	23	recnd	$⊢ \frac{B}{C} \in ℝ \to ⌊\frac{B}{C}⌋ \in ℂ$
25	22 24	syl	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℂ$
26	25	3adant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to ⌊\frac{B}{C}⌋ \in ℂ$
27	2 21 26	mulassd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A C ⌊\frac{B}{C}⌋ = A C ⌊\frac{B}{C}⌋$
28	19 27	eqtr2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A C ⌊\frac{B}{C}⌋ = A C ⌊\frac{A B}{A C}⌋$
29	28	oveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A B - A C ⌊\frac{B}{C}⌋ = A B - A C ⌊\frac{A B}{A C}⌋$
30	11 29	eqtrd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A (B - C ⌊\frac{B}{C}⌋) = A B - A C ⌊\frac{A B}{A C}⌋$
31		modval	$⊢ (B \in ℝ \land C \in ℝ^{+}) \to B \mod C = B - C ⌊\frac{B}{C}⌋$
32	31	3adant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to B \mod C = B - C ⌊\frac{B}{C}⌋$
33	32	oveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A (B \mod C) = A (B - C ⌊\frac{B}{C}⌋)$
34		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
35		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
36	34 35	sylan	$⊢ (A \in ℝ^{+} \land B \in ℝ) \to A B \in ℝ$
37	36	3adant3	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A B \in ℝ$
38		rpmulcl	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+}) \to A C \in ℝ^{+}$
39		modval	$⊢ (A B \in ℝ \land A C \in ℝ^{+}) \to A B \mod A C = A B - A C ⌊\frac{A B}{A C}⌋$
40	37 38 39	3imp3i2an	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A B \mod A C = A B - A C ⌊\frac{A B}{A C}⌋$
41	30 33 40	3eqtr4d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ^{+}) \to A (B \mod C) = A B \mod A C$

Metamath Proof Explorer

Theorem moddi

Proof