Metamath Proof Explorer

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 syl5ib ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) ) = ( ( 𝐵 · 𝐶 ) − ( 𝐷 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) → ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) ) )
72 47 71 syld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) → ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) ) )
73 72 3impia ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 · 𝐶 ) mod 𝐷 ) = ( ( 𝐵 · 𝐶 ) mod 𝐷 ) )