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 ) ) )