Metamath Proof Explorer

Theorem modelico

Description: Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Assertion modelico 
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. ( 0 [,) B ) )

Proof

Step Hyp Ref Expression
1 modcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )
2 modge0 
 |-  ( ( A e. RR /\ B e. RR+ ) -> 0 <_ ( A mod B ) )
3 modlt 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) < B )
4 0re 
 |-  0 e. RR
5 rpxr 
 |-  ( B e. RR+ -> B e. RR* )
6 5 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR* )
7 elico2 
 |-  ( ( 0 e. RR /\ B e. RR* ) -> ( ( A mod B ) e. ( 0 [,) B ) <-> ( ( A mod B ) e. RR /\ 0 <_ ( A mod B ) /\ ( A mod B ) < B ) ) )
8 4 6 7 sylancr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) e. ( 0 [,) B ) <-> ( ( A mod B ) e. RR /\ 0 <_ ( A mod B ) /\ ( A mod B ) < B ) ) )
9 1 2 3 8 mpbir3and 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. ( 0 [,) B ) )