Metamath Proof Explorer


Theorem negmod

Description: The negation of a number modulo a positive number is equal to the difference of the modulus and the number modulo the modulus. (Contributed by AV, 5-Jul-2020)

Ref Expression
Assertion negmod
|- ( ( A e. RR /\ N e. RR+ ) -> ( -u A mod N ) = ( ( N - A ) mod N ) )

Proof

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