modcyc

Description: The modulo operation is periodic. (Contributed by NM, 10-Nov-2008)

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

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ N \in ℤ \to N \in ℝ$
2		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
3		remulcl	$⊢ (N \in ℝ \land B \in ℝ) \to N B \in ℝ$
4	1 2 3	syl2an	$⊢ (N \in ℤ \land B \in ℝ^{+}) \to N B \in ℝ$
5		readdcl	$⊢ (A \in ℝ \land N B \in ℝ) \to A + N B \in ℝ$
6	4 5	sylan2	$⊢ (A \in ℝ \land (N \in ℤ \land B \in ℝ^{+})) \to A + N B \in ℝ$
7	6	3impb	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to A + N B \in ℝ$
8		simp3	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B \in ℝ^{+}$
9		modval	$⊢ (A + N B \in ℝ \land B \in ℝ^{+}) \to (A + N B) \mod B = A + N B - B ⌊\frac{A + N B}{B}⌋$
10	7 8 9	syl2anc	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to (A + N B) \mod B = A + N B - B ⌊\frac{A + N B}{B}⌋$
11		recn	$⊢ A \in ℝ \to A \in ℂ$
12	11	3ad2ant1	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to A \in ℂ$
13	4	recnd	$⊢ (N \in ℤ \land B \in ℝ^{+}) \to N B \in ℂ$
14	13	3adant1	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to N B \in ℂ$
15		rpcnne0	$⊢ B \in ℝ^{+} \to (B \in ℂ \land B \neq 0)$
16	15	3ad2ant3	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to (B \in ℂ \land B \neq 0)$
17		divdir	$⊢ (A \in ℂ \land N B \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{A + N B}{B} = (\frac{A}{B}) + (\frac{N B}{B})$
18	12 14 16 17	syl3anc	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to \frac{A + N B}{B} = (\frac{A}{B}) + (\frac{N B}{B})$
19		zcn	$⊢ N \in ℤ \to N \in ℂ$
20		divcan4	$⊢ (N \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{N B}{B} = N$
21	20	3expb	$⊢ (N \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{N B}{B} = N$
22	19 15 21	syl2an	$⊢ (N \in ℤ \land B \in ℝ^{+}) \to \frac{N B}{B} = N$
23	22	3adant1	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to \frac{N B}{B} = N$
24	23	oveq2d	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to (\frac{A}{B}) + (\frac{N B}{B}) = (\frac{A}{B}) + N$
25	18 24	eqtrd	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to \frac{A + N B}{B} = (\frac{A}{B}) + N$
26	25	fveq2d	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to ⌊\frac{A + N B}{B}⌋ = ⌊(\frac{A}{B}) + N⌋$
27		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
28	27	3adant2	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
29		simp2	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to N \in ℤ$
30		fladdz	$⊢ (\frac{A}{B} \in ℝ \land N \in ℤ) \to ⌊(\frac{A}{B}) + N⌋ = ⌊\frac{A}{B}⌋ + N$
31	28 29 30	syl2anc	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to ⌊(\frac{A}{B}) + N⌋ = ⌊\frac{A}{B}⌋ + N$
32	26 31	eqtrd	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to ⌊\frac{A + N B}{B}⌋ = ⌊\frac{A}{B}⌋ + N$
33	32	oveq2d	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B ⌊\frac{A + N B}{B}⌋ = B (⌊\frac{A}{B}⌋ + N)$
34		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
35	34	3ad2ant3	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B \in ℂ$
36		reflcl	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \in ℝ$
37	36	recnd	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \in ℂ$
38	27 37	syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℂ$
39	38	3adant2	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℂ$
40	19	3ad2ant2	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to N \in ℂ$
41	35 39 40	adddid	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B (⌊\frac{A}{B}⌋ + N) = B ⌊\frac{A}{B}⌋ + B \cdot N$
42		mulcom	$⊢ (N \in ℂ \land B \in ℂ) \to N B = B \cdot N$
43	19 34 42	syl2an	$⊢ (N \in ℤ \land B \in ℝ^{+}) \to N B = B \cdot N$
44	43	3adant1	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to N B = B \cdot N$
45	44	eqcomd	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B \cdot N = N B$
46	45	oveq2d	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ + B \cdot N = B ⌊\frac{A}{B}⌋ + N B$
47	33 41 46	3eqtrd	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B ⌊\frac{A + N B}{B}⌋ = B ⌊\frac{A}{B}⌋ + N B$
48	47	oveq2d	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to A + N B - B ⌊\frac{A + N B}{B}⌋ = A + N B - (B ⌊\frac{A}{B}⌋ + N B)$
49	34	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℂ$
50	49 38	mulcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ \in ℂ$
51	50	3adant2	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ \in ℂ$
52	12 51 14	pnpcan2d	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to A + N B - (B ⌊\frac{A}{B}⌋ + N B) = A - B ⌊\frac{A}{B}⌋$
53	10 48 52	3eqtrd	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to (A + N B) \mod B = A - B ⌊\frac{A}{B}⌋$
54		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
55	54	3adant2	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
56	53 55	eqtr4d	$⊢ (A \in ℝ \land N \in ℤ \land B \in ℝ^{+}) \to (A + N B) \mod B = A \mod B$
57	56	3com23	$⊢ (A \in ℝ \land B \in ℝ^{+} \land N \in ℤ) \to (A + N B) \mod B = A \mod B$

Metamath Proof Explorer

Theorem modcyc

Proof