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 ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = ( ⌊ ‘ ( 𝐶 / 𝐵 ) ) )