Metamath Proof Explorer

Theorem modlt

Description: The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008)

Ref Expression
Assertion modlt 
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) < B )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 rpcnne0 
 |-  ( B e. RR+ -> ( B e. CC /\ B =/= 0 ) )
3 divcan2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. ( A / B ) ) = A )
4 3 3expb 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( B x. ( A / B ) ) = A )
5 1 2 4 syl2an 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( A / B ) ) = A )
6 5 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( B x. ( A / B ) ) - ( B x. ( |_ ` ( A / B ) ) ) ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
7 rpcn 
 |-  ( B e. RR+ -> B e. CC )
8 7 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
9 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
10 9 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. CC )
11 refldivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. RR )
12 11 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
13 8 10 12 subdid 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( ( A / B ) - ( |_ ` ( A / B ) ) ) ) = ( ( B x. ( A / B ) ) - ( B x. ( |_ ` ( A / B ) ) ) ) )
14 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
15 6 13 14 3eqtr4rd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( B x. ( ( A / B ) - ( |_ ` ( A / B ) ) ) ) )
16 fraclt1 
 |-  ( ( A / B ) e. RR -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < 1 )
17 9 16 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < 1 )
18 divid 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( B / B ) = 1 )
19 2 18 syl 
 |-  ( B e. RR+ -> ( B / B ) = 1 )
20 19 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B / B ) = 1 )
21 17 20 breqtrrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < ( B / B ) )
22 9 11 resubcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) e. RR )
23 rpre 
 |-  ( B e. RR+ -> B e. RR )
24 23 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR )
25 rpregt0 
 |-  ( B e. RR+ -> ( B e. RR /\ 0 < B ) )
26 25 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B e. RR /\ 0 < B ) )
27 ltmuldiv2 
 |-  ( ( ( ( A / B ) - ( |_ ` ( A / B ) ) ) e. RR /\ B e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( B x. ( ( A / B ) - ( |_ ` ( A / B ) ) ) ) < B <-> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < ( B / B ) ) )
28 22 24 26 27 syl3anc 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( B x. ( ( A / B ) - ( |_ ` ( A / B ) ) ) ) < B <-> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < ( B / B ) ) )
29 21 28 mpbird 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( ( A / B ) - ( |_ ` ( A / B ) ) ) ) < B )
30 15 29 eqbrtrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) < B )