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

Metamath Proof Explorer

Theorem prmdvdsexp

Description: A prime divides a positive power of an integer iff it divides the integer. (Contributed by Mario Carneiro, 24-Feb-2014) (Revised by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion prmdvdsexp 
|- ( ( P e. Prime /\ A e. ZZ /\ N e. NN ) -> ( P || ( A ^ N ) <-> P || A ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 1 -> ( A ^ m ) = ( A ^ 1 ) )
2 1 breq2d 
 |-  ( m = 1 -> ( P || ( A ^ m ) <-> P || ( A ^ 1 ) ) )
3 2 bibi1d 
 |-  ( m = 1 -> ( ( P || ( A ^ m ) <-> P || A ) <-> ( P || ( A ^ 1 ) <-> P || A ) ) )
4 3 imbi2d 
 |-  ( m = 1 -> ( ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ m ) <-> P || A ) ) <-> ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ 1 ) <-> P || A ) ) ) )
5 oveq2 
 |-  ( m = k -> ( A ^ m ) = ( A ^ k ) )
6 5 breq2d 
 |-  ( m = k -> ( P || ( A ^ m ) <-> P || ( A ^ k ) ) )
7 6 bibi1d 
 |-  ( m = k -> ( ( P || ( A ^ m ) <-> P || A ) <-> ( P || ( A ^ k ) <-> P || A ) ) )
8 7 imbi2d 
 |-  ( m = k -> ( ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ m ) <-> P || A ) ) <-> ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ k ) <-> P || A ) ) ) )
9 oveq2 
 |-  ( m = ( k + 1 ) -> ( A ^ m ) = ( A ^ ( k + 1 ) ) )
10 9 breq2d 
 |-  ( m = ( k + 1 ) -> ( P || ( A ^ m ) <-> P || ( A ^ ( k + 1 ) ) ) )
11 10 bibi1d 
 |-  ( m = ( k + 1 ) -> ( ( P || ( A ^ m ) <-> P || A ) <-> ( P || ( A ^ ( k + 1 ) ) <-> P || A ) ) )
12 11 imbi2d 
 |-  ( m = ( k + 1 ) -> ( ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ m ) <-> P || A ) ) <-> ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ ( k + 1 ) ) <-> P || A ) ) ) )
13 oveq2 
 |-  ( m = N -> ( A ^ m ) = ( A ^ N ) )
14 13 breq2d 
 |-  ( m = N -> ( P || ( A ^ m ) <-> P || ( A ^ N ) ) )
15 14 bibi1d 
 |-  ( m = N -> ( ( P || ( A ^ m ) <-> P || A ) <-> ( P || ( A ^ N ) <-> P || A ) ) )
16 15 imbi2d 
 |-  ( m = N -> ( ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ m ) <-> P || A ) ) <-> ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ N ) <-> P || A ) ) ) )
17 zcn 
 |-  ( A e. ZZ -> A e. CC )
18 17 adantl 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> A e. CC )
19 18 exp1d 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A ^ 1 ) = A )
20 19 breq2d 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ 1 ) <-> P || A ) )
21 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
22 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
23 18 21 22 syl2an 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
24 23 breq2d 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> ( P || ( A ^ ( k + 1 ) ) <-> P || ( ( A ^ k ) x. A ) ) )
25 simpll 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> P e. Prime )
26 simpr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> A e. ZZ )
27 zexpcl 
 |-  ( ( A e. ZZ /\ k e. NN0 ) -> ( A ^ k ) e. ZZ )
28 26 21 27 syl2an 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> ( A ^ k ) e. ZZ )
29 simplr 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> A e. ZZ )
30 euclemma 
 |-  ( ( P e. Prime /\ ( A ^ k ) e. ZZ /\ A e. ZZ ) -> ( P || ( ( A ^ k ) x. A ) <-> ( P || ( A ^ k ) \/ P || A ) ) )
31 25 28 29 30 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> ( P || ( ( A ^ k ) x. A ) <-> ( P || ( A ^ k ) \/ P || A ) ) )
32 24 31 bitrd 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> ( P || ( A ^ ( k + 1 ) ) <-> ( P || ( A ^ k ) \/ P || A ) ) )
33 orbi1 
 |-  ( ( P || ( A ^ k ) <-> P || A ) -> ( ( P || ( A ^ k ) \/ P || A ) <-> ( P || A \/ P || A ) ) )
34 oridm 
 |-  ( ( P || A \/ P || A ) <-> P || A )
35 33 34 bitrdi 
 |-  ( ( P || ( A ^ k ) <-> P || A ) -> ( ( P || ( A ^ k ) \/ P || A ) <-> P || A ) )
36 35 bibi2d 
 |-  ( ( P || ( A ^ k ) <-> P || A ) -> ( ( P || ( A ^ ( k + 1 ) ) <-> ( P || ( A ^ k ) \/ P || A ) ) <-> ( P || ( A ^ ( k + 1 ) ) <-> P || A ) ) )
37 32 36 syl5ibcom 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ k e. NN ) -> ( ( P || ( A ^ k ) <-> P || A ) -> ( P || ( A ^ ( k + 1 ) ) <-> P || A ) ) )
38 37 expcom 
 |-  ( k e. NN -> ( ( P e. Prime /\ A e. ZZ ) -> ( ( P || ( A ^ k ) <-> P || A ) -> ( P || ( A ^ ( k + 1 ) ) <-> P || A ) ) ) )
39 38 a2d 
 |-  ( k e. NN -> ( ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ k ) <-> P || A ) ) -> ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ ( k + 1 ) ) <-> P || A ) ) ) )
40 4 8 12 16 20 39 nnind 
 |-  ( N e. NN -> ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A ^ N ) <-> P || A ) ) )
41 40 impcom 
 |-  ( ( ( P e. Prime /\ A e. ZZ ) /\ N e. NN ) -> ( P || ( A ^ N ) <-> P || A ) )
42 41 3impa 
 |-  ( ( P e. Prime /\ A e. ZZ /\ N e. NN ) -> ( P || ( A ^ N ) <-> P || A ) )