Metamath Proof Explorer

Theorem modxai

Description: Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014) (Revised by Mario Carneiro, 5-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 modxai.1 
 |-  N e. NN
2 modxai.2 
 |-  A e. NN
3 modxai.3 
 |-  B e. NN0
4 modxai.4 
 |-  D e. ZZ
5 modxai.5 
 |-  K e. NN0
6 modxai.6 
 |-  M e. NN0
7 modxai.7 
 |-  C e. NN0
8 modxai.8 
 |-  L e. NN0
9 modxai.11 
 |-  ( ( A ^ B ) mod N ) = ( K mod N )
10 modxai.12 
 |-  ( ( A ^ C ) mod N ) = ( L mod N )
11 modxai.9 
 |-  ( B + C ) = E
12 modxai.10 
 |-  ( ( D x. N ) + M ) = ( K x. L )
13 11 oveq2i 
 |-  ( A ^ ( B + C ) ) = ( A ^ E )
14 2 nncni 
 |-  A e. CC
15 expadd 
 |-  ( ( A e. CC /\ B e. NN0 /\ C e. NN0 ) -> ( A ^ ( B + C ) ) = ( ( A ^ B ) x. ( A ^ C ) ) )
16 14 3 7 15 mp3an 
 |-  ( A ^ ( B + C ) ) = ( ( A ^ B ) x. ( A ^ C ) )
17 13 16 eqtr3i 
 |-  ( A ^ E ) = ( ( A ^ B ) x. ( A ^ C ) )
18 17 oveq1i 
 |-  ( ( A ^ E ) mod N ) = ( ( ( A ^ B ) x. ( A ^ C ) ) mod N )
19 nnexpcl 
 |-  ( ( A e. NN /\ B e. NN0 ) -> ( A ^ B ) e. NN )
20 2 3 19 mp2an 
 |-  ( A ^ B ) e. NN
21 20 nnzi 
 |-  ( A ^ B ) e. ZZ
22 21 a1i 
 |-  ( T. -> ( A ^ B ) e. ZZ )
23 5 nn0zi 
 |-  K e. ZZ
24 23 a1i 
 |-  ( T. -> K e. ZZ )
25 nnexpcl 
 |-  ( ( A e. NN /\ C e. NN0 ) -> ( A ^ C ) e. NN )
26 2 7 25 mp2an 
 |-  ( A ^ C ) e. NN
27 26 nnzi 
 |-  ( A ^ C ) e. ZZ
28 27 a1i 
 |-  ( T. -> ( A ^ C ) e. ZZ )
29 8 nn0zi 
 |-  L e. ZZ
30 29 a1i 
 |-  ( T. -> L e. ZZ )
31 nnrp 
 |-  ( N e. NN -> N e. RR+ )
32 1 31 ax-mp 
 |-  N e. RR+
33 32 a1i 
 |-  ( T. -> N e. RR+ )
34 9 a1i 
 |-  ( T. -> ( ( A ^ B ) mod N ) = ( K mod N ) )
35 10 a1i 
 |-  ( T. -> ( ( A ^ C ) mod N ) = ( L mod N ) )
36 22 24 28 30 33 34 35 modmul12d 
 |-  ( T. -> ( ( ( A ^ B ) x. ( A ^ C ) ) mod N ) = ( ( K x. L ) mod N ) )
37 36 mptru 
 |-  ( ( ( A ^ B ) x. ( A ^ C ) ) mod N ) = ( ( K x. L ) mod N )
38 zcn 
 |-  ( D e. ZZ -> D e. CC )
39 4 38 ax-mp 
 |-  D e. CC
40 1 nncni 
 |-  N e. CC
41 39 40 mulcli 
 |-  ( D x. N ) e. CC
42 6 nn0cni 
 |-  M e. CC
43 41 42 addcomi 
 |-  ( ( D x. N ) + M ) = ( M + ( D x. N ) )
44 12 43 eqtr3i 
 |-  ( K x. L ) = ( M + ( D x. N ) )
45 44 oveq1i 
 |-  ( ( K x. L ) mod N ) = ( ( M + ( D x. N ) ) mod N )
46 37 45 eqtri 
 |-  ( ( ( A ^ B ) x. ( A ^ C ) ) mod N ) = ( ( M + ( D x. N ) ) mod N )
47 6 nn0rei 
 |-  M e. RR
48 modcyc 
 |-  ( ( M e. RR /\ N e. RR+ /\ D e. ZZ ) -> ( ( M + ( D x. N ) ) mod N ) = ( M mod N ) )
49 47 32 4 48 mp3an 
 |-  ( ( M + ( D x. N ) ) mod N ) = ( M mod N )
50 46 49 eqtri 
 |-  ( ( ( A ^ B ) x. ( A ^ C ) ) mod N ) = ( M mod N )
51 18 50 eqtri 
 |-  ( ( A ^ E ) mod N ) = ( M mod N )