MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcmpt Structured version   Unicode version

Theorem pcmpt 13299
Description: Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
Hypotheses
Ref Expression
pcmpt.1  |-  F  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( n ^ A
) ,  1 ) )
pcmpt.2  |-  ( ph  ->  A. n  e.  Prime  A  e.  NN0 )
pcmpt.3  |-  ( ph  ->  N  e.  NN )
pcmpt.4  |-  ( ph  ->  P  e.  Prime )
pcmpt.5  |-  ( n  =  P  ->  A  =  B )
Assertion
Ref Expression
pcmpt  |-  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  N
) )  =  if ( P  <_  N ,  B ,  0 ) )
Distinct variable groups:    B, n    P, n
Allowed substitution hints:    ph( n)    A( n)    F( n)    N( n)

Proof of Theorem pcmpt
Dummy variables  k  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcmpt.3 . 2  |-  ( ph  ->  N  e.  NN )
2 fveq2 5763 . . . . . 6  |-  ( p  =  1  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  1
) )
32oveq2d 6133 . . . . 5  |-  ( p  =  1  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  1 )
) )
4 breq2 4247 . . . . . 6  |-  ( p  =  1  ->  ( P  <_  p  <->  P  <_  1 ) )
54ifbid 3785 . . . . 5  |-  ( p  =  1  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  1 ,  B ,  0 ) )
63, 5eqeq12d 2457 . . . 4  |-  ( p  =  1  ->  (
( P  pCnt  (  seq  1 (  x.  ,  F ) `  p
) )  =  if ( P  <_  p ,  B ,  0 )  <-> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  1
) )  =  if ( P  <_  1 ,  B ,  0 ) ) )
76imbi2d 309 . . 3  |-  ( p  =  1  ->  (
( ph  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  if ( P  <_  p ,  B ,  0 ) )  <->  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  1
) )  =  if ( P  <_  1 ,  B ,  0 ) ) ) )
8 fveq2 5763 . . . . . 6  |-  ( p  =  k  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  k
) )
98oveq2d 6133 . . . . 5  |-  ( p  =  k  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  k )
) )
10 breq2 4247 . . . . . 6  |-  ( p  =  k  ->  ( P  <_  p  <->  P  <_  k ) )
1110ifbid 3785 . . . . 5  |-  ( p  =  k  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  k ,  B ,  0 ) )
129, 11eqeq12d 2457 . . . 4  |-  ( p  =  k  ->  (
( P  pCnt  (  seq  1 (  x.  ,  F ) `  p
) )  =  if ( P  <_  p ,  B ,  0 )  <-> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  =  if ( P  <_  k ,  B ,  0 ) ) )
1312imbi2d 309 . . 3  |-  ( p  =  k  ->  (
( ph  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  if ( P  <_  p ,  B ,  0 ) )  <->  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  =  if ( P  <_  k ,  B ,  0 ) ) ) )
14 fveq2 5763 . . . . . 6  |-  ( p  =  ( k  +  1 )  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )
1514oveq2d 6133 . . . . 5  |-  ( p  =  ( k  +  1 )  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  ( k  +  1 ) ) ) )
16 breq2 4247 . . . . . 6  |-  ( p  =  ( k  +  1 )  ->  ( P  <_  p  <->  P  <_  ( k  +  1 ) ) )
1716ifbid 3785 . . . . 5  |-  ( p  =  ( k  +  1 )  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  ( k  +  1 ) ,  B ,  0 ) )
1815, 17eqeq12d 2457 . . . 4  |-  ( p  =  ( k  +  1 )  ->  (
( P  pCnt  (  seq  1 (  x.  ,  F ) `  p
) )  =  if ( P  <_  p ,  B ,  0 )  <-> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )  =  if ( P  <_  (
k  +  1 ) ,  B ,  0 ) ) )
1918imbi2d 309 . . 3  |-  ( p  =  ( k  +  1 )  ->  (
( ph  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  if ( P  <_  p ,  B ,  0 ) )  <->  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )  =  if ( P  <_  (
k  +  1 ) ,  B ,  0 ) ) ) )
20 fveq2 5763 . . . . . 6  |-  ( p  =  N  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  N
) )
2120oveq2d 6133 . . . . 5  |-  ( p  =  N  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  N )
) )
22 breq2 4247 . . . . . 6  |-  ( p  =  N  ->  ( P  <_  p  <->  P  <_  N ) )
2322ifbid 3785 . . . . 5  |-  ( p  =  N  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  N ,  B ,  0 ) )
2421, 23eqeq12d 2457 . . . 4  |-  ( p  =  N  ->  (
( P  pCnt  (  seq  1 (  x.  ,  F ) `  p
) )  =  if ( P  <_  p ,  B ,  0 )  <-> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  N
) )  =  if ( P  <_  N ,  B ,  0 ) ) )
2524imbi2d 309 . . 3  |-  ( p  =  N  ->  (
( ph  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  if ( P  <_  p ,  B ,  0 ) )  <->  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  N
) )  =  if ( P  <_  N ,  B ,  0 ) ) ) )
26 pcmpt.4 . . . 4  |-  ( ph  ->  P  e.  Prime )
27 1z 10349 . . . . . . . . 9  |-  1  e.  ZZ
28 seq1 11374 . . . . . . . . 9  |-  ( 1  e.  ZZ  ->  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 ) )
2927, 28ax-mp 5 . . . . . . . 8  |-  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 )
30 1nn 10049 . . . . . . . . 9  |-  1  e.  NN
31 1nprm 13122 . . . . . . . . . . . 12  |-  -.  1  e.  Prime
32 eleq1 2503 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
n  e.  Prime  <->  1  e.  Prime ) )
3331, 32mtbiri 296 . . . . . . . . . . 11  |-  ( n  =  1  ->  -.  n  e.  Prime )
34 iffalse 3774 . . . . . . . . . . 11  |-  ( -.  n  e.  Prime  ->  if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  =  1 )
3533, 34syl 16 . . . . . . . . . 10  |-  ( n  =  1  ->  if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  =  1 )
36 pcmpt.1 . . . . . . . . . 10  |-  F  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( n ^ A
) ,  1 ) )
37 1ex 9124 . . . . . . . . . 10  |-  1  e.  _V
3835, 36, 37fvmpt 5842 . . . . . . . . 9  |-  ( 1  e.  NN  ->  ( F `  1 )  =  1 )
3930, 38ax-mp 5 . . . . . . . 8  |-  ( F `
 1 )  =  1
4029, 39eqtri 2463 . . . . . . 7  |-  (  seq  1 (  x.  ,  F ) `  1
)  =  1
4140oveq2i 6128 . . . . . 6  |-  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  1 )
)  =  ( P 
pCnt  1 )
42 pc1 13267 . . . . . 6  |-  ( P  e.  Prime  ->  ( P 
pCnt  1 )  =  0 )
4341, 42syl5eq 2487 . . . . 5  |-  ( P  e.  Prime  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  1 )
)  =  0 )
44 prmuz2 13135 . . . . . . . 8  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
45 eluz2b2 10586 . . . . . . . . 9  |-  ( P  e.  ( ZZ>= `  2
)  <->  ( P  e.  NN  /\  1  < 
P ) )
4645simprbi 452 . . . . . . . 8  |-  ( P  e.  ( ZZ>= `  2
)  ->  1  <  P )
4744, 46syl 16 . . . . . . 7  |-  ( P  e.  Prime  ->  1  < 
P )
48 1re 9128 . . . . . . . 8  |-  1  e.  RR
49 eluzelre 10535 . . . . . . . . 9  |-  ( P  e.  ( ZZ>= `  2
)  ->  P  e.  RR )
5044, 49syl 16 . . . . . . . 8  |-  ( P  e.  Prime  ->  P  e.  RR )
51 ltnle 9193 . . . . . . . 8  |-  ( ( 1  e.  RR  /\  P  e.  RR )  ->  ( 1  <  P  <->  -.  P  <_  1 ) )
5248, 50, 51sylancr 646 . . . . . . 7  |-  ( P  e.  Prime  ->  ( 1  <  P  <->  -.  P  <_  1 ) )
5347, 52mpbid 203 . . . . . 6  |-  ( P  e.  Prime  ->  -.  P  <_  1 )
54 iffalse 3774 . . . . . 6  |-  ( -.  P  <_  1  ->  if ( P  <_  1 ,  B ,  0 )  =  0 )
5553, 54syl 16 . . . . 5  |-  ( P  e.  Prime  ->  if ( P  <_  1 ,  B ,  0 )  =  0 )
5643, 55eqtr4d 2478 . . . 4  |-  ( P  e.  Prime  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  1 )
)  =  if ( P  <_  1 ,  B ,  0 ) )
5726, 56syl 16 . . 3  |-  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  1
) )  =  if ( P  <_  1 ,  B ,  0 ) )
5826adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  P  e.  Prime )
59 pcmpt.2 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. n  e.  Prime  A  e.  NN0 )
6036, 59pcmptcl 13298 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F : NN --> NN  /\  seq  1 (  x.  ,  F ) : NN --> NN ) )
6160simpld 447 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : NN --> NN )
62 peano2nn 10050 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
63 ffvelrn 5904 . . . . . . . . . . . . . . 15  |-  ( ( F : NN --> NN  /\  ( k  +  1 )  e.  NN )  ->  ( F `  ( k  +  1 ) )  e.  NN )
6461, 62, 63syl2an 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 ( k  +  1 ) )  e.  NN )
6564adantrr 699 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( F `  (
k  +  1 ) )  e.  NN )
6658, 65pccld 13262 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  e.  NN0 )
6766nn0cnd 10314 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  e.  CC )
6867addid2d 9305 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( 0  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )  =  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )
6962ad2antrl 710 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( k  +  1 )  e.  NN )
70 ovex 6142 . . . . . . . . . . . . . 14  |-  ( k  +  1 )  e. 
_V
71 ovex 6142 . . . . . . . . . . . . . . 15  |-  ( n ^ A )  e. 
_V
7271, 37ifex 3826 . . . . . . . . . . . . . 14  |-  if ( n  e.  Prime ,  ( n ^ A ) ,  1 )  e. 
_V
7370, 72csbexOLD 4374 . . . . . . . . . . . . 13  |-  [_ (
k  +  1 )  /  n ]_ if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  e.  _V
7436fvmpts 5843 . . . . . . . . . . . . . 14  |-  ( ( ( k  +  1 )  e.  NN  /\  [_ ( k  +  1 )  /  n ]_ if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  e.  _V )  -> 
( F `  (
k  +  1 ) )  =  [_ (
k  +  1 )  /  n ]_ if ( n  e.  Prime ,  ( n ^ A
) ,  1 ) )
75 nfv 1631 . . . . . . . . . . . . . . . 16  |-  F/ n
( k  +  1 )  e.  Prime
76 nfcv 2579 . . . . . . . . . . . . . . . . 17  |-  F/_ n
( k  +  1 )
77 nfcv 2579 . . . . . . . . . . . . . . . . 17  |-  F/_ n ^
78 nfcsb1v 3285 . . . . . . . . . . . . . . . . 17  |-  F/_ n [_ ( k  +  1 )  /  n ]_ A
7976, 77, 78nfov 6140 . . . . . . . . . . . . . . . 16  |-  F/_ n
( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A )
80 nfcv 2579 . . . . . . . . . . . . . . . 16  |-  F/_ n
1
8175, 79, 80nfif 3791 . . . . . . . . . . . . . . 15  |-  F/_ n if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ,  1 )
82 eleq1 2503 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( k  +  1 )  ->  (
n  e.  Prime  <->  ( k  +  1 )  e. 
Prime ) )
83 id 21 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( k  +  1 )  ->  n  =  ( k  +  1 ) )
84 csbeq1a 3278 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( k  +  1 )  ->  A  =  [_ ( k  +  1 )  /  n ]_ A )
8583, 84oveq12d 6135 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( k  +  1 )  ->  (
n ^ A )  =  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) )
86 eqidd 2444 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( k  +  1 )  ->  1  =  1 )
8782, 85, 86ifbieq12d 3789 . . . . . . . . . . . . . . 15  |-  ( n  =  ( k  +  1 )  ->  if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  =  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ,  1 ) )
8870, 81, 87csbief 3294 . . . . . . . . . . . . . 14  |-  [_ (
k  +  1 )  /  n ]_ if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  =  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ,  1 )
8974, 88syl6eq 2491 . . . . . . . . . . . . 13  |-  ( ( ( k  +  1 )  e.  NN  /\  [_ ( k  +  1 )  /  n ]_ if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  e.  _V )  -> 
( F `  (
k  +  1 ) )  =  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ (
k  +  1 )  /  n ]_ A
) ,  1 ) )
9069, 73, 89sylancl 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( F `  (
k  +  1 ) )  =  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ (
k  +  1 )  /  n ]_ A
) ,  1 ) )
91 simprr 735 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( k  +  1 )  =  P )
9291, 58eqeltrd 2517 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( k  +  1 )  e.  Prime )
93 iftrue 3773 . . . . . . . . . . . . 13  |-  ( ( k  +  1 )  e.  Prime  ->  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ (
k  +  1 )  /  n ]_ A
) ,  1 )  =  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) )
9492, 93syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ,  1 )  =  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) )
9591csbeq1d 3276 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  [_ ( k  +  1 )  /  n ]_ A  =  [_ P  /  n ]_ A )
96 nfcvd 2580 . . . . . . . . . . . . . . . 16  |-  ( P  e.  Prime  ->  F/_ n B )
97 pcmpt.5 . . . . . . . . . . . . . . . 16  |-  ( n  =  P  ->  A  =  B )
9896, 97csbiegf 3293 . . . . . . . . . . . . . . 15  |-  ( P  e.  Prime  ->  [_ P  /  n ]_ A  =  B )
9958, 98syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  [_ P  /  n ]_ A  =  B
)
10095, 99eqtrd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  [_ ( k  +  1 )  /  n ]_ A  =  B )
10191, 100oveq12d 6135 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A )  =  ( P ^ B ) )
10290, 94, 1013eqtrd 2479 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( F `  (
k  +  1 ) )  =  ( P ^ B ) )
103102oveq2d 6133 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  =  ( P 
pCnt  ( P ^ B ) ) )
10497eleq1d 2509 . . . . . . . . . . . . . 14  |-  ( n  =  P  ->  ( A  e.  NN0  <->  B  e.  NN0 ) )
105104rspcv 3057 . . . . . . . . . . . . 13  |-  ( P  e.  Prime  ->  ( A. n  e.  Prime  A  e. 
NN0  ->  B  e.  NN0 ) )
10626, 59, 105sylc 59 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  NN0 )
107106adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  B  e.  NN0 )
108 pcidlem 13283 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  B  e.  NN0 )  ->  ( P  pCnt  ( P ^ B ) )  =  B )
10958, 107, 108syl2anc 644 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( P ^ B ) )  =  B )
11068, 103, 1093eqtrd 2479 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( 0  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )  =  B )
111 oveq1 6124 . . . . . . . . . 10  |-  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  =  0  ->  ( ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  k )
)  +  ( P 
pCnt  ( F `  ( k  +  1 ) ) ) )  =  ( 0  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) ) )
112111eqeq1d 2451 . . . . . . . . 9  |-  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  =  0  ->  ( ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )  =  B  <->  ( 0  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )  =  B ) )
113110, 112syl5ibrcom 215 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k ) )  =  0  ->  ( ( P  pCnt  (  seq  1
(  x.  ,  F
) `  k )
)  +  ( P 
pCnt  ( F `  ( k  +  1 ) ) ) )  =  B ) )
114 nnre 10045 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  RR )
115114ad2antrl 710 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
k  e.  RR )
116 ltp1 9886 . . . . . . . . . . . . 13  |-  ( k  e.  RR  ->  k  <  ( k  +  1 ) )
117 peano2re 9277 . . . . . . . . . . . . . 14  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
118 ltnle 9193 . . . . . . . . . . . . . 14  |-  ( ( k  e.  RR  /\  ( k  +  1 )  e.  RR )  ->  ( k  < 
( k  +  1 )  <->  -.  ( k  +  1 )  <_ 
k ) )
119117, 118mpdan 651 . . . . . . . . . . . . 13  |-  ( k  e.  RR  ->  (
k  <  ( k  +  1 )  <->  -.  (
k  +  1 )  <_  k ) )
120116, 119mpbid 203 . . . . . . . . . . . 12  |-  ( k  e.  RR  ->  -.  ( k  +  1 )  <_  k )
121115, 120syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  -.  ( k  +  1 )  <_  k )
12291breq1d 4253 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( k  +  1 )  <_  k  <->  P  <_  k ) )
123121, 122mtbid 293 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  -.  P  <_  k )
124 iffalse 3774 . . . . . . . . . 10  |-  ( -.  P  <_  k  ->  if ( P  <_  k ,  B ,  0 )  =  0 )
125123, 124syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  if ( P  <_  k ,  B ,  0 )  =  0 )
126125eqeq2d 2454 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k ) )  =  if ( P  <_ 
k ,  B , 
0 )  <->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `
 k ) )  =  0 ) )
127 simpr 449 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
128 nnuz 10559 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
129127, 128syl6eleq 2533 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  1 )
)
130 seqp1 11376 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  1
)  ->  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) )  =  ( (  seq  1 (  x.  ,  F ) `  k )  x.  ( F `  ( k  +  1 ) ) ) )
131129, 130syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) )  =  ( (  seq  1 (  x.  ,  F ) `  k )  x.  ( F `  ( k  +  1 ) ) ) )
132131oveq2d 6133 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  ( k  +  1 ) ) )  =  ( P 
pCnt  ( (  seq  1 (  x.  ,  F ) `  k
)  x.  ( F `
 ( k  +  1 ) ) ) ) )
13326adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  P  e. 
Prime )
13460simprd 451 . . . . . . . . . . . . . 14  |-  ( ph  ->  seq  1 (  x.  ,  F ) : NN --> NN )
135134ffvelrnda 5906 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  x.  ,  F ) `  k
)  e.  NN )
136 nnz 10341 . . . . . . . . . . . . . 14  |-  ( (  seq  1 (  x.  ,  F ) `  k )  e.  NN  ->  (  seq  1 (  x.  ,  F ) `
 k )  e.  ZZ )
137 nnne0 10070 . . . . . . . . . . . . . 14  |-  ( (  seq  1 (  x.  ,  F ) `  k )  e.  NN  ->  (  seq  1 (  x.  ,  F ) `
 k )  =/=  0 )
138136, 137jca 520 . . . . . . . . . . . . 13  |-  ( (  seq  1 (  x.  ,  F ) `  k )  e.  NN  ->  ( (  seq  1
(  x.  ,  F
) `  k )  e.  ZZ  /\  (  seq  1 (  x.  ,  F ) `  k
)  =/=  0 ) )
139135, 138syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( (  seq  1 (  x.  ,  F ) `  k )  e.  ZZ  /\  (  seq  1 (  x.  ,  F ) `
 k )  =/=  0 ) )
140 nnz 10341 . . . . . . . . . . . . . 14  |-  ( ( F `  ( k  +  1 ) )  e.  NN  ->  ( F `  ( k  +  1 ) )  e.  ZZ )
141 nnne0 10070 . . . . . . . . . . . . . 14  |-  ( ( F `  ( k  +  1 ) )  e.  NN  ->  ( F `  ( k  +  1 ) )  =/=  0 )
142140, 141jca 520 . . . . . . . . . . . . 13  |-  ( ( F `  ( k  +  1 ) )  e.  NN  ->  (
( F `  (
k  +  1 ) )  e.  ZZ  /\  ( F `  ( k  +  1 ) )  =/=  0 ) )
14364, 142syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( F `  ( k  +  1 ) )  e.  ZZ  /\  ( F `  ( k  +  1 ) )  =/=  0 ) )
144 pcmul 13263 . . . . . . . . . . . 12  |-  ( ( P  e.  Prime  /\  (
(  seq  1 (  x.  ,  F ) `
 k )  e.  ZZ  /\  (  seq  1 (  x.  ,  F ) `  k
)  =/=  0 )  /\  ( ( F `
 ( k  +  1 ) )  e.  ZZ  /\  ( F `
 ( k  +  1 ) )  =/=  0 ) )  -> 
( P  pCnt  (
(  seq  1 (  x.  ,  F ) `
 k )  x.  ( F `  (
k  +  1 ) ) ) )  =  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k ) )  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) ) )
145133, 139, 143, 144syl3anc 1185 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( P 
pCnt  ( (  seq  1 (  x.  ,  F ) `  k
)  x.  ( F `
 ( k  +  1 ) ) ) )  =  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) ) )
146132, 145eqtrd 2475 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  ( k  +  1 ) ) )  =  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) ) )
147146adantrr 699 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )  =  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) ) )
148 prmnn 13120 . . . . . . . . . . . . . . 15  |-  ( P  e.  Prime  ->  P  e.  NN )
14926, 148syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  NN )
150149nnred 10053 . . . . . . . . . . . . 13  |-  ( ph  ->  P  e.  RR )
151150adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  P  e.  RR )
152151leidd 9631 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  P  <_  P )
153152, 91breqtrrd 4269 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  P  <_  ( k  +  1 ) )
154 iftrue 3773 . . . . . . . . . 10  |-  ( P  <_  ( k  +  1 )  ->  if ( P  <_  ( k  +  1 ) ,  B ,  0 )  =  B )
155153, 154syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  if ( P  <_  (
k  +  1 ) ,  B ,  0 )  =  B )
156147, 155eqeq12d 2457 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  ( k  +  1 ) ) )  =  if ( P  <_ 
( k  +  1 ) ,  B , 
0 )  <->  ( ( P  pCnt  (  seq  1
(  x.  ,  F
) `  k )
)  +  ( P 
pCnt  ( F `  ( k  +  1 ) ) ) )  =  B ) )
157113, 126, 1563imtr4d 261 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k ) )  =  if ( P  <_ 
k ,  B , 
0 )  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  ( k  +  1 ) ) )  =  if ( P  <_  ( k  +  1 ) ,  B ,  0 ) ) )
158157expr 600 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  +  1 )  =  P  ->  (
( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  =  if ( P  <_  k ,  B ,  0 )  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  ( k  +  1 ) ) )  =  if ( P  <_ 
( k  +  1 ) ,  B , 
0 ) ) ) )
159146adantrr 699 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )  =  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) ) )
160 simplrr 739 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( k  +  1 )  =/= 
P )
161160necomd 2694 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  P  =/=  ( k  +  1 ) )
16226ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  P  e. 
Prime )
163 simpr 449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( k  +  1 )  e. 
Prime )
16459ad2antrr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  A. n  e.  Prime  A  e.  NN0 )
16578nfel1 2589 . . . . . . . . . . . . . . . . . . 19  |-  F/ n [_ ( k  +  1 )  /  n ]_ A  e.  NN0
16684eleq1d 2509 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( k  +  1 )  ->  ( A  e.  NN0  <->  [_ ( k  +  1 )  /  n ]_ A  e.  NN0 ) )
167165, 166rspc 3055 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  +  1 )  e.  Prime  ->  ( A. n  e.  Prime  A  e. 
NN0  ->  [_ ( k  +  1 )  /  n ]_ A  e.  NN0 ) )
168163, 164, 167sylc 59 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  [_ (
k  +  1 )  /  n ]_ A  e.  NN0 )
169 prmdvdsexpr 13154 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  Prime  /\  (
k  +  1 )  e.  Prime  /\  [_ (
k  +  1 )  /  n ]_ A  e.  NN0 )  ->  ( P  ||  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A )  ->  P  =  ( k  +  1 ) ) )
170162, 163, 168, 169syl3anc 1185 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( P 
||  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A )  ->  P  =  ( k  +  1 ) ) )
171170necon3ad 2644 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( P  =/=  ( k  +  1 )  ->  -.  P  ||  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ) )
172161, 171mpd 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  -.  P  ||  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) )
17362ad2antrl 710 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( k  +  1 )  e.  NN )
174173, 73, 89sylancl 645 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( F `  (
k  +  1 ) )  =  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ (
k  +  1 )  /  n ]_ A
) ,  1 ) )
175174, 93sylan9eq 2495 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( F `
 ( k  +  1 ) )  =  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) )
176175breq2d 4255 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( P 
||  ( F `  ( k  +  1 ) )  <->  P  ||  (
( k  +  1 ) ^ [_ (
k  +  1 )  /  n ]_ A
) ) )
177172, 176mtbird 294 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  -.  P  ||  ( F `  (
k  +  1 ) ) )
17861adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  F : NN --> NN )
179178, 173, 63syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( F `  (
k  +  1 ) )  e.  NN )
180179adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( F `
 ( k  +  1 ) )  e.  NN )
181 pceq0 13282 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  ( F `  ( k  +  1 ) )  e.  NN )  -> 
( ( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0  <->  -.  P  ||  ( F `  ( k  +  1 ) ) ) )
182162, 180, 181syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( ( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0  <->  -.  P  ||  ( F `  ( k  +  1 ) ) ) )
183177, 182mpbird 225 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( P 
pCnt  ( F `  ( k  +  1 ) ) )  =  0 )
184 iffalse 3774 . . . . . . . . . . . . . . 15  |-  ( -.  ( k  +  1 )  e.  Prime  ->  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ,  1 )  =  1 )
185174, 184sylan9eq 2495 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  -.  (
k  +  1 )  e.  Prime )  ->  ( F `  ( k  +  1 ) )  =  1 )
186185oveq2d 6133 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  -.  (
k  +  1 )  e.  Prime )  ->  ( P  pCnt  ( F `  ( k  +  1 ) ) )  =  ( P  pCnt  1
) )
18726, 42syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P  pCnt  1
)  =  0 )
188187ad2antrr 708 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  -.  (
k  +  1 )  e.  Prime )  ->  ( P  pCnt  1 )  =  0 )
189186, 188eqtrd 2475 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  -.  (
k  +  1 )  e.  Prime )  ->  ( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0 )
190183, 189pm2.61dan 768 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0 )
191190oveq2d 6133 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k ) )  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )  =  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  +  0 ) )
19226adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  P  e.  Prime )
193135adantrr 699 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
(  seq  1 (  x.  ,  F ) `
 k )  e.  NN )
194192, 193pccld 13262 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  e.  NN0 )
195194nn0cnd 10314 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  e.  CC )
196195addid1d 9304 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k ) )  +  0 )  =  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) ) )
197159, 191, 1963eqtrd 2479 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )  =  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) ) )
198149adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  P  e.  NN )
199198nnred 10053 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  P  e.  RR )
200173nnred 10053 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( k  +  1 )  e.  RR )
201199, 200ltlend 9256 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <  (
k  +  1 )  <-> 
( P  <_  (
k  +  1 )  /\  ( k  +  1 )  =/=  P
) ) )
202 simprl 734 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
k  e.  NN )
203 nnleltp1 10367 . . . . . . . . . . . 12  |-  ( ( P  e.  NN  /\  k  e.  NN )  ->  ( P  <_  k  <->  P  <  ( k  +  1 ) ) )
204198, 202, 203syl2anc 644 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <_  k  <->  P  <  ( k  +  1 ) ) )
205 simprr 735 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( k  +  1 )  =/=  P )
206205biantrud 495 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <_  (
k  +  1 )  <-> 
( P  <_  (
k  +  1 )  /\  ( k  +  1 )  =/=  P
) ) )
207201, 204, 2063bitr4rd 279 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <_  (
k  +  1 )  <-> 
P  <_  k )
)
208207ifbid 3785 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  if ( P  <_  (
k  +  1 ) ,  B ,  0 )  =  if ( P  <_  k ,  B ,  0 ) )
209197, 208eqeq12d 2457 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  ( k  +  1 ) ) )  =  if ( P  <_ 
( k  +  1 ) ,  B , 
0 )  <->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `
 k ) )  =  if ( P  <_  k ,  B ,  0 ) ) )
210209biimprd 216 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k ) )  =  if ( P  <_ 
k ,  B , 
0 )  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  ( k  +  1 ) ) )  =  if ( P  <_  ( k  +  1 ) ,  B ,  0 ) ) )
211210expr 600 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  +  1 )  =/=  P  ->  (
( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  =  if ( P  <_  k ,  B ,  0 )  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  ( k  +  1 ) ) )  =  if ( P  <_ 
( k  +  1 ) ,  B , 
0 ) ) ) )
212158, 211pm2.61dne 2688 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  =  if ( P  <_  k ,  B ,  0 )  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  ( k  +  1 ) ) )  =  if ( P  <_ 
( k  +  1 ) ,  B , 
0 ) ) )
213212expcom 426 . . . 4  |-  ( k  e.  NN  ->  ( ph  ->  ( ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  k )
)  =  if ( P  <_  k ,  B ,  0 )  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  ( k  +  1 ) ) )  =  if ( P  <_ 
( k  +  1 ) ,  B , 
0 ) ) ) )
214213a2d 25 . . 3  |-  ( k  e.  NN  ->  (
( ph  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  k )
)  =  if ( P  <_  k ,  B ,  0 ) )  ->  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )  =  if ( P  <_  (
k  +  1 ) ,  B ,  0 ) ) ) )
2157, 13, 19, 25, 57, 214nnind 10056 . 2  |-  ( N  e.  NN  ->  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  N ) )  =  if ( P  <_  N ,  B , 
0 ) ) )
2161, 215mpcom 35 1  |-  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  N
) )  =  if ( P  <_  N ,  B ,  0 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1654    e. wcel 1728    =/= wne 2606   A.wral 2712   _Vcvv 2965   [_csb 3270   ifcif 3767   class class class wbr 4243    e. cmpt 4297   -->wf 5485   ` cfv 5489  (class class class)co 6117   RRcr 9027   0cc0 9028   1c1 9029    + caddc 9031    x. cmul 9033    < clt 9158    <_ cle 9159   NNcn 10038   2c2 10087   NN0cn0 10259   ZZcz 10320   ZZ>=cuz 10526    seq cseq 11361   ^cexp 11420    || cdivides 12890   Primecprime 13117    pCnt cpc 13248
This theorem is referenced by:  pcmpt2  13300  pcprod  13302  1arithlem4  13332  chtublem  21033  bposlem3  21108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-cnex 9084  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-mulcom 9092  ax-addass 9093  ax-mulass 9094  ax-distr 9095  ax-i2m1 9096  ax-1ne0 9097  ax-1rid 9098  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103  ax-pre-ltadd 9104  ax-pre-mulgt0 9105  ax-pre-sup 9106
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rmo 2720  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-br 4244  df-opab 4298  df-mpt 4299  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-1st 6385  df-2nd 6386  df-riota 6585  df-recs 6669  df-rdg 6704  df-1o 6760  df-2o 6761  df-oadd 6764  df-er 6941  df-en 7146  df-dom 7147  df-sdom 7148  df-fin 7149  df-sup 7482  df-pnf 9160  df-mnf 9161  df-xr 9162  df-ltxr 9163  df-le 9164  df-sub 9331  df-neg 9332  df-div 9716  df-nn 10039  df-2 10096  df-3 10097  df-n0 10260  df-z 10321  df-uz 10527  df-q 10613  df-rp 10651  df-fz 11082  df-fl 11240  df-mod 11289  df-seq 11362  df-exp 11421  df-cj 11942  df-re 11943  df-im 11944  df-sqr 12078  df-abs 12079  df-dvds 12891  df-gcd 13045  df-prm 13118  df-pc 13249
  Copyright terms: Public domain W3C validator