Metamath Proof Explorer


Theorem lefldiveq

Description: A closed enough, smaller real C has the same floor of A when both are divided by B . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses lefldiveq.a ( 𝜑𝐴 ∈ ℝ )
lefldiveq.b ( 𝜑𝐵 ∈ ℝ+ )
lefldiveq.c ( 𝜑𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 ) )
Assertion lefldiveq ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lefldiveq.a ( 𝜑𝐴 ∈ ℝ )
2 lefldiveq.b ( 𝜑𝐵 ∈ ℝ+ )
3 lefldiveq.c ( 𝜑𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 ) )
4 moddiffl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
5 1 2 4 syl2anc ( 𝜑 → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
6 1 2 rerpdivcld ( 𝜑 → ( 𝐴 / 𝐵 ) ∈ ℝ )
7 6 flcld ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℤ )
8 5 7 eqeltrd ( 𝜑 → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ∈ ℤ )
9 flid ( ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ∈ ℤ → ( ⌊ ‘ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ) = ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) )
10 8 9 syl ( 𝜑 → ( ⌊ ‘ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ) = ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) )
11 10 5 eqtr2d ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( ⌊ ‘ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ) )
12 1 2 modcld ( 𝜑 → ( 𝐴 mod 𝐵 ) ∈ ℝ )
13 1 12 resubcld ( 𝜑 → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ )
14 13 2 rerpdivcld ( 𝜑 → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ∈ ℝ )
15 iccssre ( ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 ) ⊆ ℝ )
16 13 1 15 syl2anc ( 𝜑 → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 ) ⊆ ℝ )
17 16 3 sseldd ( 𝜑𝐶 ∈ ℝ )
18 17 2 rerpdivcld ( 𝜑 → ( 𝐶 / 𝐵 ) ∈ ℝ )
19 13 rexrd ( 𝜑 → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ* )
20 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
21 iccgelb ( ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ*𝐴 ∈ ℝ*𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 ) ) → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ≤ 𝐶 )
22 19 20 3 21 syl3anc ( 𝜑 → ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ≤ 𝐶 )
23 13 17 2 22 lediv1dd ( 𝜑 → ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ≤ ( 𝐶 / 𝐵 ) )
24 flwordi ( ( ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ∧ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ≤ ( 𝐶 / 𝐵 ) ) → ( ⌊ ‘ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ) ≤ ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) )
25 14 18 23 24 syl3anc ( 𝜑 → ( ⌊ ‘ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) / 𝐵 ) ) ≤ ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) )
26 11 25 eqbrtrd ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ≤ ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) )
27 iccleub ( ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) ∈ ℝ*𝐴 ∈ ℝ*𝐶 ∈ ( ( 𝐴 − ( 𝐴 mod 𝐵 ) ) [,] 𝐴 ) ) → 𝐶𝐴 )
28 19 20 3 27 syl3anc ( 𝜑𝐶𝐴 )
29 17 1 2 28 lediv1dd ( 𝜑 → ( 𝐶 / 𝐵 ) ≤ ( 𝐴 / 𝐵 ) )
30 flwordi ( ( ( 𝐶 / 𝐵 ) ∈ ℝ ∧ ( 𝐴 / 𝐵 ) ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ≤ ( 𝐴 / 𝐵 ) ) → ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ≤ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
31 18 6 29 30 syl3anc ( 𝜑 → ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ≤ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
32 reflcl ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
33 6 32 syl ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
34 reflcl ( ( 𝐶 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ∈ ℝ )
35 18 34 syl ( 𝜑 → ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ∈ ℝ )
36 33 35 letri3d ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ↔ ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ≤ ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ∧ ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) ≤ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
37 26 31 36 mpbir2and ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) )