Metamath Proof Explorer


Theorem modsubdir

Description: Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008)

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

Proof

Step Hyp Ref Expression
1 modcl
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( A mod C ) e. RR )
2 1 3adant2
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( A mod C ) e. RR )
3 modcl
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( B mod C ) e. RR )
4 3 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( B mod C ) e. RR )
5 2 4 subge0d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( 0 <_ ( ( A mod C ) - ( B mod C ) ) <-> ( B mod C ) <_ ( A mod C ) ) )
6 resubcl
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
7 6 3adant3
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( A - B ) e. RR )
8 simp3
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> C e. RR+ )
9 rerpdivcl
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( A / C ) e. RR )
10 9 flcld
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( |_ ` ( A / C ) ) e. ZZ )
11 10 3adant2
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( |_ ` ( A / C ) ) e. ZZ )
12 rerpdivcl
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( B / C ) e. RR )
13 12 flcld
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. ZZ )
14 13 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. ZZ )
15 11 14 zsubcld
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) e. ZZ )
16 modcyc2
 |-  ( ( ( A - B ) e. RR /\ C e. RR+ /\ ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) e. ZZ ) -> ( ( ( A - B ) - ( C x. ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) ) ) mod C ) = ( ( A - B ) mod C ) )
17 7 8 15 16 syl3anc
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( ( A - B ) - ( C x. ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) ) ) mod C ) = ( ( A - B ) mod C ) )
18 recn
 |-  ( A e. RR -> A e. CC )
19 18 3ad2ant1
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> A e. CC )
20 recn
 |-  ( B e. RR -> B e. CC )
21 20 3ad2ant2
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> B e. CC )
22 rpre
 |-  ( C e. RR+ -> C e. RR )
23 22 adantl
 |-  ( ( A e. RR /\ C e. RR+ ) -> C e. RR )
24 refldivcl
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( |_ ` ( A / C ) ) e. RR )
25 23 24 remulcld
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( A / C ) ) ) e. RR )
26 25 recnd
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( A / C ) ) ) e. CC )
27 26 3adant2
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( A / C ) ) ) e. CC )
28 22 adantl
 |-  ( ( B e. RR /\ C e. RR+ ) -> C e. RR )
29 refldivcl
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. RR )
30 28 29 remulcld
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( B / C ) ) ) e. RR )
31 30 recnd
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( B / C ) ) ) e. CC )
32 31 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( B / C ) ) ) e. CC )
33 19 21 27 32 sub4d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A - B ) - ( ( C x. ( |_ ` ( A / C ) ) ) - ( C x. ( |_ ` ( B / C ) ) ) ) ) = ( ( A - ( C x. ( |_ ` ( A / C ) ) ) ) - ( B - ( C x. ( |_ ` ( B / C ) ) ) ) ) )
34 22 3ad2ant3
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> C e. RR )
35 34 recnd
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> C e. CC )
36 24 recnd
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( |_ ` ( A / C ) ) e. CC )
37 36 3adant2
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( |_ ` ( A / C ) ) e. CC )
38 29 recnd
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. CC )
39 38 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. CC )
40 35 37 39 subdid
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( C x. ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) ) = ( ( C x. ( |_ ` ( A / C ) ) ) - ( C x. ( |_ ` ( B / C ) ) ) ) )
41 40 oveq2d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A - B ) - ( C x. ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) ) ) = ( ( A - B ) - ( ( C x. ( |_ ` ( A / C ) ) ) - ( C x. ( |_ ` ( B / C ) ) ) ) ) )
42 modval
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( A mod C ) = ( A - ( C x. ( |_ ` ( A / C ) ) ) ) )
43 42 3adant2
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( A mod C ) = ( A - ( C x. ( |_ ` ( A / C ) ) ) ) )
44 modval
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( B mod C ) = ( B - ( C x. ( |_ ` ( B / C ) ) ) ) )
45 44 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( B mod C ) = ( B - ( C x. ( |_ ` ( B / C ) ) ) ) )
46 43 45 oveq12d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A mod C ) - ( B mod C ) ) = ( ( A - ( C x. ( |_ ` ( A / C ) ) ) ) - ( B - ( C x. ( |_ ` ( B / C ) ) ) ) ) )
47 33 41 46 3eqtr4d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A - B ) - ( C x. ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) ) ) = ( ( A mod C ) - ( B mod C ) ) )
48 47 oveq1d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( ( A - B ) - ( C x. ( ( |_ ` ( A / C ) ) - ( |_ ` ( B / C ) ) ) ) ) mod C ) = ( ( ( A mod C ) - ( B mod C ) ) mod C ) )
49 17 48 eqtr3d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A - B ) mod C ) = ( ( ( A mod C ) - ( B mod C ) ) mod C ) )
50 49 adantr
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ 0 <_ ( ( A mod C ) - ( B mod C ) ) ) -> ( ( A - B ) mod C ) = ( ( ( A mod C ) - ( B mod C ) ) mod C ) )
51 2 4 resubcld
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A mod C ) - ( B mod C ) ) e. RR )
52 51 adantr
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ 0 <_ ( ( A mod C ) - ( B mod C ) ) ) -> ( ( A mod C ) - ( B mod C ) ) e. RR )
53 simpl3
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ 0 <_ ( ( A mod C ) - ( B mod C ) ) ) -> C e. RR+ )
54 simpr
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ 0 <_ ( ( A mod C ) - ( B mod C ) ) ) -> 0 <_ ( ( A mod C ) - ( B mod C ) ) )
55 modge0
 |-  ( ( B e. RR /\ C e. RR+ ) -> 0 <_ ( B mod C ) )
56 55 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> 0 <_ ( B mod C ) )
57 2 4 subge02d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( 0 <_ ( B mod C ) <-> ( ( A mod C ) - ( B mod C ) ) <_ ( A mod C ) ) )
58 56 57 mpbid
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A mod C ) - ( B mod C ) ) <_ ( A mod C ) )
59 modlt
 |-  ( ( A e. RR /\ C e. RR+ ) -> ( A mod C ) < C )
60 59 3adant2
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( A mod C ) < C )
61 51 2 34 58 60 lelttrd
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( A mod C ) - ( B mod C ) ) < C )
62 61 adantr
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ 0 <_ ( ( A mod C ) - ( B mod C ) ) ) -> ( ( A mod C ) - ( B mod C ) ) < C )
63 modid
 |-  ( ( ( ( ( A mod C ) - ( B mod C ) ) e. RR /\ C e. RR+ ) /\ ( 0 <_ ( ( A mod C ) - ( B mod C ) ) /\ ( ( A mod C ) - ( B mod C ) ) < C ) ) -> ( ( ( A mod C ) - ( B mod C ) ) mod C ) = ( ( A mod C ) - ( B mod C ) ) )
64 52 53 54 62 63 syl22anc
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ 0 <_ ( ( A mod C ) - ( B mod C ) ) ) -> ( ( ( A mod C ) - ( B mod C ) ) mod C ) = ( ( A mod C ) - ( B mod C ) ) )
65 50 64 eqtrd
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ 0 <_ ( ( A mod C ) - ( B mod C ) ) ) -> ( ( A - B ) mod C ) = ( ( A mod C ) - ( B mod C ) ) )
66 modge0
 |-  ( ( ( A - B ) e. RR /\ C e. RR+ ) -> 0 <_ ( ( A - B ) mod C ) )
67 6 66 stoic3
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> 0 <_ ( ( A - B ) mod C ) )
68 67 adantr
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ ( ( A - B ) mod C ) = ( ( A mod C ) - ( B mod C ) ) ) -> 0 <_ ( ( A - B ) mod C ) )
69 simpr
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ ( ( A - B ) mod C ) = ( ( A mod C ) - ( B mod C ) ) ) -> ( ( A - B ) mod C ) = ( ( A mod C ) - ( B mod C ) ) )
70 68 69 breqtrd
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR+ ) /\ ( ( A - B ) mod C ) = ( ( A mod C ) - ( B mod C ) ) ) -> 0 <_ ( ( A mod C ) - ( B mod C ) ) )
71 65 70 impbida
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( 0 <_ ( ( A mod C ) - ( B mod C ) ) <-> ( ( A - B ) mod C ) = ( ( A mod C ) - ( B mod C ) ) ) )
72 5 71 bitr3d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR+ ) -> ( ( B mod C ) <_ ( A mod C ) <-> ( ( A - B ) mod C ) = ( ( A mod C ) - ( B mod C ) ) ) )