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

Metamath Proof Explorer

Theorem mod2xnegi

Description: Version of mod2xi with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014)

Ref Expression
Hypotheses mod2xnegi.1 
|- A e. NN
mod2xnegi.2 
|- B e. NN0
mod2xnegi.3 
|- D e. ZZ
mod2xnegi.4 
|- K e. NN
mod2xnegi.5 
|- M e. NN0
mod2xnegi.6 
|- L e. NN0
mod2xnegi.10 
|- ( ( A ^ B ) mod N ) = ( L mod N )
mod2xnegi.7 
|- ( 2 x. B ) = E
mod2xnegi.8 
|- ( L + K ) = N
mod2xnegi.9 
|- ( ( D x. N ) + M ) = ( K x. K )
Assertion mod2xnegi 
|- ( ( A ^ E ) mod N ) = ( M mod N )

Proof

Step Hyp Ref Expression
1 mod2xnegi.1 
 |-  A e. NN
2 mod2xnegi.2 
 |-  B e. NN0
3 mod2xnegi.3 
 |-  D e. ZZ
4 mod2xnegi.4 
 |-  K e. NN
5 mod2xnegi.5 
 |-  M e. NN0
6 mod2xnegi.6 
 |-  L e. NN0
7 mod2xnegi.10 
 |-  ( ( A ^ B ) mod N ) = ( L mod N )
8 mod2xnegi.7 
 |-  ( 2 x. B ) = E
9 mod2xnegi.8 
 |-  ( L + K ) = N
10 mod2xnegi.9 
 |-  ( ( D x. N ) + M ) = ( K x. K )
11 nn0nnaddcl 
 |-  ( ( L e. NN0 /\ K e. NN ) -> ( L + K ) e. NN )
12 6 4 11 mp2an 
 |-  ( L + K ) e. NN
13 9 12 eqeltrri 
 |-  N e. NN
14 13 nnzi 
 |-  N e. ZZ
15 zaddcl 
 |-  ( ( N e. ZZ /\ D e. ZZ ) -> ( N + D ) e. ZZ )
16 14 3 15 mp2an 
 |-  ( N + D ) e. ZZ
17 4 nnnn0i 
 |-  K e. NN0
18 17 17 nn0addcli 
 |-  ( K + K ) e. NN0
19 18 nn0zi 
 |-  ( K + K ) e. ZZ
20 zsubcl 
 |-  ( ( ( N + D ) e. ZZ /\ ( K + K ) e. ZZ ) -> ( ( N + D ) - ( K + K ) ) e. ZZ )
21 16 19 20 mp2an 
 |-  ( ( N + D ) - ( K + K ) ) e. ZZ
22 13 nncni 
 |-  N e. CC
23 zcn 
 |-  ( D e. ZZ -> D e. CC )
24 3 23 ax-mp 
 |-  D e. CC
25 22 24 addcli 
 |-  ( N + D ) e. CC
26 4 nncni 
 |-  K e. CC
27 26 26 addcli 
 |-  ( K + K ) e. CC
28 25 27 22 subdiri 
 |-  ( ( ( N + D ) - ( K + K ) ) x. N ) = ( ( ( N + D ) x. N ) - ( ( K + K ) x. N ) )
29 28 oveq1i 
 |-  ( ( ( ( N + D ) - ( K + K ) ) x. N ) + M ) = ( ( ( ( N + D ) x. N ) - ( ( K + K ) x. N ) ) + M )
30 25 22 mulcli 
 |-  ( ( N + D ) x. N ) e. CC
31 5 nn0cni 
 |-  M e. CC
32 27 22 mulcli 
 |-  ( ( K + K ) x. N ) e. CC
33 30 31 32 addsubi 
 |-  ( ( ( ( N + D ) x. N ) + M ) - ( ( K + K ) x. N ) ) = ( ( ( ( N + D ) x. N ) - ( ( K + K ) x. N ) ) + M )
34 10 oveq2i 
 |-  ( ( N x. N ) + ( ( D x. N ) + M ) ) = ( ( N x. N ) + ( K x. K ) )
35 22 26 26 adddii 
 |-  ( N x. ( K + K ) ) = ( ( N x. K ) + ( N x. K ) )
36 34 35 oveq12i 
 |-  ( ( ( N x. N ) + ( ( D x. N ) + M ) ) - ( N x. ( K + K ) ) ) = ( ( ( N x. N ) + ( K x. K ) ) - ( ( N x. K ) + ( N x. K ) ) )
37 22 24 22 adddiri 
 |-  ( ( N + D ) x. N ) = ( ( N x. N ) + ( D x. N ) )
38 37 oveq1i 
 |-  ( ( ( N + D ) x. N ) + M ) = ( ( ( N x. N ) + ( D x. N ) ) + M )
39 22 22 mulcli 
 |-  ( N x. N ) e. CC
40 24 22 mulcli 
 |-  ( D x. N ) e. CC
41 39 40 31 addassi 
 |-  ( ( ( N x. N ) + ( D x. N ) ) + M ) = ( ( N x. N ) + ( ( D x. N ) + M ) )
42 38 41 eqtr2i 
 |-  ( ( N x. N ) + ( ( D x. N ) + M ) ) = ( ( ( N + D ) x. N ) + M )
43 22 27 mulcomi 
 |-  ( N x. ( K + K ) ) = ( ( K + K ) x. N )
44 42 43 oveq12i 
 |-  ( ( ( N x. N ) + ( ( D x. N ) + M ) ) - ( N x. ( K + K ) ) ) = ( ( ( ( N + D ) x. N ) + M ) - ( ( K + K ) x. N ) )
45 36 44 eqtr3i 
 |-  ( ( ( N x. N ) + ( K x. K ) ) - ( ( N x. K ) + ( N x. K ) ) ) = ( ( ( ( N + D ) x. N ) + M ) - ( ( K + K ) x. N ) )
46 mulsub 
 |-  ( ( ( N e. CC /\ K e. CC ) /\ ( N e. CC /\ K e. CC ) ) -> ( ( N - K ) x. ( N - K ) ) = ( ( ( N x. N ) + ( K x. K ) ) - ( ( N x. K ) + ( N x. K ) ) ) )
47 22 26 22 26 46 mp4an 
 |-  ( ( N - K ) x. ( N - K ) ) = ( ( ( N x. N ) + ( K x. K ) ) - ( ( N x. K ) + ( N x. K ) ) )
48 6 nn0cni 
 |-  L e. CC
49 22 26 48 subadd2i 
 |-  ( ( N - K ) = L <-> ( L + K ) = N )
50 9 49 mpbir 
 |-  ( N - K ) = L
51 50 50 oveq12i 
 |-  ( ( N - K ) x. ( N - K ) ) = ( L x. L )
52 47 51 eqtr3i 
 |-  ( ( ( N x. N ) + ( K x. K ) ) - ( ( N x. K ) + ( N x. K ) ) ) = ( L x. L )
53 45 52 eqtr3i 
 |-  ( ( ( ( N + D ) x. N ) + M ) - ( ( K + K ) x. N ) ) = ( L x. L )
54 29 33 53 3eqtr2i 
 |-  ( ( ( ( N + D ) - ( K + K ) ) x. N ) + M ) = ( L x. L )
55 13 1 2 21 6 5 7 8 54 mod2xi 
 |-  ( ( A ^ E ) mod N ) = ( M mod N )