Theorem modmul1

Description: Multiplication property of the modulo operation. Note that the multiplier C must be an integer. (Contributed by NM, 12-Nov-2008)

	Ref	Expression
Assertion	modmul1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		modval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐴 mod 𝐷 ) = ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) )
2		modval	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐵 mod 𝐷 ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) )
3	1 2	eqeqan12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) )
4	3	anandirs	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) )
5	4	adantrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) )
6		oveq1	⊢ ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) → ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) · 𝐶 ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) · 𝐶 ) )
7	5 6	syl6bi	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) → ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) · 𝐶 ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) · 𝐶 ) ) )
8		rpcn	⊢ ( 𝐷 ∈ ℝ+ → 𝐷 ∈ ℂ )
9	8	ad2antll	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐷 ∈ ℂ )
10		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
11	10	ad2antrl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℂ )
12		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐴 / 𝐷 ) ∈ ℝ )
13	12	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℤ )
14	13	zcnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℂ )
15	14	adantrl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℂ )
16	9 11 15	mulassd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐷 · 𝐶 ) · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) = ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) )
17	9 11 15	mul32d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐷 · 𝐶 ) · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) = ( ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) · 𝐶 ) )
18	16 17	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) · 𝐶 ) )
19	18	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐴 · 𝐶 ) − ( ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) · 𝐶 ) ) )
20		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
21	20	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐴 ∈ ℂ )
22	8	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
23	22 14	mulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ∈ ℂ )
24	23	adantrl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ∈ ℂ )
25	21 24 11	subdird	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) · 𝐶 ) ) )
26	19 25	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) · 𝐶 ) )
27	26	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) · 𝐶 ) )
28	8	ad2antll	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐷 ∈ ℂ )
29	10	ad2antrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℂ )
30		rerpdivcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐵 / 𝐷 ) ∈ ℝ )
31	30	flcld	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℤ )
32	31	zcnd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℂ )
33	32	adantrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℂ )
34	28 29 33	mulassd	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐷 · 𝐶 ) · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) = ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) )
35	28 29 33	mul32d	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐷 · 𝐶 ) · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) = ( ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) · 𝐶 ) )
36	34 35	eqtr3d	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) = ( ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) · 𝐶 ) )
37	36	oveq2d	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) = ( ( 𝐵 · 𝐶 ) − ( ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) · 𝐶 ) ) )
38		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
39	38	adantr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐵 ∈ ℂ )
40	8	adantl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
41	40 32	mulcld	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ∈ ℂ )
42	41	adantrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ∈ ℂ )
43	39 42 29	subdird	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) · 𝐶 ) = ( ( 𝐵 · 𝐶 ) − ( ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) · 𝐶 ) ) )
44	37 43	eqtr4d	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) · 𝐶 ) )
45	44	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) · 𝐶 ) )
46	27 45	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) ↔ ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) · 𝐶 ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) · 𝐶 ) ) )
47	7 46	sylibrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) → ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) ) )
48		oveq1	⊢ ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) mod 𝐷 ) )
49		zre	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℝ )
50		remulcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
51	49 50	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
52	51	adantrr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
53		simprr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐷 ∈ ℝ+ )
54		simprl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℤ )
55	13	adantrl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℤ )
56	54 55	zmulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ∈ ℤ )
57		modcyc2	⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ∈ ℤ ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( 𝐴 · 𝐶 ) mod 𝐷 ) )
58	52 53 56 57	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( 𝐴 · 𝐶 ) mod 𝐷 ) )
59	58	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( 𝐴 · 𝐶 ) mod 𝐷 ) )
60		remulcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
61	49 60	sylan2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
62	61	adantrr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
63		simprr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐷 ∈ ℝ+ )
64		simprl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℤ )
65	31	adantrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℤ )
66	64 65	zmulcld	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ∈ ℤ )
67		modcyc2	⊢ ( ( ( 𝐵 · 𝐶 ) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ∈ ℤ ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) )
68	62 63 66 67	syl3anc	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) )
69	68	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) )
70	59 69	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) mod 𝐷 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) mod 𝐷 ) ↔ ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) ) )
71	48 70	imbitrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) → ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) ) )
72	47 71	syld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) → ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) ) )
73	72	3impia	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) )