Metamath Proof Explorer

Theorem modexp

Description: Exponentiation property of the modulo operation, see theorem 5.2(c) in ApostolNT p. 107. (Contributed by Mario Carneiro, 28-Feb-2014)

Ref Expression
Assertion modexp 
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) )

Proof

Step Hyp Ref Expression
1 simp2l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> C e. NN0 )
2 id 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) )
3 2 3adant2l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) )
4 oveq2 
 |-  ( x = 0 -> ( A ^ x ) = ( A ^ 0 ) )
5 4 oveq1d 
 |-  ( x = 0 -> ( ( A ^ x ) mod D ) = ( ( A ^ 0 ) mod D ) )
6 oveq2 
 |-  ( x = 0 -> ( B ^ x ) = ( B ^ 0 ) )
7 6 oveq1d 
 |-  ( x = 0 -> ( ( B ^ x ) mod D ) = ( ( B ^ 0 ) mod D ) )
8 5 7 eqeq12d 
 |-  ( x = 0 -> ( ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) <-> ( ( A ^ 0 ) mod D ) = ( ( B ^ 0 ) mod D ) ) )
9 8 imbi2d 
 |-  ( x = 0 -> ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) ) <-> ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ 0 ) mod D ) = ( ( B ^ 0 ) mod D ) ) ) )
10 oveq2 
 |-  ( x = k -> ( A ^ x ) = ( A ^ k ) )
11 10 oveq1d 
 |-  ( x = k -> ( ( A ^ x ) mod D ) = ( ( A ^ k ) mod D ) )
12 oveq2 
 |-  ( x = k -> ( B ^ x ) = ( B ^ k ) )
13 12 oveq1d 
 |-  ( x = k -> ( ( B ^ x ) mod D ) = ( ( B ^ k ) mod D ) )
14 11 13 eqeq12d 
 |-  ( x = k -> ( ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) <-> ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) )
15 14 imbi2d 
 |-  ( x = k -> ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) ) <-> ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) ) )
16 oveq2 
 |-  ( x = ( k + 1 ) -> ( A ^ x ) = ( A ^ ( k + 1 ) ) )
17 16 oveq1d 
 |-  ( x = ( k + 1 ) -> ( ( A ^ x ) mod D ) = ( ( A ^ ( k + 1 ) ) mod D ) )
18 oveq2 
 |-  ( x = ( k + 1 ) -> ( B ^ x ) = ( B ^ ( k + 1 ) ) )
19 18 oveq1d 
 |-  ( x = ( k + 1 ) -> ( ( B ^ x ) mod D ) = ( ( B ^ ( k + 1 ) ) mod D ) )
20 17 19 eqeq12d 
 |-  ( x = ( k + 1 ) -> ( ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) <-> ( ( A ^ ( k + 1 ) ) mod D ) = ( ( B ^ ( k + 1 ) ) mod D ) ) )
21 20 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) ) <-> ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ ( k + 1 ) ) mod D ) = ( ( B ^ ( k + 1 ) ) mod D ) ) ) )
22 oveq2 
 |-  ( x = C -> ( A ^ x ) = ( A ^ C ) )
23 22 oveq1d 
 |-  ( x = C -> ( ( A ^ x ) mod D ) = ( ( A ^ C ) mod D ) )
24 oveq2 
 |-  ( x = C -> ( B ^ x ) = ( B ^ C ) )
25 24 oveq1d 
 |-  ( x = C -> ( ( B ^ x ) mod D ) = ( ( B ^ C ) mod D ) )
26 23 25 eqeq12d 
 |-  ( x = C -> ( ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) <-> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) ) )
27 26 imbi2d 
 |-  ( x = C -> ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ x ) mod D ) = ( ( B ^ x ) mod D ) ) <-> ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) ) ) )
28 zcn 
 |-  ( A e. ZZ -> A e. CC )
29 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
30 28 29 syl 
 |-  ( A e. ZZ -> ( A ^ 0 ) = 1 )
31 zcn 
 |-  ( B e. ZZ -> B e. CC )
32 exp0 
 |-  ( B e. CC -> ( B ^ 0 ) = 1 )
33 31 32 syl 
 |-  ( B e. ZZ -> ( B ^ 0 ) = 1 )
34 33 eqcomd 
 |-  ( B e. ZZ -> 1 = ( B ^ 0 ) )
35 30 34 sylan9eq 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A ^ 0 ) = ( B ^ 0 ) )
36 35 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A ^ 0 ) mod D ) = ( ( B ^ 0 ) mod D ) )
37 36 3ad2ant1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ 0 ) mod D ) = ( ( B ^ 0 ) mod D ) )
38 simp21l 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> A e. ZZ )
39 simp1 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> k e. NN0 )
40 zexpcl 
 |-  ( ( A e. ZZ /\ k e. NN0 ) -> ( A ^ k ) e. ZZ )
41 38 39 40 syl2anc 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( A ^ k ) e. ZZ )
42 simp21r 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> B e. ZZ )
43 zexpcl 
 |-  ( ( B e. ZZ /\ k e. NN0 ) -> ( B ^ k ) e. ZZ )
44 42 39 43 syl2anc 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( B ^ k ) e. ZZ )
45 simp22 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> D e. RR+ )
46 simp3 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) )
47 simp23 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( A mod D ) = ( B mod D ) )
48 41 44 38 42 45 46 47 modmul12d 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( ( ( A ^ k ) x. A ) mod D ) = ( ( ( B ^ k ) x. B ) mod D ) )
49 38 zcnd 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> A e. CC )
50 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
51 49 39 50 syl2anc 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
52 51 oveq1d 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( ( A ^ ( k + 1 ) ) mod D ) = ( ( ( A ^ k ) x. A ) mod D ) )
53 42 zcnd 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> B e. CC )
54 expp1 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B ^ ( k + 1 ) ) = ( ( B ^ k ) x. B ) )
55 53 39 54 syl2anc 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( B ^ ( k + 1 ) ) = ( ( B ^ k ) x. B ) )
56 55 oveq1d 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( ( B ^ ( k + 1 ) ) mod D ) = ( ( ( B ^ k ) x. B ) mod D ) )
57 48 52 56 3eqtr4d 
 |-  ( ( k e. NN0 /\ ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) /\ ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( ( A ^ ( k + 1 ) ) mod D ) = ( ( B ^ ( k + 1 ) ) mod D ) )
58 57 3exp 
 |-  ( k e. NN0 -> ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) -> ( ( A ^ ( k + 1 ) ) mod D ) = ( ( B ^ ( k + 1 ) ) mod D ) ) ) )
59 58 a2d 
 |-  ( k e. NN0 -> ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ k ) mod D ) = ( ( B ^ k ) mod D ) ) -> ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ ( k + 1 ) ) mod D ) = ( ( B ^ ( k + 1 ) ) mod D ) ) ) )
60 9 15 21 27 37 59 nn0ind 
 |-  ( C e. NN0 -> ( ( ( A e. ZZ /\ B e. ZZ ) /\ D e. RR+ /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) ) )
61 1 3 60 sylc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) )