Metamath Proof Explorer

Theorem modabs

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

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

Proof

Step Hyp Ref Expression
1 modcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )
2 1 anim1i 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> ( ( A mod B ) e. RR /\ C e. RR+ ) )
3 2 3impa 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) -> ( ( A mod B ) e. RR /\ C e. RR+ ) )
4 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> ( ( A mod B ) e. RR /\ C e. RR+ ) )
5 modge0 
 |-  ( ( A e. RR /\ B e. RR+ ) -> 0 <_ ( A mod B ) )
6 5 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) -> 0 <_ ( A mod B ) )
7 6 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> 0 <_ ( A mod B ) )
8 1 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) -> ( A mod B ) e. RR )
9 8 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> ( A mod B ) e. RR )
10 rpre 
 |-  ( B e. RR+ -> B e. RR )
11 10 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) -> B e. RR )
12 11 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> B e. RR )
13 rpre 
 |-  ( C e. RR+ -> C e. RR )
14 13 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) -> C e. RR )
15 14 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> C e. RR )
16 modlt 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) < B )
17 16 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) -> ( A mod B ) < B )
18 17 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> ( A mod B ) < B )
19 simpr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> B <_ C )
20 9 12 15 18 19 ltletrd 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> ( A mod B ) < C )
21 modid 
 |-  ( ( ( ( A mod B ) e. RR /\ C e. RR+ ) /\ ( 0 <_ ( A mod B ) /\ ( A mod B ) < C ) ) -> ( ( A mod B ) mod C ) = ( A mod B ) )
22 4 7 20 21 syl12anc 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR+ ) /\ B <_ C ) -> ( ( A mod B ) mod C ) = ( A mod B ) )