This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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