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 
|- ( ph -> A e. RR )
ltmod.b 
|- ( ph -> B e. RR+ )
ltmod.c 
|- ( ph -> C e. ( ( A - ( A mod B ) ) [,) A ) )
Assertion ltmod 
|- ( ph -> ( C mod B ) < ( A mod B ) )

Proof

Step Hyp Ref Expression
1 ltmod.a 
 |-  ( ph -> A e. RR )
2 ltmod.b 
 |-  ( ph -> B e. RR+ )
3 ltmod.c 
 |-  ( ph -> C e. ( ( A - ( A mod B ) ) [,) A ) )
4 1 2 modcld 
 |-  ( ph -> ( A mod B ) e. RR )
5 1 4 resubcld 
 |-  ( ph -> ( A - ( A mod B ) ) e. RR )
6 1 rexrd 
 |-  ( ph -> A e. RR* )
7 icossre 
 |-  ( ( ( A - ( A mod B ) ) e. RR /\ A e. RR* ) -> ( ( A - ( A mod B ) ) [,) A ) C_ RR )
8 5 6 7 syl2anc 
 |-  ( ph -> ( ( A - ( A mod B ) ) [,) A ) C_ RR )
9 8 3 sseldd 
 |-  ( ph -> C e. RR )
10 2 rpred 
 |-  ( ph -> B e. RR )
11 9 2 rerpdivcld 
 |-  ( ph -> ( C / B ) e. RR )
12 11 flcld 
 |-  ( ph -> ( |_ ` ( C / B ) ) e. ZZ )
13 12 zred 
 |-  ( ph -> ( |_ ` ( C / B ) ) e. RR )
14 10 13 remulcld 
 |-  ( ph -> ( B x. ( |_ ` ( C / B ) ) ) e. RR )
15 5 rexrd 
 |-  ( ph -> ( A - ( A mod B ) ) e. RR* )
16 icoltub 
 |-  ( ( ( A - ( A mod B ) ) e. RR* /\ A e. RR* /\ C e. ( ( A - ( A mod B ) ) [,) A ) ) -> C < A )
17 15 6 3 16 syl3anc 
 |-  ( ph -> C < A )
18 9 1 14 17 ltsub1dd 
 |-  ( ph -> ( C - ( B x. ( |_ ` ( C / B ) ) ) ) < ( A - ( B x. ( |_ ` ( C / B ) ) ) ) )
19 icossicc 
 |-  ( ( A - ( A mod B ) ) [,) A ) C_ ( ( A - ( A mod B ) ) [,] A )
20 19 3 sselid 
 |-  ( ph -> C e. ( ( A - ( A mod B ) ) [,] A ) )
21 1 2 20 lefldiveq 
 |-  ( ph -> ( |_ ` ( A / B ) ) = ( |_ ` ( C / B ) ) )
22 21 eqcomd 
 |-  ( ph -> ( |_ ` ( C / B ) ) = ( |_ ` ( A / B ) ) )
23 22 oveq2d 
 |-  ( ph -> ( B x. ( |_ ` ( C / B ) ) ) = ( B x. ( |_ ` ( A / B ) ) ) )
24 23 oveq2d 
 |-  ( ph -> ( A - ( B x. ( |_ ` ( C / B ) ) ) ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
25 18 24 breqtrd 
 |-  ( ph -> ( C - ( B x. ( |_ ` ( C / B ) ) ) ) < ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
26 modval 
 |-  ( ( C e. RR /\ B e. RR+ ) -> ( C mod B ) = ( C - ( B x. ( |_ ` ( C / B ) ) ) ) )
27 9 2 26 syl2anc 
 |-  ( ph -> ( C mod B ) = ( C - ( B x. ( |_ ` ( C / B ) ) ) ) )
28 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
29 1 2 28 syl2anc 
 |-  ( ph -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
30 25 27 29 3brtr4d 
 |-  ( ph -> ( C mod B ) < ( A mod B ) )