This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐴 − ( 𝐴 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 𝐵 ) )