| Step |
Hyp |
Ref |
Expression |
| 1 |
|
recn |
|- ( A e. RR -> A e. CC ) |
| 2 |
|
rpcn |
|- ( B e. RR+ -> B e. CC ) |
| 3 |
|
zcn |
|- ( N e. ZZ -> N e. CC ) |
| 4 |
|
mulneg1 |
|- ( ( N e. CC /\ B e. CC ) -> ( -u N x. B ) = -u ( N x. B ) ) |
| 5 |
4
|
ancoms |
|- ( ( B e. CC /\ N e. CC ) -> ( -u N x. B ) = -u ( N x. B ) ) |
| 6 |
|
mulcom |
|- ( ( B e. CC /\ N e. CC ) -> ( B x. N ) = ( N x. B ) ) |
| 7 |
6
|
negeqd |
|- ( ( B e. CC /\ N e. CC ) -> -u ( B x. N ) = -u ( N x. B ) ) |
| 8 |
5 7
|
eqtr4d |
|- ( ( B e. CC /\ N e. CC ) -> ( -u N x. B ) = -u ( B x. N ) ) |
| 9 |
8
|
3adant1 |
|- ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( -u N x. B ) = -u ( B x. N ) ) |
| 10 |
9
|
oveq2d |
|- ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( A + ( -u N x. B ) ) = ( A + -u ( B x. N ) ) ) |
| 11 |
|
mulcl |
|- ( ( B e. CC /\ N e. CC ) -> ( B x. N ) e. CC ) |
| 12 |
|
negsub |
|- ( ( A e. CC /\ ( B x. N ) e. CC ) -> ( A + -u ( B x. N ) ) = ( A - ( B x. N ) ) ) |
| 13 |
11 12
|
sylan2 |
|- ( ( A e. CC /\ ( B e. CC /\ N e. CC ) ) -> ( A + -u ( B x. N ) ) = ( A - ( B x. N ) ) ) |
| 14 |
13
|
3impb |
|- ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( A + -u ( B x. N ) ) = ( A - ( B x. N ) ) ) |
| 15 |
10 14
|
eqtr2d |
|- ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( A - ( B x. N ) ) = ( A + ( -u N x. B ) ) ) |
| 16 |
1 2 3 15
|
syl3an |
|- ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( A - ( B x. N ) ) = ( A + ( -u N x. B ) ) ) |
| 17 |
16
|
oveq1d |
|- ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( ( A - ( B x. N ) ) mod B ) = ( ( A + ( -u N x. B ) ) mod B ) ) |
| 18 |
|
znegcl |
|- ( N e. ZZ -> -u N e. ZZ ) |
| 19 |
|
modcyc |
|- ( ( A e. RR /\ B e. RR+ /\ -u N e. ZZ ) -> ( ( A + ( -u N x. B ) ) mod B ) = ( A mod B ) ) |
| 20 |
18 19
|
syl3an3 |
|- ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( ( A + ( -u N x. B ) ) mod B ) = ( A mod B ) ) |
| 21 |
17 20
|
eqtrd |
|- ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( ( A - ( B x. N ) ) mod B ) = ( A mod B ) ) |