This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )