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

Metamath Proof Explorer

Theorem modnegd

Description: Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses modnegd.1 
|- ( ph -> A e. RR )
modnegd.2 
|- ( ph -> B e. RR )
modnegd.3 
|- ( ph -> C e. RR+ )
modnegd.4 
|- ( ph -> ( A mod C ) = ( B mod C ) )
Assertion modnegd 
|- ( ph -> ( -u A mod C ) = ( -u B mod C ) )

Proof

Step Hyp Ref Expression
1 modnegd.1 
 |-  ( ph -> A e. RR )
2 modnegd.2 
 |-  ( ph -> B e. RR )
3 modnegd.3 
 |-  ( ph -> C e. RR+ )
4 modnegd.4 
 |-  ( ph -> ( A mod C ) = ( B mod C ) )
5 1zzd 
 |-  ( ph -> 1 e. ZZ )
6 5 znegcld 
 |-  ( ph -> -u 1 e. ZZ )
7 modmul1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( -u 1 e. ZZ /\ C e. RR+ ) /\ ( A mod C ) = ( B mod C ) ) -> ( ( A x. -u 1 ) mod C ) = ( ( B x. -u 1 ) mod C ) )
8 1 2 6 3 4 7 syl221anc 
 |-  ( ph -> ( ( A x. -u 1 ) mod C ) = ( ( B x. -u 1 ) mod C ) )
9 1 recnd 
 |-  ( ph -> A e. CC )
10 1cnd 
 |-  ( ph -> 1 e. CC )
11 10 negcld 
 |-  ( ph -> -u 1 e. CC )
12 9 11 mulcomd 
 |-  ( ph -> ( A x. -u 1 ) = ( -u 1 x. A ) )
13 9 mulm1d 
 |-  ( ph -> ( -u 1 x. A ) = -u A )
14 12 13 eqtrd 
 |-  ( ph -> ( A x. -u 1 ) = -u A )
15 14 oveq1d 
 |-  ( ph -> ( ( A x. -u 1 ) mod C ) = ( -u A mod C ) )
16 2 recnd 
 |-  ( ph -> B e. CC )
17 16 11 mulcomd 
 |-  ( ph -> ( B x. -u 1 ) = ( -u 1 x. B ) )
18 16 mulm1d 
 |-  ( ph -> ( -u 1 x. B ) = -u B )
19 17 18 eqtrd 
 |-  ( ph -> ( B x. -u 1 ) = -u B )
20 19 oveq1d 
 |-  ( ph -> ( ( B x. -u 1 ) mod C ) = ( -u B mod C ) )
21 8 15 20 3eqtr3d 
 |-  ( ph -> ( -u A mod C ) = ( -u B mod C ) )