Metamath Proof Explorer


Theorem ltmod

Description: A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ltmod.a ( 𝜑𝐴 ∈ ℝ )
ltmod.b ( 𝜑𝐵 ∈ ℝ+ )
ltmod.c ( 𝜑𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,) 𝐴 ) )
Assertion ltmod ( 𝜑 → ( 𝐶 mod 𝐵 ) < ( 𝐴 mod 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ltmod.a ( 𝜑𝐴 ∈ ℝ )
2 ltmod.b ( 𝜑𝐵 ∈ ℝ+ )
3 ltmod.c ( 𝜑𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,) 𝐴 ) )
4 1 2 modcld ( 𝜑 → ( 𝐴 mod 𝐵 ) ∈ ℝ )
5 1 4 resubcld ( 𝜑 → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ )
6 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
7 icossre ( ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,) 𝐴 ) ⊆ ℝ )
8 5 6 7 syl2anc ( 𝜑 → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,) 𝐴 ) ⊆ ℝ )
9 8 3 sseldd ( 𝜑𝐶 ∈ ℝ )
10 2 rpred ( 𝜑𝐵 ∈ ℝ )
11 9 2 rerpdivcld ( 𝜑 → ( 𝐶 / 𝐵 ) ∈ ℝ )
12 11 flcld ( 𝜑 → ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ∈ ℤ )
13 12 zred ( 𝜑 → ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ∈ ℝ )
14 10 13 remulcld ( 𝜑 → ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) ∈ ℝ )
15 5 rexrd ( 𝜑 → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ* )
16 icoltub ( ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ*𝐴 ∈ ℝ*𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,) 𝐴 ) ) → 𝐶 < 𝐴 )
17 15 6 3 16 syl3anc ( 𝜑𝐶 < 𝐴 )
18 9 1 14 17 ltsub1dd ( 𝜑 → ( 𝐶 − ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) ) < ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) ) )
19 icossicc ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,) 𝐴 ) ⊆ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 )
20 19 3 sseldi ( 𝜑𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 ) )
21 1 2 20 lefldiveq ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) )
22 21 eqcomd ( 𝜑 → ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
23 22 oveq2d ( 𝜑 → ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) = ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) )
24 23 oveq2d ( 𝜑 → ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
25 18 24 breqtrd ( 𝜑 → ( 𝐶 − ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) ) < ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
26 modval ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐶 mod 𝐵 ) = ( 𝐶 − ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) ) )
27 9 2 26 syl2anc ( 𝜑 → ( 𝐶 mod 𝐵 ) = ( 𝐶 − ( 𝐵 · ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ) ) )
28 modval ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
29 1 2 28 syl2anc ( 𝜑 → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
30 25 27 29 3brtr4d ( 𝜑 → ( 𝐶 mod 𝐵 ) < ( 𝐴 mod 𝐵 ) )