Metamath Proof Explorer

Theorem modsubdir

Description: Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008)

Ref Expression
Assertion modsubdir ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) ≤ ( 𝐴 mod 𝐶 ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 modcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℝ )
2 1 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℝ )
3 modcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℝ )
4 3 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℝ )
5 2 4 subge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ↔ ( 𝐵 mod 𝐶 ) ≤ ( 𝐴 mod 𝐶 ) ) )
6 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
7 6 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
8 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ+ )
9 rerpdivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 / 𝐶 ) ∈ ℝ )
10 9 flcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ∈ ℤ )
11 10 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ∈ ℤ )
12 rerpdivcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 / 𝐶 ) ∈ ℝ )
13 12 flcld ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℤ )
14 13 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℤ )
15 11 14 zsubcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℤ )
16 modcyc2 ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ∧ ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℤ ) → ( ( ( 𝐴 − 𝐵 ) − ( 𝐶 · ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) mod 𝐶 ) = ( ( 𝐴 − 𝐵 ) mod 𝐶 ) )
17 7 8 15 16 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 − 𝐵 ) − ( 𝐶 · ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) mod 𝐶 ) = ( ( 𝐴 − 𝐵 ) mod 𝐶 ) )
18 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
19 18 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
20 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
21 20 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
22 rpre ⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℝ )
23 22 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
24 refldivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ∈ ℝ )
25 23 24 remulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) ∈ ℝ )
26 25 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) ∈ ℂ )
27 26 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) ∈ ℂ )
28 22 adantl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
29 refldivcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℝ )
30 28 29 remulcld ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℝ )
31 30 recnd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℂ )
32 31 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℂ )
33 19 21 27 32 sub4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 − 𝐵 ) − ( ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 − ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) ) − ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) )
34 22 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
35 34 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
36 24 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ∈ ℂ )
37 36 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ∈ ℂ )
38 29 recnd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ )
39 38 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ )
40 35 37 39 subdid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) = ( ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) )
41 40 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 − 𝐵 ) − ( 𝐶 · ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 − 𝐵 ) − ( ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) )
42 modval ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) = ( 𝐴 − ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) ) )
43 42 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) = ( 𝐴 − ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) ) )
44 modval ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) = ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) )
45 44 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) = ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) )
46 43 45 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) = ( ( 𝐴 − ( 𝐶 · ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) ) ) − ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) )
47 33 41 46 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 − 𝐵 ) − ( 𝐶 · ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) )
48 47 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 − 𝐵 ) − ( 𝐶 · ( ( ⌊ ‘ ( 𝐴 / 𝐶 ) ) − ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) mod 𝐶 ) = ( ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) )
49 17 48 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) )
50 49 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) )
51 2 4 resubcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ∈ ℝ )
52 51 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ∈ ℝ )
53 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → 𝐶 ∈ ℝ+ )
54 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) )
55 modge0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 0 ≤ ( 𝐵 mod 𝐶 ) )
56 55 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 0 ≤ ( 𝐵 mod 𝐶 ) )
57 2 4 subge02d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 0 ≤ ( 𝐵 mod 𝐶 ) ↔ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ≤ ( 𝐴 mod 𝐶 ) ) )
58 56 57 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ≤ ( 𝐴 mod 𝐶 ) )
59 modlt ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) < 𝐶 )
60 59 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) < 𝐶 )
61 51 2 34 58 60 lelttrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) < 𝐶 )
62 61 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) < 𝐶 )
63 modid ⊢ ( ( ( ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ∧ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) < 𝐶 ) ) → ( ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) )
64 52 53 54 62 63 syl22anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → ( ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) )
65 50 64 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) )
66 modge0 ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 0 ≤ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) )
67 6 66 stoic3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 0 ≤ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) )
68 67 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → 0 ≤ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) )
69 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) )
70 68 69 breqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) → 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) )
71 65 70 impbida ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 0 ≤ ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) )
72 5 71 bitr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) ≤ ( 𝐴 mod 𝐶 ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝐶 ) = ( ( 𝐴 mod 𝐶 ) − ( 𝐵 mod 𝐶 ) ) ) )