Metamath Proof Explorer

Theorem modid2

Description: Identity law for modulo. (Contributed by NM, 29-Dec-2008)

Ref Expression
Assertion modid2 
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = A <-> ( 0 <_ A /\ A < B ) ) )

Proof

Step Hyp Ref Expression
1 modge0 
 |-  ( ( A e. RR /\ B e. RR+ ) -> 0 <_ ( A mod B ) )
2 modlt 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) < B )
3 1 2 jca 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( 0 <_ ( A mod B ) /\ ( A mod B ) < B ) )
4 breq2 
 |-  ( ( A mod B ) = A -> ( 0 <_ ( A mod B ) <-> 0 <_ A ) )
5 breq1 
 |-  ( ( A mod B ) = A -> ( ( A mod B ) < B <-> A < B ) )
6 4 5 anbi12d 
 |-  ( ( A mod B ) = A -> ( ( 0 <_ ( A mod B ) /\ ( A mod B ) < B ) <-> ( 0 <_ A /\ A < B ) ) )
7 3 6 syl5ibcom 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = A -> ( 0 <_ A /\ A < B ) ) )
8 modid 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = A )
9 8 ex 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( 0 <_ A /\ A < B ) -> ( A mod B ) = A ) )
10 7 9 impbid 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = A <-> ( 0 <_ A /\ A < B ) ) )