Step |
Hyp |
Ref |
Expression |
1 |
|
modcl |
|- ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR ) |
2 |
1
|
3adant2 |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR ) |
3 |
|
simp1 |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> A e. RR ) |
4 |
|
modcl |
|- ( ( B e. RR /\ M e. RR+ ) -> ( B mod M ) e. RR ) |
5 |
4
|
3adant1 |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( B mod M ) e. RR ) |
6 |
|
simp2 |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> B e. RR ) |
7 |
|
simp3 |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> M e. RR+ ) |
8 |
|
modabs2 |
|- ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) ) |
9 |
8
|
3adant2 |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) ) |
10 |
|
modabs2 |
|- ( ( B e. RR /\ M e. RR+ ) -> ( ( B mod M ) mod M ) = ( B mod M ) ) |
11 |
10
|
3adant1 |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( B mod M ) mod M ) = ( B mod M ) ) |
12 |
2 3 5 6 7 9 11
|
modsub12d |
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) - ( B mod M ) ) mod M ) = ( ( A - B ) mod M ) ) |