ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prmpwdvds Unicode version

Theorem prmpwdvds 12300
Description: A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)
Assertion
Ref Expression
prmpwdvds  |-  ( ( ( K  e.  ZZ  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  N  e.  NN )  /\  ( D  ||  ( K  x.  ( P ^ N ) )  /\  -.  D  ||  ( K  x.  ( P ^ ( N  - 
1 ) ) ) ) )  ->  ( P ^ N )  ||  D )

Proof of Theorem prmpwdvds
Dummy variables  k  n  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 5858 . . . . . 6  |-  ( k  =  K  ->  (
k  x.  ( P ^ N ) )  =  ( K  x.  ( P ^ N ) ) )
21breq2d 3999 . . . . 5  |-  ( k  =  K  ->  ( D  ||  ( k  x.  ( P ^ N
) )  <->  D  ||  ( K  x.  ( P ^ N ) ) ) )
3 oveq1 5858 . . . . . . 7  |-  ( k  =  K  ->  (
k  x.  ( P ^ ( N  - 
1 ) ) )  =  ( K  x.  ( P ^ ( N  -  1 ) ) ) )
43breq2d 3999 . . . . . 6  |-  ( k  =  K  ->  ( D  ||  ( k  x.  ( P ^ ( N  -  1 ) ) )  <->  D  ||  ( K  x.  ( P ^ ( N  - 
1 ) ) ) ) )
54notbid 662 . . . . 5  |-  ( k  =  K  ->  ( -.  D  ||  ( k  x.  ( P ^
( N  -  1 ) ) )  <->  -.  D  ||  ( K  x.  ( P ^ ( N  - 
1 ) ) ) ) )
62, 5anbi12d 470 . . . 4  |-  ( k  =  K  ->  (
( D  ||  (
k  x.  ( P ^ N ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  - 
1 ) ) ) )  <->  ( D  ||  ( K  x.  ( P ^ N ) )  /\  -.  D  ||  ( K  x.  ( P ^ ( N  - 
1 ) ) ) ) ) )
76imbi1d 230 . . 3  |-  ( k  =  K  ->  (
( ( D  ||  ( k  x.  ( P ^ N ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  - 
1 ) ) ) )  ->  ( P ^ N )  ||  D
)  <->  ( ( D 
||  ( K  x.  ( P ^ N ) )  /\  -.  D  ||  ( K  x.  ( P ^ ( N  - 
1 ) ) ) )  ->  ( P ^ N )  ||  D
) ) )
8 oveq2 5859 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  ( P ^ x )  =  ( P ^ 1 ) )
98oveq2d 5867 . . . . . . . . . . . 12  |-  ( x  =  1  ->  (
k  x.  ( P ^ x ) )  =  ( k  x.  ( P ^ 1 ) ) )
109breq2d 3999 . . . . . . . . . . 11  |-  ( x  =  1  ->  ( D  ||  ( k  x.  ( P ^ x
) )  <->  D  ||  (
k  x.  ( P ^ 1 ) ) ) )
11 oveq1 5858 . . . . . . . . . . . . . . 15  |-  ( x  =  1  ->  (
x  -  1 )  =  ( 1  -  1 ) )
1211oveq2d 5867 . . . . . . . . . . . . . 14  |-  ( x  =  1  ->  ( P ^ ( x  - 
1 ) )  =  ( P ^ (
1  -  1 ) ) )
1312oveq2d 5867 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  (
k  x.  ( P ^ ( x  - 
1 ) ) )  =  ( k  x.  ( P ^ (
1  -  1 ) ) ) )
1413breq2d 3999 . . . . . . . . . . . 12  |-  ( x  =  1  ->  ( D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) )  <->  D  ||  (
k  x.  ( P ^ ( 1  -  1 ) ) ) ) )
1514notbid 662 . . . . . . . . . . 11  |-  ( x  =  1  ->  ( -.  D  ||  ( k  x.  ( P ^
( x  -  1 ) ) )  <->  -.  D  ||  ( k  x.  ( P ^ ( 1  -  1 ) ) ) ) )
1610, 15anbi12d 470 . . . . . . . . . 10  |-  ( x  =  1  ->  (
( D  ||  (
k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  <->  ( D  ||  ( k  x.  ( P ^ 1 ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( 1  -  1 ) ) ) ) ) )
178breq1d 3997 . . . . . . . . . 10  |-  ( x  =  1  ->  (
( P ^ x
)  ||  D  <->  ( P ^ 1 )  ||  D ) )
1816, 17imbi12d 233 . . . . . . . . 9  |-  ( x  =  1  ->  (
( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  ( ( D  ||  ( k  x.  ( P ^ 1 ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
1  -  1 ) ) ) )  -> 
( P ^ 1 )  ||  D ) ) )
1918ralbidv 2470 . . . . . . . 8  |-  ( x  =  1  ->  ( A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ 1 ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
1  -  1 ) ) ) )  -> 
( P ^ 1 )  ||  D ) ) )
2019imbi2d 229 . . . . . . 7  |-  ( x  =  1  ->  (
( ( D  e.  ZZ  /\  P  e. 
Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ x
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) ) )  -> 
( P ^ x
)  ||  D )
)  <->  ( ( D  e.  ZZ  /\  P  e.  Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ 1 ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
1  -  1 ) ) ) )  -> 
( P ^ 1 )  ||  D ) ) ) )
21 oveq2 5859 . . . . . . . . . . . . 13  |-  ( x  =  n  ->  ( P ^ x )  =  ( P ^ n
) )
2221oveq2d 5867 . . . . . . . . . . . 12  |-  ( x  =  n  ->  (
k  x.  ( P ^ x ) )  =  ( k  x.  ( P ^ n
) ) )
2322breq2d 3999 . . . . . . . . . . 11  |-  ( x  =  n  ->  ( D  ||  ( k  x.  ( P ^ x
) )  <->  D  ||  (
k  x.  ( P ^ n ) ) ) )
24 oveq1 5858 . . . . . . . . . . . . . . 15  |-  ( x  =  n  ->  (
x  -  1 )  =  ( n  - 
1 ) )
2524oveq2d 5867 . . . . . . . . . . . . . 14  |-  ( x  =  n  ->  ( P ^ ( x  - 
1 ) )  =  ( P ^ (
n  -  1 ) ) )
2625oveq2d 5867 . . . . . . . . . . . . 13  |-  ( x  =  n  ->  (
k  x.  ( P ^ ( x  - 
1 ) ) )  =  ( k  x.  ( P ^ (
n  -  1 ) ) ) )
2726breq2d 3999 . . . . . . . . . . . 12  |-  ( x  =  n  ->  ( D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) )  <->  D  ||  (
k  x.  ( P ^ ( n  - 
1 ) ) ) ) )
2827notbid 662 . . . . . . . . . . 11  |-  ( x  =  n  ->  ( -.  D  ||  ( k  x.  ( P ^
( x  -  1 ) ) )  <->  -.  D  ||  ( k  x.  ( P ^ ( n  - 
1 ) ) ) ) )
2923, 28anbi12d 470 . . . . . . . . . 10  |-  ( x  =  n  ->  (
( D  ||  (
k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  <->  ( D  ||  ( k  x.  ( P ^ n ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( n  - 
1 ) ) ) ) ) )
3021breq1d 3997 . . . . . . . . . 10  |-  ( x  =  n  ->  (
( P ^ x
)  ||  D  <->  ( P ^ n )  ||  D ) )
3129, 30imbi12d 233 . . . . . . . . 9  |-  ( x  =  n  ->  (
( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  ( ( D  ||  ( k  x.  ( P ^ n
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )
) )
3231ralbidv 2470 . . . . . . . 8  |-  ( x  =  n  ->  ( A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ n
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )
) )
3332imbi2d 229 . . . . . . 7  |-  ( x  =  n  ->  (
( ( D  e.  ZZ  /\  P  e. 
Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ x
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) ) )  -> 
( P ^ x
)  ||  D )
)  <->  ( ( D  e.  ZZ  /\  P  e.  Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ n
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )
) ) )
34 oveq2 5859 . . . . . . . . . . . . 13  |-  ( x  =  ( n  + 
1 )  ->  ( P ^ x )  =  ( P ^ (
n  +  1 ) ) )
3534oveq2d 5867 . . . . . . . . . . . 12  |-  ( x  =  ( n  + 
1 )  ->  (
k  x.  ( P ^ x ) )  =  ( k  x.  ( P ^ (
n  +  1 ) ) ) )
3635breq2d 3999 . . . . . . . . . . 11  |-  ( x  =  ( n  + 
1 )  ->  ( D  ||  ( k  x.  ( P ^ x
) )  <->  D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) ) ) )
37 oveq1 5858 . . . . . . . . . . . . . . 15  |-  ( x  =  ( n  + 
1 )  ->  (
x  -  1 )  =  ( ( n  +  1 )  - 
1 ) )
3837oveq2d 5867 . . . . . . . . . . . . . 14  |-  ( x  =  ( n  + 
1 )  ->  ( P ^ ( x  - 
1 ) )  =  ( P ^ (
( n  +  1 )  -  1 ) ) )
3938oveq2d 5867 . . . . . . . . . . . . 13  |-  ( x  =  ( n  + 
1 )  ->  (
k  x.  ( P ^ ( x  - 
1 ) ) )  =  ( k  x.  ( P ^ (
( n  +  1 )  -  1 ) ) ) )
4039breq2d 3999 . . . . . . . . . . . 12  |-  ( x  =  ( n  + 
1 )  ->  ( D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) )  <->  D  ||  (
k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) ) )
4140notbid 662 . . . . . . . . . . 11  |-  ( x  =  ( n  + 
1 )  ->  ( -.  D  ||  ( k  x.  ( P ^
( x  -  1 ) ) )  <->  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) ) )
4236, 41anbi12d 470 . . . . . . . . . 10  |-  ( x  =  ( n  + 
1 )  ->  (
( D  ||  (
k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  <->  ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) ) ) )
4334breq1d 3997 . . . . . . . . . 10  |-  ( x  =  ( n  + 
1 )  ->  (
( P ^ x
)  ||  D  <->  ( P ^ ( n  + 
1 ) )  ||  D ) )
4442, 43imbi12d 233 . . . . . . . . 9  |-  ( x  =  ( n  + 
1 )  ->  (
( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  ( ( D  ||  ( k  x.  ( P ^ (
n  +  1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
( n  +  1 )  -  1 ) ) ) )  -> 
( P ^ (
n  +  1 ) )  ||  D ) ) )
4544ralbidv 2470 . . . . . . . 8  |-  ( x  =  ( n  + 
1 )  ->  ( A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ (
n  +  1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
( n  +  1 )  -  1 ) ) ) )  -> 
( P ^ (
n  +  1 ) )  ||  D ) ) )
4645imbi2d 229 . . . . . . 7  |-  ( x  =  ( n  + 
1 )  ->  (
( ( D  e.  ZZ  /\  P  e. 
Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ x
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) ) )  -> 
( P ^ x
)  ||  D )
)  <->  ( ( D  e.  ZZ  /\  P  e.  Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ (
n  +  1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
( n  +  1 )  -  1 ) ) ) )  -> 
( P ^ (
n  +  1 ) )  ||  D ) ) ) )
47 oveq2 5859 . . . . . . . . . . . . 13  |-  ( x  =  N  ->  ( P ^ x )  =  ( P ^ N
) )
4847oveq2d 5867 . . . . . . . . . . . 12  |-  ( x  =  N  ->  (
k  x.  ( P ^ x ) )  =  ( k  x.  ( P ^ N
) ) )
4948breq2d 3999 . . . . . . . . . . 11  |-  ( x  =  N  ->  ( D  ||  ( k  x.  ( P ^ x
) )  <->  D  ||  (
k  x.  ( P ^ N ) ) ) )
50 oveq1 5858 . . . . . . . . . . . . . . 15  |-  ( x  =  N  ->  (
x  -  1 )  =  ( N  - 
1 ) )
5150oveq2d 5867 . . . . . . . . . . . . . 14  |-  ( x  =  N  ->  ( P ^ ( x  - 
1 ) )  =  ( P ^ ( N  -  1 ) ) )
5251oveq2d 5867 . . . . . . . . . . . . 13  |-  ( x  =  N  ->  (
k  x.  ( P ^ ( x  - 
1 ) ) )  =  ( k  x.  ( P ^ ( N  -  1 ) ) ) )
5352breq2d 3999 . . . . . . . . . . . 12  |-  ( x  =  N  ->  ( D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) )  <->  D  ||  (
k  x.  ( P ^ ( N  - 
1 ) ) ) ) )
5453notbid 662 . . . . . . . . . . 11  |-  ( x  =  N  ->  ( -.  D  ||  ( k  x.  ( P ^
( x  -  1 ) ) )  <->  -.  D  ||  ( k  x.  ( P ^ ( N  - 
1 ) ) ) ) )
5549, 54anbi12d 470 . . . . . . . . . 10  |-  ( x  =  N  ->  (
( D  ||  (
k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  <->  ( D  ||  ( k  x.  ( P ^ N ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  - 
1 ) ) ) ) ) )
5647breq1d 3997 . . . . . . . . . 10  |-  ( x  =  N  ->  (
( P ^ x
)  ||  D  <->  ( P ^ N )  ||  D
) )
5755, 56imbi12d 233 . . . . . . . . 9  |-  ( x  =  N  ->  (
( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  ( ( D  ||  ( k  x.  ( P ^ N
) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  -  1 ) ) ) )  -> 
( P ^ N
)  ||  D )
) )
5857ralbidv 2470 . . . . . . . 8  |-  ( x  =  N  ->  ( A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ x ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( x  - 
1 ) ) ) )  ->  ( P ^ x )  ||  D )  <->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ N
) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  -  1 ) ) ) )  -> 
( P ^ N
)  ||  D )
) )
5958imbi2d 229 . . . . . . 7  |-  ( x  =  N  ->  (
( ( D  e.  ZZ  /\  P  e. 
Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ x
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
x  -  1 ) ) ) )  -> 
( P ^ x
)  ||  D )
)  <->  ( ( D  e.  ZZ  /\  P  e.  Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ N
) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  -  1 ) ) ) )  -> 
( P ^ N
)  ||  D )
) ) )
60 breq1 3990 . . . . . . . . . . . . . 14  |-  ( x  =  D  ->  (
x  ||  ( k  x.  P )  <->  D  ||  (
k  x.  P ) ) )
61 breq1 3990 . . . . . . . . . . . . . . 15  |-  ( x  =  D  ->  (
x  ||  k  <->  D  ||  k
) )
6261notbid 662 . . . . . . . . . . . . . 14  |-  ( x  =  D  ->  ( -.  x  ||  k  <->  -.  D  ||  k ) )
6360, 62anbi12d 470 . . . . . . . . . . . . 13  |-  ( x  =  D  ->  (
( x  ||  (
k  x.  P )  /\  -.  x  ||  k )  <->  ( D  ||  ( k  x.  P
)  /\  -.  D  ||  k ) ) )
64 breq2 3991 . . . . . . . . . . . . 13  |-  ( x  =  D  ->  ( P  ||  x  <->  P  ||  D
) )
6563, 64imbi12d 233 . . . . . . . . . . . 12  |-  ( x  =  D  ->  (
( ( x  ||  ( k  x.  P
)  /\  -.  x  ||  k )  ->  P  ||  x )  <->  ( ( D  ||  ( k  x.  P )  /\  -.  D  ||  k )  ->  P  ||  D ) ) )
6665imbi2d 229 . . . . . . . . . . 11  |-  ( x  =  D  ->  (
( ( P  e. 
Prime  /\  k  e.  ZZ )  ->  ( ( x 
||  ( k  x.  P )  /\  -.  x  ||  k )  ->  P  ||  x ) )  <-> 
( ( P  e. 
Prime  /\  k  e.  ZZ )  ->  ( ( D 
||  ( k  x.  P )  /\  -.  D  ||  k )  ->  P  ||  D ) ) ) )
67 simplrl 530 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  ->  P  e.  Prime )
68 prmnn 12057 . . . . . . . . . . . . . . . 16  |-  ( P  e.  Prime  ->  P  e.  NN )
6967, 68syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  ->  P  e.  NN )
70 simpll 524 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  ->  x  e.  ZZ )
71 dvdsdc 11753 . . . . . . . . . . . . . . 15  |-  ( ( P  e.  NN  /\  x  e.  ZZ )  -> DECID  P 
||  x )
7269, 70, 71syl2anc 409 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  -> DECID  P  ||  x )
73 coprm 12091 . . . . . . . . . . . . . . . 16  |-  ( ( P  e.  Prime  /\  x  e.  ZZ )  ->  ( -.  P  ||  x  <->  ( P  gcd  x )  =  1 ) )
7467, 70, 73syl2anc 409 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  ->  ( -.  P  ||  x  <->  ( P  gcd  x )  =  1 ) )
75 zcn 9210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ZZ  ->  k  e.  CC )
7675ad2antll 488 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  k  e.  CC )
77 prmz 12058 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  Prime  ->  P  e.  ZZ )
7877ad2antrl 487 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  P  e.  ZZ )
7978zcnd 9328 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  P  e.  CC )
8076, 79mulcomd 7934 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( k  x.  P )  =  ( P  x.  k ) )
8180breq2d 3999 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( x  ||  ( k  x.  P
)  <->  x  ||  ( P  x.  k ) ) )
82 simpl 108 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  x  e.  ZZ )
8378, 82gcdcomd 11922 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( P  gcd  x )  =  ( x  gcd  P ) )
8483eqeq1d 2179 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( ( P  gcd  x )  =  1  <->  ( x  gcd  P )  =  1 ) )
8581, 84anbi12d 470 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( (
x  ||  ( k  x.  P )  /\  ( P  gcd  x )  =  1 )  <->  ( x  ||  ( P  x.  k
)  /\  ( x  gcd  P )  =  1 ) ) )
86 simprr 527 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  k  e.  ZZ )
87 coprmdvds 12039 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  P  e.  ZZ  /\  k  e.  ZZ )  ->  (
( x  ||  ( P  x.  k )  /\  ( x  gcd  P
)  =  1 )  ->  x  ||  k
) )
8882, 78, 86, 87syl3anc 1233 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( (
x  ||  ( P  x.  k )  /\  (
x  gcd  P )  =  1 )  ->  x  ||  k ) )
8985, 88sylbid 149 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( (
x  ||  ( k  x.  P )  /\  ( P  gcd  x )  =  1 )  ->  x  ||  k ) )
9089expdimp 257 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  ->  (
( P  gcd  x
)  =  1  ->  x  ||  k ) )
9174, 90sylbid 149 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  ->  ( -.  P  ||  x  ->  x  ||  k ) )
92 con1dc 851 . . . . . . . . . . . . . 14  |-  (DECID  P  ||  x  ->  ( ( -.  P  ||  x  ->  x  ||  k )  -> 
( -.  x  ||  k  ->  P  ||  x
) ) )
9372, 91, 92sylc 62 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  ||  ( k  x.  P
) )  ->  ( -.  x  ||  k  ->  P  ||  x ) )
9493expimpd 361 . . . . . . . . . . . 12  |-  ( ( x  e.  ZZ  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( (
x  ||  ( k  x.  P )  /\  -.  x  ||  k )  ->  P  ||  x ) )
9594ex 114 . . . . . . . . . . 11  |-  ( x  e.  ZZ  ->  (
( P  e.  Prime  /\  k  e.  ZZ )  ->  ( ( x 
||  ( k  x.  P )  /\  -.  x  ||  k )  ->  P  ||  x ) ) )
9666, 95vtoclga 2796 . . . . . . . . . 10  |-  ( D  e.  ZZ  ->  (
( P  e.  Prime  /\  k  e.  ZZ )  ->  ( ( D 
||  ( k  x.  P )  /\  -.  D  ||  k )  ->  P  ||  D ) ) )
9796impl 378 . . . . . . . . 9  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( ( D 
||  ( k  x.  P )  /\  -.  D  ||  k )  ->  P  ||  D ) )
9877zcnd 9328 . . . . . . . . . . . . . 14  |-  ( P  e.  Prime  ->  P  e.  CC )
9998exp1d 10597 . . . . . . . . . . . . 13  |-  ( P  e.  Prime  ->  ( P ^ 1 )  =  P )
10099ad2antlr 486 . . . . . . . . . . . 12  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( P ^
1 )  =  P )
101100oveq2d 5867 . . . . . . . . . . 11  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( k  x.  ( P ^ 1 ) )  =  ( k  x.  P ) )
102101breq2d 3999 . . . . . . . . . 10  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( D  ||  ( k  x.  ( P ^ 1 ) )  <-> 
D  ||  ( k  x.  P ) ) )
103 1m1e0 8940 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
104103oveq2i 5862 . . . . . . . . . . . . . . 15  |-  ( P ^ ( 1  -  1 ) )  =  ( P ^ 0 )
10577ad2antlr 486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  P  e.  ZZ )
106105zcnd 9328 . . . . . . . . . . . . . . . 16  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  P  e.  CC )
107106exp0d 10596 . . . . . . . . . . . . . . 15  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( P ^
0 )  =  1 )
108104, 107eqtrid 2215 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( P ^
( 1  -  1 ) )  =  1 )
109108oveq2d 5867 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( k  x.  ( P ^ (
1  -  1 ) ) )  =  ( k  x.  1 ) )
11075adantl 275 . . . . . . . . . . . . . 14  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  k  e.  CC )
111110mulid1d 7930 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( k  x.  1 )  =  k )
112109, 111eqtrd 2203 . . . . . . . . . . . 12  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( k  x.  ( P ^ (
1  -  1 ) ) )  =  k )
113112breq2d 3999 . . . . . . . . . . 11  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( D  ||  ( k  x.  ( P ^ ( 1  -  1 ) ) )  <-> 
D  ||  k )
)
114113notbid 662 . . . . . . . . . 10  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( -.  D  ||  ( k  x.  ( P ^ ( 1  -  1 ) ) )  <->  -.  D  ||  k ) )
115102, 114anbi12d 470 . . . . . . . . 9  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( ( D 
||  ( k  x.  ( P ^ 1 ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
1  -  1 ) ) ) )  <->  ( D  ||  ( k  x.  P
)  /\  -.  D  ||  k ) ) )
116106exp1d 10597 . . . . . . . . . 10  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( P ^
1 )  =  P )
117116breq1d 3997 . . . . . . . . 9  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( ( P ^ 1 )  ||  D 
<->  P  ||  D ) )
11897, 115, 1173imtr4d 202 . . . . . . . 8  |-  ( ( ( D  e.  ZZ  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( ( D 
||  ( k  x.  ( P ^ 1 ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
1  -  1 ) ) ) )  -> 
( P ^ 1 )  ||  D ) )
119118ralrimiva 2543 . . . . . . 7  |-  ( ( D  e.  ZZ  /\  P  e.  Prime )  ->  A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ 1 ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( 1  -  1 ) ) ) )  ->  ( P ^ 1 )  ||  D ) )
120 oveq1 5858 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  (
k  x.  ( P ^ n ) )  =  ( x  x.  ( P ^ n
) ) )
121120breq2d 3999 . . . . . . . . . . . . 13  |-  ( k  =  x  ->  ( D  ||  ( k  x.  ( P ^ n
) )  <->  D  ||  (
x  x.  ( P ^ n ) ) ) )
122 oveq1 5858 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
k  x.  ( P ^ ( n  - 
1 ) ) )  =  ( x  x.  ( P ^ (
n  -  1 ) ) ) )
123122breq2d 3999 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  ( D  ||  ( k  x.  ( P ^ (
n  -  1 ) ) )  <->  D  ||  (
x  x.  ( P ^ ( n  - 
1 ) ) ) ) )
124123notbid 662 . . . . . . . . . . . . 13  |-  ( k  =  x  ->  ( -.  D  ||  ( k  x.  ( P ^
( n  -  1 ) ) )  <->  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) ) )
125121, 124anbi12d 470 . . . . . . . . . . . 12  |-  ( k  =  x  ->  (
( D  ||  (
k  x.  ( P ^ n ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( n  - 
1 ) ) ) )  <->  ( D  ||  ( x  x.  ( P ^ n ) )  /\  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) ) ) )
126125imbi1d 230 . . . . . . . . . . 11  |-  ( k  =  x  ->  (
( ( D  ||  ( k  x.  ( P ^ n ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  <->  ( ( D  ||  ( x  x.  ( P ^ n
) )  /\  -.  D  ||  ( x  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )
) )
127126cbvralvw 2700 . . . . . . . . . 10  |-  ( A. k  e.  ZZ  (
( D  ||  (
k  x.  ( P ^ n ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  <->  A. x  e.  ZZ  ( ( D 
||  ( x  x.  ( P ^ n
) )  /\  -.  D  ||  ( x  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )
)
128 simprr 527 . . . . . . . . . . . . . . 15  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  k  e.  ZZ )
12977ad2antrl 487 . . . . . . . . . . . . . . 15  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  P  e.  ZZ )
130128, 129zmulcld 9333 . . . . . . . . . . . . . 14  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
k  x.  P )  e.  ZZ )
131 oveq1 5858 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( k  x.  P )  ->  (
x  x.  ( P ^ n ) )  =  ( ( k  x.  P )  x.  ( P ^ n
) ) )
132131breq2d 3999 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( k  x.  P )  ->  ( D  ||  ( x  x.  ( P ^ n
) )  <->  D  ||  (
( k  x.  P
)  x.  ( P ^ n ) ) ) )
133 oveq1 5858 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( k  x.  P )  ->  (
x  x.  ( P ^ ( n  - 
1 ) ) )  =  ( ( k  x.  P )  x.  ( P ^ (
n  -  1 ) ) ) )
134133breq2d 3999 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( k  x.  P )  ->  ( D  ||  ( x  x.  ( P ^ (
n  -  1 ) ) )  <->  D  ||  (
( k  x.  P
)  x.  ( P ^ ( n  - 
1 ) ) ) ) )
135134notbid 662 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( k  x.  P )  ->  ( -.  D  ||  ( x  x.  ( P ^
( n  -  1 ) ) )  <->  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ ( n  - 
1 ) ) ) ) )
136132, 135anbi12d 470 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( k  x.  P )  ->  (
( D  ||  (
x  x.  ( P ^ n ) )  /\  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) )  <->  ( D  ||  ( ( k  x.  P )  x.  ( P ^ n ) )  /\  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ ( n  - 
1 ) ) ) ) ) )
137136imbi1d 230 . . . . . . . . . . . . . . 15  |-  ( x  =  ( k  x.  P )  ->  (
( ( D  ||  ( x  x.  ( P ^ n ) )  /\  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  <->  ( ( D  ||  ( ( k  x.  P )  x.  ( P ^ n
) )  /\  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )
) )
138137rspcv 2830 . . . . . . . . . . . . . 14  |-  ( ( k  x.  P )  e.  ZZ  ->  ( A. x  e.  ZZ  ( ( D  ||  ( x  x.  ( P ^ n ) )  /\  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  ->  (
( D  ||  (
( k  x.  P
)  x.  ( P ^ n ) )  /\  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D ) ) )
139130, 138syl 14 . . . . . . . . . . . . 13  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( A. x  e.  ZZ  ( ( D  ||  ( x  x.  ( P ^ n ) )  /\  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  ->  (
( D  ||  (
( k  x.  P
)  x.  ( P ^ n ) )  /\  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D ) ) )
140 nnnn0 9135 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  NN0 )
141140ad2antrr 485 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  n  e.  NN0 )
142 zexpcl 10484 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  ZZ  /\  n  e.  NN0 )  -> 
( P ^ n
)  e.  ZZ )
143129, 141, 142syl2anc 409 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ n )  e.  ZZ )
144 simplr 525 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  D  e.  ZZ )
145 divides 11744 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P ^ n
)  e.  ZZ  /\  D  e.  ZZ )  ->  ( ( P ^
n )  ||  D  <->  E. x  e.  ZZ  (
x  x.  ( P ^ n ) )  =  D ) )
146143, 144, 145syl2anc 409 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( P ^ n
)  ||  D  <->  E. x  e.  ZZ  ( x  x.  ( P ^ n
) )  =  D ) )
14794adantll 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( x  ||  (
k  x.  P )  /\  -.  x  ||  k )  ->  P  ||  x ) )
14868ad2antrl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  P  e.  NN )
149148nncnd 8885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  P  e.  CC )
150140ad2antrr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  n  e.  NN0 )
151149, 150expp1d 10603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ ( n  + 
1 ) )  =  ( ( P ^
n )  x.  P
) )
152148, 150nnexpcld 10624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ n )  e.  NN )
153152nncnd 8885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ n )  e.  CC )
154153, 149mulcomd 7934 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( P ^ n
)  x.  P )  =  ( P  x.  ( P ^ n ) ) )
155151, 154eqtrd 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ ( n  + 
1 ) )  =  ( P  x.  ( P ^ n ) ) )
156155oveq2d 5867 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
k  x.  ( P ^ ( n  + 
1 ) ) )  =  ( k  x.  ( P  x.  ( P ^ n ) ) ) )
15775ad2antll 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  k  e.  CC )
158157, 149, 153mulassd 7936 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( k  x.  P
)  x.  ( P ^ n ) )  =  ( k  x.  ( P  x.  ( P ^ n ) ) ) )
159156, 158eqtr4d 2206 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
k  x.  ( P ^ ( n  + 
1 ) ) )  =  ( ( k  x.  P )  x.  ( P ^ n
) ) )
160159breq2d 3999 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( x  x.  ( P ^ n ) ) 
||  ( k  x.  ( P ^ (
n  +  1 ) ) )  <->  ( x  x.  ( P ^ n
) )  ||  (
( k  x.  P
)  x.  ( P ^ n ) ) ) )
161 simplr 525 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  x  e.  ZZ )
162 simprr 527 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  k  e.  ZZ )
163148nnzd 9326 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  P  e.  ZZ )
164162, 163zmulcld 9333 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
k  x.  P )  e.  ZZ )
165152nnzd 9326 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ n )  e.  ZZ )
166152nnne0d 8916 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ n )  =/=  0 )
167 dvdsmulcr 11776 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ZZ  /\  ( k  x.  P
)  e.  ZZ  /\  ( ( P ^
n )  e.  ZZ  /\  ( P ^ n
)  =/=  0 ) )  ->  ( (
x  x.  ( P ^ n ) ) 
||  ( ( k  x.  P )  x.  ( P ^ n
) )  <->  x  ||  (
k  x.  P ) ) )
168161, 164, 165, 166, 167syl112anc 1237 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( x  x.  ( P ^ n ) ) 
||  ( ( k  x.  P )  x.  ( P ^ n
) )  <->  x  ||  (
k  x.  P ) ) )
169160, 168bitrd 187 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( x  x.  ( P ^ n ) ) 
||  ( k  x.  ( P ^ (
n  +  1 ) ) )  <->  x  ||  (
k  x.  P ) ) )
170 dvdsmulcr 11776 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ZZ  /\  k  e.  ZZ  /\  (
( P ^ n
)  e.  ZZ  /\  ( P ^ n )  =/=  0 ) )  ->  ( ( x  x.  ( P ^
n ) )  ||  ( k  x.  ( P ^ n ) )  <-> 
x  ||  k )
)
171161, 162, 165, 166, 170syl112anc 1237 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( x  x.  ( P ^ n ) ) 
||  ( k  x.  ( P ^ n
) )  <->  x  ||  k
) )
172171notbid 662 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( -.  ( x  x.  ( P ^ n ) ) 
||  ( k  x.  ( P ^ n
) )  <->  -.  x  ||  k ) )
173169, 172anbi12d 470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( ( x  x.  ( P ^ n
) )  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  ( x  x.  ( P ^
n ) )  ||  ( k  x.  ( P ^ n ) ) )  <->  ( x  ||  ( k  x.  P
)  /\  -.  x  ||  k ) ) )
174155breq1d 3997 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( P ^ (
n  +  1 ) )  ||  ( x  x.  ( P ^
n ) )  <->  ( P  x.  ( P ^ n
) )  ||  (
x  x.  ( P ^ n ) ) ) )
175 dvdsmulcr 11776 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( P  e.  ZZ  /\  x  e.  ZZ  /\  (
( P ^ n
)  e.  ZZ  /\  ( P ^ n )  =/=  0 ) )  ->  ( ( P  x.  ( P ^
n ) )  ||  ( x  x.  ( P ^ n ) )  <-> 
P  ||  x )
)
176163, 161, 165, 166, 175syl112anc 1237 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( P  x.  ( P ^ n ) ) 
||  ( x  x.  ( P ^ n
) )  <->  P  ||  x
) )
177174, 176bitrd 187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( P ^ (
n  +  1 ) )  ||  ( x  x.  ( P ^
n ) )  <->  P  ||  x
) )
178147, 173, 1773imtr4d 202 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( n  e.  NN  /\  x  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( ( x  x.  ( P ^ n
) )  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  ( x  x.  ( P ^
n ) )  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  ( x  x.  ( P ^ n ) ) ) )
179178an32s 563 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  NN  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  e.  ZZ )  ->  (
( ( x  x.  ( P ^ n
) )  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  ( x  x.  ( P ^
n ) )  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  ( x  x.  ( P ^ n ) ) ) )
180 breq1 3990 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  x.  ( P ^ n ) )  =  D  ->  (
( x  x.  ( P ^ n ) ) 
||  ( k  x.  ( P ^ (
n  +  1 ) ) )  <->  D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) ) ) )
181 breq1 3990 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  x.  ( P ^ n ) )  =  D  ->  (
( x  x.  ( P ^ n ) ) 
||  ( k  x.  ( P ^ n
) )  <->  D  ||  (
k  x.  ( P ^ n ) ) ) )
182181notbid 662 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  x.  ( P ^ n ) )  =  D  ->  ( -.  ( x  x.  ( P ^ n ) ) 
||  ( k  x.  ( P ^ n
) )  <->  -.  D  ||  ( k  x.  ( P ^ n ) ) ) )
183180, 182anbi12d 470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  x.  ( P ^ n ) )  =  D  ->  (
( ( x  x.  ( P ^ n
) )  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  ( x  x.  ( P ^
n ) )  ||  ( k  x.  ( P ^ n ) ) )  <->  ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) ) ) )
184 breq2 3991 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  x.  ( P ^ n ) )  =  D  ->  (
( P ^ (
n  +  1 ) )  ||  ( x  x.  ( P ^
n ) )  <->  ( P ^ ( n  + 
1 ) )  ||  D ) )
185183, 184imbi12d 233 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  x.  ( P ^ n ) )  =  D  ->  (
( ( ( x  x.  ( P ^
n ) )  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  ( x  x.  ( P ^
n ) )  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  ( x  x.  ( P ^ n ) ) )  <->  ( ( D 
||  ( k  x.  ( P ^ (
n  +  1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n
) ) )  -> 
( P ^ (
n  +  1 ) )  ||  D ) ) )
186179, 185syl5ibcom 154 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  /\  x  e.  ZZ )  ->  (
( x  x.  ( P ^ n ) )  =  D  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
187186rexlimdva 2587 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  /\  ( P  e.  Prime  /\  k  e.  ZZ ) )  ->  ( E. x  e.  ZZ  (
x  x.  ( P ^ n ) )  =  D  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
188187adantlr 474 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( E. x  e.  ZZ  ( x  x.  ( P ^ n ) )  =  D  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
189146, 188sylbid 149 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( P ^ n
)  ||  D  ->  ( ( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
190189com23 78 . . . . . . . . . . . . . . 15  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) )  ->  ( ( P ^ n )  ||  D  ->  ( P ^
( n  +  1 ) )  ||  D
) ) )
191190a2d 26 . . . . . . . . . . . . . 14  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ n )  ||  D )  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
19275ad2antll 488 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  k  e.  CC )
193129zcnd 9328 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  P  e.  CC )
194143zcnd 9328 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ n )  e.  CC )
195192, 193, 194mulassd 7936 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( k  x.  P
)  x.  ( P ^ n ) )  =  ( k  x.  ( P  x.  ( P ^ n ) ) ) )
196193, 194mulcomd 7934 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P  x.  ( P ^ n ) )  =  ( ( P ^ n )  x.  P ) )
197193, 141expp1d 10603 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ ( n  + 
1 ) )  =  ( ( P ^
n )  x.  P
) )
198196, 197eqtr4d 2206 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P  x.  ( P ^ n ) )  =  ( P ^
( n  +  1 ) ) )
199198oveq2d 5867 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
k  x.  ( P  x.  ( P ^
n ) ) )  =  ( k  x.  ( P ^ (
n  +  1 ) ) ) )
200195, 199eqtrd 2203 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( k  x.  P
)  x.  ( P ^ n ) )  =  ( k  x.  ( P ^ (
n  +  1 ) ) ) )
201200breq2d 3999 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( D  ||  ( ( k  x.  P )  x.  ( P ^ n
) )  <->  D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) ) ) )
202 nnm1nn0 9169 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  (
n  -  1 )  e.  NN0 )
203202ad2antrr 485 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
n  -  1 )  e.  NN0 )
204 zexpcl 10484 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e.  ZZ  /\  ( n  -  1
)  e.  NN0 )  ->  ( P ^ (
n  -  1 ) )  e.  ZZ )
205129, 203, 204syl2anc 409 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ ( n  - 
1 ) )  e.  ZZ )
206205zcnd 9328 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ ( n  - 
1 ) )  e.  CC )
207192, 193, 206mulassd 7936 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( k  x.  P
)  x.  ( P ^ ( n  - 
1 ) ) )  =  ( k  x.  ( P  x.  ( P ^ ( n  - 
1 ) ) ) ) )
208193, 206mulcomd 7934 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P  x.  ( P ^ ( n  - 
1 ) ) )  =  ( ( P ^ ( n  - 
1 ) )  x.  P ) )
209 simpll 524 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  n  e.  NN )
210 expm1t 10497 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e.  CC  /\  n  e.  NN )  ->  ( P ^ n
)  =  ( ( P ^ ( n  -  1 ) )  x.  P ) )
211193, 209, 210syl2anc 409 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ n )  =  ( ( P ^
( n  -  1 ) )  x.  P
) )
212208, 211eqtr4d 2206 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P  x.  ( P ^ ( n  - 
1 ) ) )  =  ( P ^
n ) )
213212oveq2d 5867 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
k  x.  ( P  x.  ( P ^
( n  -  1 ) ) ) )  =  ( k  x.  ( P ^ n
) ) )
214207, 213eqtrd 2203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( k  x.  P
)  x.  ( P ^ ( n  - 
1 ) ) )  =  ( k  x.  ( P ^ n
) ) )
215214breq2d 3999 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( D  ||  ( ( k  x.  P )  x.  ( P ^ (
n  -  1 ) ) )  <->  D  ||  (
k  x.  ( P ^ n ) ) ) )
216215notbid 662 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( -.  D  ||  ( ( k  x.  P )  x.  ( P ^
( n  -  1 ) ) )  <->  -.  D  ||  ( k  x.  ( P ^ n ) ) ) )
217201, 216anbi12d 470 . . . . . . . . . . . . . . 15  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( D  ||  (
( k  x.  P
)  x.  ( P ^ n ) )  /\  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ ( n  - 
1 ) ) ) )  <->  ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) ) ) )
218217imbi1d 230 . . . . . . . . . . . . . 14  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( ( D  ||  ( ( k  x.  P )  x.  ( P ^ n ) )  /\  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  <->  ( ( D  ||  ( k  x.  ( P ^ (
n  +  1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n
) ) )  -> 
( P ^ n
)  ||  D )
) )
219 nncn 8879 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  n  e.  CC )
220219ad2antrr 485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  n  e.  CC )
221 ax-1cn 7860 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
222 pncan 8118 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  CC  /\  1  e.  CC )  ->  ( ( n  + 
1 )  -  1 )  =  n )
223220, 221, 222sylancl 411 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( n  +  1 )  -  1 )  =  n )
224223oveq2d 5867 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( P ^ ( ( n  +  1 )  - 
1 ) )  =  ( P ^ n
) )
225224oveq2d 5867 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) )  =  ( k  x.  ( P ^ n
) ) )
226225breq2d 3999 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( D  ||  ( k  x.  ( P ^ (
( n  +  1 )  -  1 ) ) )  <->  D  ||  (
k  x.  ( P ^ n ) ) ) )
227226notbid 662 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( -.  D  ||  ( k  x.  ( P ^
( ( n  + 
1 )  -  1 ) ) )  <->  -.  D  ||  ( k  x.  ( P ^ n ) ) ) )
228227anbi2d 461 . . . . . . . . . . . . . . 15  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  <->  ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n ) ) ) ) )
229228imbi1d 230 . . . . . . . . . . . . . 14  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D )  <->  ( ( D  ||  ( k  x.  ( P ^ (
n  +  1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ n
) ) )  -> 
( P ^ (
n  +  1 ) )  ||  D ) ) )
230191, 218, 2293imtr4d 202 . . . . . . . . . . . . 13  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  (
( ( D  ||  ( ( k  x.  P )  x.  ( P ^ n ) )  /\  -.  D  ||  ( ( k  x.  P )  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
231139, 230syld 45 . . . . . . . . . . . 12  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  k  e.  ZZ ) )  ->  ( A. x  e.  ZZ  ( ( D  ||  ( x  x.  ( P ^ n ) )  /\  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
232231anassrs 398 . . . . . . . . . . 11  |-  ( ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  P  e.  Prime )  /\  k  e.  ZZ )  ->  ( A. x  e.  ZZ  ( ( D  ||  ( x  x.  ( P ^ n ) )  /\  -.  D  ||  ( x  x.  ( P ^ ( n  - 
1 ) ) ) )  ->  ( P ^ n )  ||  D )  ->  (
( D  ||  (
k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
233232ralrimdva 2550 . . . . . . . . . 10  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  P  e.  Prime )  ->  ( A. x  e.  ZZ  ( ( D 
||  ( x  x.  ( P ^ n
) )  /\  -.  D  ||  ( x  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )  ->  A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
234127, 233syl5bi 151 . . . . . . . . 9  |-  ( ( ( n  e.  NN  /\  D  e.  ZZ )  /\  P  e.  Prime )  ->  ( A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ n
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )  ->  A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) )
235234expl 376 . . . . . . . 8  |-  ( n  e.  NN  ->  (
( D  e.  ZZ  /\  P  e.  Prime )  ->  ( A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ n
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )  ->  A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ ( n  + 
1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( ( n  +  1 )  - 
1 ) ) ) )  ->  ( P ^ ( n  + 
1 ) )  ||  D ) ) ) )
236235a2d 26 . . . . . . 7  |-  ( n  e.  NN  ->  (
( ( D  e.  ZZ  /\  P  e. 
Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ n
) )  /\  -.  D  ||  ( k  x.  ( P ^ (
n  -  1 ) ) ) )  -> 
( P ^ n
)  ||  D )
)  ->  ( ( D  e.  ZZ  /\  P  e.  Prime )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ (
n  +  1 ) ) )  /\  -.  D  ||  ( k  x.  ( P ^ (
( n  +  1 )  -  1 ) ) ) )  -> 
( P ^ (
n  +  1 ) )  ||  D ) ) ) )
23720, 33, 46, 59, 119, 236nnind 8887 . . . . . 6  |-  ( N  e.  NN  ->  (
( D  e.  ZZ  /\  P  e.  Prime )  ->  A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ N ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  - 
1 ) ) ) )  ->  ( P ^ N )  ||  D
) ) )
238237com12 30 . . . . 5  |-  ( ( D  e.  ZZ  /\  P  e.  Prime )  -> 
( N  e.  NN  ->  A. k  e.  ZZ  ( ( D  ||  ( k  x.  ( P ^ N ) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  - 
1 ) ) ) )  ->  ( P ^ N )  ||  D
) ) )
239238impr 377 . . . 4  |-  ( ( D  e.  ZZ  /\  ( P  e.  Prime  /\  N  e.  NN ) )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ N
) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  -  1 ) ) ) )  -> 
( P ^ N
)  ||  D )
)
240239adantll 473 . . 3  |-  ( ( ( K  e.  ZZ  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  N  e.  NN ) )  ->  A. k  e.  ZZ  ( ( D 
||  ( k  x.  ( P ^ N
) )  /\  -.  D  ||  ( k  x.  ( P ^ ( N  -  1 ) ) ) )  -> 
( P ^ N
)  ||  D )
)
241 simpll 524 . . 3  |-  ( ( ( K  e.  ZZ  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  N  e.  NN ) )  ->  K  e.  ZZ )
2427, 240, 241rspcdva 2839 . 2  |-  ( ( ( K  e.  ZZ  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  N  e.  NN ) )  ->  (
( D  ||  ( K  x.  ( P ^ N ) )  /\  -.  D  ||  ( K  x.  ( P ^
( N  -  1 ) ) ) )  ->  ( P ^ N )  ||  D
) )
2432423impia 1195 1  |-  ( ( ( K  e.  ZZ  /\  D  e.  ZZ )  /\  ( P  e. 
Prime  /\  N  e.  NN )  /\  ( D  ||  ( K  x.  ( P ^ N ) )  /\  -.  D  ||  ( K  x.  ( P ^ ( N  - 
1 ) ) ) ) )  ->  ( P ^ N )  ||  D )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104  DECID wdc 829    /\ w3a 973    = wceq 1348    e. wcel 2141    =/= wne 2340   A.wral 2448   E.wrex 2449   class class class wbr 3987  (class class class)co 5851   CCcc 7765   0cc0 7767   1c1 7768    + caddc 7770    x. cmul 7772    - cmin 8083   NNcn 8871   NN0cn0 9128   ZZcz 9205   ^cexp 10468    || cdvds 11742    gcd cgcd 11890   Primecprime 12054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7858  ax-resscn 7859  ax-1cn 7860  ax-1re 7861  ax-icn 7862  ax-addcl 7863  ax-addrcl 7864  ax-mulcl 7865  ax-mulrcl 7866  ax-addcom 7867  ax-mulcom 7868  ax-addass 7869  ax-mulass 7870  ax-distr 7871  ax-i2m1 7872  ax-0lt1 7873  ax-1rid 7874  ax-0id 7875  ax-rnegex 7876  ax-precex 7877  ax-cnre 7878  ax-pre-ltirr 7879  ax-pre-ltwlin 7880  ax-pre-lttrn 7881  ax-pre-apti 7882  ax-pre-ltadd 7883  ax-pre-mulgt0 7884  ax-pre-mulext 7885  ax-arch 7886  ax-caucvg 7887
This theorem depends on definitions:  df-bi 116  df-stab 826  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-recs 6282  df-frec 6368  df-1o 6393  df-2o 6394  df-er 6511  df-en 6717  df-sup 6959  df-pnf 7949  df-mnf 7950  df-xr 7951  df-ltxr 7952  df-le 7953  df-sub 8085  df-neg 8086  df-reap 8487  df-ap 8494  df-div 8583  df-inn 8872  df-2 8930  df-3 8931  df-4 8932  df-n0 9129  df-z 9206  df-uz 9481  df-q 9572  df-rp 9604  df-fz 9959  df-fzo 10092  df-fl 10219  df-mod 10272  df-seqfrec 10395  df-exp 10469  df-cj 10799  df-re 10800  df-im 10801  df-rsqrt 10955  df-abs 10956  df-dvds 11743  df-gcd 11891  df-prm 12055
This theorem is referenced by:  pockthlem  12301
  Copyright terms: Public domain W3C validator