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