Step |
Hyp |
Ref |
Expression |
1 |
|
rpcn |
|- ( N e. RR+ -> N e. CC ) |
2 |
|
recn |
|- ( A e. RR -> A e. CC ) |
3 |
|
negsub |
|- ( ( N e. CC /\ A e. CC ) -> ( N + -u A ) = ( N - A ) ) |
4 |
1 2 3
|
syl2anr |
|- ( ( A e. RR /\ N e. RR+ ) -> ( N + -u A ) = ( N - A ) ) |
5 |
4
|
eqcomd |
|- ( ( A e. RR /\ N e. RR+ ) -> ( N - A ) = ( N + -u A ) ) |
6 |
5
|
oveq1d |
|- ( ( A e. RR /\ N e. RR+ ) -> ( ( N - A ) mod N ) = ( ( N + -u A ) mod N ) ) |
7 |
1
|
mulid2d |
|- ( N e. RR+ -> ( 1 x. N ) = N ) |
8 |
7
|
adantl |
|- ( ( A e. RR /\ N e. RR+ ) -> ( 1 x. N ) = N ) |
9 |
8
|
oveq1d |
|- ( ( A e. RR /\ N e. RR+ ) -> ( ( 1 x. N ) + -u A ) = ( N + -u A ) ) |
10 |
9
|
oveq1d |
|- ( ( A e. RR /\ N e. RR+ ) -> ( ( ( 1 x. N ) + -u A ) mod N ) = ( ( N + -u A ) mod N ) ) |
11 |
|
1cnd |
|- ( A e. RR -> 1 e. CC ) |
12 |
|
mulcl |
|- ( ( 1 e. CC /\ N e. CC ) -> ( 1 x. N ) e. CC ) |
13 |
11 1 12
|
syl2an |
|- ( ( A e. RR /\ N e. RR+ ) -> ( 1 x. N ) e. CC ) |
14 |
|
renegcl |
|- ( A e. RR -> -u A e. RR ) |
15 |
14
|
recnd |
|- ( A e. RR -> -u A e. CC ) |
16 |
15
|
adantr |
|- ( ( A e. RR /\ N e. RR+ ) -> -u A e. CC ) |
17 |
13 16
|
addcomd |
|- ( ( A e. RR /\ N e. RR+ ) -> ( ( 1 x. N ) + -u A ) = ( -u A + ( 1 x. N ) ) ) |
18 |
17
|
oveq1d |
|- ( ( A e. RR /\ N e. RR+ ) -> ( ( ( 1 x. N ) + -u A ) mod N ) = ( ( -u A + ( 1 x. N ) ) mod N ) ) |
19 |
14
|
adantr |
|- ( ( A e. RR /\ N e. RR+ ) -> -u A e. RR ) |
20 |
|
simpr |
|- ( ( A e. RR /\ N e. RR+ ) -> N e. RR+ ) |
21 |
|
1zzd |
|- ( ( A e. RR /\ N e. RR+ ) -> 1 e. ZZ ) |
22 |
|
modcyc |
|- ( ( -u A e. RR /\ N e. RR+ /\ 1 e. ZZ ) -> ( ( -u A + ( 1 x. N ) ) mod N ) = ( -u A mod N ) ) |
23 |
19 20 21 22
|
syl3anc |
|- ( ( A e. RR /\ N e. RR+ ) -> ( ( -u A + ( 1 x. N ) ) mod N ) = ( -u A mod N ) ) |
24 |
18 23
|
eqtrd |
|- ( ( A e. RR /\ N e. RR+ ) -> ( ( ( 1 x. N ) + -u A ) mod N ) = ( -u A mod N ) ) |
25 |
6 10 24
|
3eqtr2rd |
|- ( ( A e. RR /\ N e. RR+ ) -> ( -u A mod N ) = ( ( N - A ) mod N ) ) |