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
|- ( ph -> A e. RR )
lefldiveq.b
|- ( ph -> B e. RR+ )
lefldiveq.c
|- ( ph -> C e. ( ( A - ( A mod B ) ) [,] A ) )
Assertion lefldiveq
|- ( ph -> ( |_ ` ( A / B ) ) = ( |_ ` ( C / B ) ) )

Proof

Step Hyp Ref Expression
1 lefldiveq.a
 |-  ( ph -> A e. RR )
2 lefldiveq.b
 |-  ( ph -> B e. RR+ )
3 lefldiveq.c
 |-  ( ph -> C e. ( ( A - ( A mod B ) ) [,] A ) )
4 moddiffl
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) )
5 1 2 4 syl2anc
 |-  ( ph -> ( ( A - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) )
6 1 2 rerpdivcld
 |-  ( ph -> ( A / B ) e. RR )
7 6 flcld
 |-  ( ph -> ( |_ ` ( A / B ) ) e. ZZ )
8 5 7 eqeltrd
 |-  ( ph -> ( ( A - ( A mod B ) ) / B ) e. ZZ )
9 flid
 |-  ( ( ( A - ( A mod B ) ) / B ) e. ZZ -> ( |_ ` ( ( A - ( A mod B ) ) / B ) ) = ( ( A - ( A mod B ) ) / B ) )
10 8 9 syl
 |-  ( ph -> ( |_ ` ( ( A - ( A mod B ) ) / B ) ) = ( ( A - ( A mod B ) ) / B ) )
11 10 5 eqtr2d
 |-  ( ph -> ( |_ ` ( A / B ) ) = ( |_ ` ( ( A - ( A mod B ) ) / B ) ) )
12 1 2 modcld
 |-  ( ph -> ( A mod B ) e. RR )
13 1 12 resubcld
 |-  ( ph -> ( A - ( A mod B ) ) e. RR )
14 13 2 rerpdivcld
 |-  ( ph -> ( ( A - ( A mod B ) ) / B ) e. RR )
15 iccssre
 |-  ( ( ( A - ( A mod B ) ) e. RR /\ A e. RR ) -> ( ( A - ( A mod B ) ) [,] A ) C_ RR )
16 13 1 15 syl2anc
 |-  ( ph -> ( ( A - ( A mod B ) ) [,] A ) C_ RR )
17 16 3 sseldd
 |-  ( ph -> C e. RR )
18 17 2 rerpdivcld
 |-  ( ph -> ( C / B ) e. RR )
19 13 rexrd
 |-  ( ph -> ( A - ( A mod B ) ) e. RR* )
20 1 rexrd
 |-  ( ph -> A e. RR* )
21 iccgelb
 |-  ( ( ( A - ( A mod B ) ) e. RR* /\ A e. RR* /\ C e. ( ( A - ( A mod B ) ) [,] A ) ) -> ( A - ( A mod B ) ) <_ C )
22 19 20 3 21 syl3anc
 |-  ( ph -> ( A - ( A mod B ) ) <_ C )
23 13 17 2 22 lediv1dd
 |-  ( ph -> ( ( A - ( A mod B ) ) / B ) <_ ( C / B ) )
24 flwordi
 |-  ( ( ( ( A - ( A mod B ) ) / B ) e. RR /\ ( C / B ) e. RR /\ ( ( A - ( A mod B ) ) / B ) <_ ( C / B ) ) -> ( |_ ` ( ( A - ( A mod B ) ) / B ) ) <_ ( |_ ` ( C / B ) ) )
25 14 18 23 24 syl3anc
 |-  ( ph -> ( |_ ` ( ( A - ( A mod B ) ) / B ) ) <_ ( |_ ` ( C / B ) ) )
26 11 25 eqbrtrd
 |-  ( ph -> ( |_ ` ( A / B ) ) <_ ( |_ ` ( C / B ) ) )
27 iccleub
 |-  ( ( ( A - ( A mod B ) ) e. RR* /\ A e. RR* /\ C e. ( ( A - ( A mod B ) ) [,] A ) ) -> C <_ A )
28 19 20 3 27 syl3anc
 |-  ( ph -> C <_ A )
29 17 1 2 28 lediv1dd
 |-  ( ph -> ( C / B ) <_ ( A / B ) )
30 flwordi
 |-  ( ( ( C / B ) e. RR /\ ( A / B ) e. RR /\ ( C / B ) <_ ( A / B ) ) -> ( |_ ` ( C / B ) ) <_ ( |_ ` ( A / B ) ) )
31 18 6 29 30 syl3anc
 |-  ( ph -> ( |_ ` ( C / B ) ) <_ ( |_ ` ( A / B ) ) )
32 reflcl
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. RR )
33 6 32 syl
 |-  ( ph -> ( |_ ` ( A / B ) ) e. RR )
34 reflcl
 |-  ( ( C / B ) e. RR -> ( |_ ` ( C / B ) ) e. RR )
35 18 34 syl
 |-  ( ph -> ( |_ ` ( C / B ) ) e. RR )
36 33 35 letri3d
 |-  ( ph -> ( ( |_ ` ( A / B ) ) = ( |_ ` ( C / B ) ) <-> ( ( |_ ` ( A / B ) ) <_ ( |_ ` ( C / B ) ) /\ ( |_ ` ( C / B ) ) <_ ( |_ ` ( A / B ) ) ) ) )
37 26 31 36 mpbir2and
 |-  ( ph -> ( |_ ` ( A / B ) ) = ( |_ ` ( C / B ) ) )