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

Theorem pcmpt 13190
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 5670 . . . . . 6  |-  ( p  =  1  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  1
) )
32oveq2d 6038 . . . . 5  |-  ( p  =  1  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  1 )
) )
4 breq2 4159 . . . . . 6  |-  ( p  =  1  ->  ( P  <_  p  <->  P  <_  1 ) )
54ifbid 3702 . . . . 5  |-  ( p  =  1  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  1 ,  B ,  0 ) )
63, 5eqeq12d 2403 . . . 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 308 . . 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 5670 . . . . . 6  |-  ( p  =  k  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  k
) )
98oveq2d 6038 . . . . 5  |-  ( p  =  k  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  k )
) )
10 breq2 4159 . . . . . 6  |-  ( p  =  k  ->  ( P  <_  p  <->  P  <_  k ) )
1110ifbid 3702 . . . . 5  |-  ( p  =  k  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  k ,  B ,  0 ) )
129, 11eqeq12d 2403 . . . 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 308 . . 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 5670 . . . . . 6  |-  ( p  =  ( k  +  1 )  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )
1514oveq2d 6038 . . . . 5  |-  ( p  =  ( k  +  1 )  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  ( k  +  1 ) ) ) )
16 breq2 4159 . . . . . 6  |-  ( p  =  ( k  +  1 )  ->  ( P  <_  p  <->  P  <_  ( k  +  1 ) ) )
1716ifbid 3702 . . . . 5  |-  ( p  =  ( k  +  1 )  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  ( k  +  1 ) ,  B ,  0 ) )
1815, 17eqeq12d 2403 . . . 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 308 . . 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 5670 . . . . . 6  |-  ( p  =  N  ->  (  seq  1 (  x.  ,  F ) `  p
)  =  (  seq  1 (  x.  ,  F ) `  N
) )
2120oveq2d 6038 . . . . 5  |-  ( p  =  N  ->  ( P  pCnt  (  seq  1
(  x.  ,  F
) `  p )
)  =  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  N )
) )
22 breq2 4159 . . . . . 6  |-  ( p  =  N  ->  ( P  <_  p  <->  P  <_  N ) )
2322ifbid 3702 . . . . 5  |-  ( p  =  N  ->  if ( P  <_  p ,  B ,  0 )  =  if ( P  <_  N ,  B ,  0 ) )
2421, 23eqeq12d 2403 . . . 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 308 . . 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 10245 . . . . . . . . 9  |-  1  e.  ZZ
28 seq1 11265 . . . . . . . . 9  |-  ( 1  e.  ZZ  ->  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 ) )
2927, 28ax-mp 8 . . . . . . . 8  |-  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 )
30 1nn 9945 . . . . . . . . 9  |-  1  e.  NN
31 1nprm 13013 . . . . . . . . . . . 12  |-  -.  1  e.  Prime
32 eleq1 2449 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
n  e.  Prime  <->  1  e.  Prime ) )
3331, 32mtbiri 295 . . . . . . . . . . 11  |-  ( n  =  1  ->  -.  n  e.  Prime )
34 iffalse 3691 . . . . . . . . . . 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 9021 . . . . . . . . . 10  |-  1  e.  _V
3835, 36, 37fvmpt 5747 . . . . . . . . 9  |-  ( 1  e.  NN  ->  ( F `  1 )  =  1 )
3930, 38ax-mp 8 . . . . . . . 8  |-  ( F `
 1 )  =  1
4029, 39eqtri 2409 . . . . . . 7  |-  (  seq  1 (  x.  ,  F ) `  1
)  =  1
4140oveq2i 6033 . . . . . 6  |-  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  1 )
)  =  ( P 
pCnt  1 )
42 pc1 13158 . . . . . 6  |-  ( P  e.  Prime  ->  ( P 
pCnt  1 )  =  0 )
4341, 42syl5eq 2433 . . . . 5  |-  ( P  e.  Prime  ->  ( P 
pCnt  (  seq  1
(  x.  ,  F
) `  1 )
)  =  0 )
44 prmuz2 13026 . . . . . . . 8  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
45 eluz2b2 10482 . . . . . . . . 9  |-  ( P  e.  ( ZZ>= `  2
)  <->  ( P  e.  NN  /\  1  < 
P ) )
4645simprbi 451 . . . . . . . 8  |-  ( P  e.  ( ZZ>= `  2
)  ->  1  <  P )
4744, 46syl 16 . . . . . . 7  |-  ( P  e.  Prime  ->  1  < 
P )
48 1re 9025 . . . . . . . 8  |-  1  e.  RR
49 eluzelre 10431 . . . . . . . . 9  |-  ( P  e.  ( ZZ>= `  2
)  ->  P  e.  RR )
5044, 49syl 16 . . . . . . . 8  |-  ( P  e.  Prime  ->  P  e.  RR )
51 ltnle 9090 . . . . . . . 8  |-  ( ( 1  e.  RR  /\  P  e.  RR )  ->  ( 1  <  P  <->  -.  P  <_  1 ) )
5248, 50, 51sylancr 645 . . . . . . 7  |-  ( P  e.  Prime  ->  ( 1  <  P  <->  -.  P  <_  1 ) )
5347, 52mpbid 202 . . . . . 6  |-  ( P  e.  Prime  ->  -.  P  <_  1 )
54 iffalse 3691 . . . . . 6  |-  ( -.  P  <_  1  ->  if ( P  <_  1 ,  B ,  0 )  =  0 )
5553, 54syl 16 . . . . 5  |-  ( P  e.  Prime  ->  if ( P  <_  1 ,  B ,  0 )  =  0 )
5643, 55eqtr4d 2424 . . . 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 452 . . . . . . . . . . . . 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 13189 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F : NN --> NN  /\  seq  1 (  x.  ,  F ) : NN --> NN ) )
6160simpld 446 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : NN --> NN )
62 peano2nn 9946 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
63 ffvelrn 5809 . . . . . . . . . . . . . . 15  |-  ( ( F : NN --> NN  /\  ( k  +  1 )  e.  NN )  ->  ( F `  ( k  +  1 ) )  e.  NN )
6461, 62, 63syl2an 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 ( k  +  1 ) )  e.  NN )
6564adantrr 698 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( F `  (
k  +  1 ) )  e.  NN )
6658, 65pccld 13153 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  e.  NN0 )
6766nn0cnd 10210 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  e.  CC )
6867addid2d 9201 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( 0  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )  =  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )
6962ad2antrl 709 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( k  +  1 )  e.  NN )
70 ovex 6047 . . . . . . . . . . . . . 14  |-  ( k  +  1 )  e. 
_V
71 ovex 6047 . . . . . . . . . . . . . . 15  |-  ( n ^ A )  e. 
_V
7271, 37ifex 3742 . . . . . . . . . . . . . 14  |-  if ( n  e.  Prime ,  ( n ^ A ) ,  1 )  e. 
_V
7370, 72csbex 3207 . . . . . . . . . . . . 13  |-  [_ (
k  +  1 )  /  n ]_ if ( n  e.  Prime ,  ( n ^ A
) ,  1 )  e.  _V
7436fvmpts 5748 . . . . . . . . . . . . . 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 1626 . . . . . . . . . . . . . . . 16  |-  F/ n
( k  +  1 )  e.  Prime
76 nfcv 2525 . . . . . . . . . . . . . . . . 17  |-  F/_ n
( k  +  1 )
77 nfcv 2525 . . . . . . . . . . . . . . . . 17  |-  F/_ n ^
78 nfcsb1v 3228 . . . . . . . . . . . . . . . . 17  |-  F/_ n [_ ( k  +  1 )  /  n ]_ A
7976, 77, 78nfov 6045 . . . . . . . . . . . . . . . 16  |-  F/_ n
( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A )
80 nfcv 2525 . . . . . . . . . . . . . . . 16  |-  F/_ n
1
8175, 79, 80nfif 3708 . . . . . . . . . . . . . . 15  |-  F/_ n if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ,  1 )
82 eleq1 2449 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( k  +  1 )  ->  (
n  e.  Prime  <->  ( k  +  1 )  e. 
Prime ) )
83 id 20 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( k  +  1 )  ->  n  =  ( k  +  1 ) )
84 csbeq1a 3204 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( k  +  1 )  ->  A  =  [_ ( k  +  1 )  /  n ]_ A )
8583, 84oveq12d 6040 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( k  +  1 )  ->  (
n ^ A )  =  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) )
86 eqidd 2390 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( k  +  1 )  ->  1  =  1 )
8782, 85, 86ifbieq12d 3706 . . . . . . . . . . . . . . 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 3237 . . . . . . . . . . . . . 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 2437 . . . . . . . . . . . . 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 644 . . . . . . . . . . . 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 734 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( k  +  1 )  =  P )
9291, 58eqeltrd 2463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( k  +  1 )  e.  Prime )
93 iftrue 3690 . . . . . . . . . . . . 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 3202 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  [_ ( k  +  1 )  /  n ]_ A  =  [_ P  /  n ]_ A )
96 nfcvd 2526 . . . . . . . . . . . . . . . 16  |-  ( P  e.  Prime  ->  F/_ n B )
97 pcmpt.5 . . . . . . . . . . . . . . . 16  |-  ( n  =  P  ->  A  =  B )
9896, 97csbiegf 3236 . . . . . . . . . . . . . . 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 2421 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  [_ ( k  +  1 )  /  n ]_ A  =  B )
10191, 100oveq12d 6040 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A )  =  ( P ^ B ) )
10290, 94, 1013eqtrd 2425 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( F `  (
k  +  1 ) )  =  ( P ^ B ) )
103102oveq2d 6038 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  =  ( P 
pCnt  ( P ^ B ) ) )
10497eleq1d 2455 . . . . . . . . . . . . . 14  |-  ( n  =  P  ->  ( A  e.  NN0  <->  B  e.  NN0 ) )
105104rspcv 2993 . . . . . . . . . . . . 13  |-  ( P  e.  Prime  ->  ( A. n  e.  Prime  A  e. 
NN0  ->  B  e.  NN0 ) )
10626, 59, 105sylc 58 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  NN0 )
107106adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  B  e.  NN0 )
108 pcidlem 13174 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  B  e.  NN0 )  ->  ( P  pCnt  ( P ^ B ) )  =  B )
10958, 107, 108syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( P  pCnt  ( P ^ B ) )  =  B )
11068, 103, 1093eqtrd 2425 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( 0  +  ( P  pCnt  ( F `  ( k  +  1 ) ) ) )  =  B )
111 oveq1 6029 . . . . . . . . . 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 2397 . . . . . . . . 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 214 . . . . . . . 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 9941 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  RR )
115114ad2antrl 709 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
k  e.  RR )
116 ltp1 9782 . . . . . . . . . . . . 13  |-  ( k  e.  RR  ->  k  <  ( k  +  1 ) )
117 peano2re 9173 . . . . . . . . . . . . . 14  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
118 ltnle 9090 . . . . . . . . . . . . . 14  |-  ( ( k  e.  RR  /\  ( k  +  1 )  e.  RR )  ->  ( k  < 
( k  +  1 )  <->  -.  ( k  +  1 )  <_ 
k ) )
119117, 118mpdan 650 . . . . . . . . . . . . 13  |-  ( k  e.  RR  ->  (
k  <  ( k  +  1 )  <->  -.  (
k  +  1 )  <_  k ) )
120116, 119mpbid 202 . . . . . . . . . . . 12  |-  ( k  e.  RR  ->  -.  ( k  +  1 )  <_  k )
121115, 120syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  -.  ( k  +  1 )  <_  k )
12291breq1d 4165 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  -> 
( ( k  +  1 )  <_  k  <->  P  <_  k ) )
123121, 122mtbid 292 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  -.  P  <_  k )
124 iffalse 3691 . . . . . . . . . 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 2400 . . . . . . . 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 448 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
128 nnuz 10455 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
129127, 128syl6eleq 2479 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  1 )
)
130 seqp1 11267 . . . . . . . . . . . . 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 6038 . . . . . . . . . . 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 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  P  e. 
Prime )
13460simprd 450 . . . . . . . . . . . . . 14  |-  ( ph  ->  seq  1 (  x.  ,  F ) : NN --> NN )
135134ffvelrnda 5811 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  x.  ,  F ) `  k
)  e.  NN )
136 nnz 10237 . . . . . . . . . . . . . 14  |-  ( (  seq  1 (  x.  ,  F ) `  k )  e.  NN  ->  (  seq  1 (  x.  ,  F ) `
 k )  e.  ZZ )
137 nnne0 9966 . . . . . . . . . . . . . 14  |-  ( (  seq  1 (  x.  ,  F ) `  k )  e.  NN  ->  (  seq  1 (  x.  ,  F ) `
 k )  =/=  0 )
138136, 137jca 519 . . . . . . . . . . . . 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 10237 . . . . . . . . . . . . . 14  |-  ( ( F `  ( k  +  1 ) )  e.  NN  ->  ( F `  ( k  +  1 ) )  e.  ZZ )
141 nnne0 9966 . . . . . . . . . . . . . 14  |-  ( ( F `  ( k  +  1 ) )  e.  NN  ->  ( F `  ( k  +  1 ) )  =/=  0 )
142140, 141jca 519 . . . . . . . . . . . . 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 13154 . . . . . . . . . . . 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 1184 . . . . . . . . . . 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 2421 . . . . . . . . . 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 698 . . . . . . . . 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 13011 . . . . . . . . . . . . . . 15  |-  ( P  e.  Prime  ->  P  e.  NN )
14926, 148syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  NN )
150149nnred 9949 . . . . . . . . . . . . 13  |-  ( ph  ->  P  e.  RR )
151150adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  P  e.  RR )
152151leidd 9527 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  P  <_  P )
153152, 91breqtrrd 4181 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =  P ) )  ->  P  <_  ( k  +  1 ) )
154 iftrue 3690 . . . . . . . . . 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 2403 . . . . . . . 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 260 . . . . . . 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 599 . . . . . 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 698 . . . . . . . . . 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 738 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( k  +  1 )  =/= 
P )
161160necomd 2635 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  P  =/=  ( k  +  1 ) )
16226ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  P  e. 
Prime )
163 simpr 448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( k  +  1 )  e. 
Prime )
16459ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  A. n  e.  Prime  A  e.  NN0 )
16578nfel1 2535 . . . . . . . . . . . . . . . . . . 19  |-  F/ n [_ ( k  +  1 )  /  n ]_ A  e.  NN0
16684eleq1d 2455 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( k  +  1 )  ->  ( A  e.  NN0  <->  [_ ( k  +  1 )  /  n ]_ A  e.  NN0 ) )
167165, 166rspc 2991 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  +  1 )  e.  Prime  ->  ( A. n  e.  Prime  A  e. 
NN0  ->  [_ ( k  +  1 )  /  n ]_ A  e.  NN0 ) )
168163, 164, 167sylc 58 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  [_ (
k  +  1 )  /  n ]_ A  e.  NN0 )
169 prmdvdsexpr 13045 . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( P 
||  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A )  ->  P  =  ( k  +  1 ) ) )
171170necon3ad 2588 . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( k  +  1 )  e.  NN )
174173, 73, 89sylancl 644 . . . . . . . . . . . . . . . 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 2441 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( F `
 ( k  +  1 ) )  =  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) )
176175breq2d 4167 . . . . . . . . . . . . . 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 293 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  -.  P  ||  ( F `  (
k  +  1 ) ) )
17861adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  F : NN --> NN )
179178, 173, 63syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( F `  (
k  +  1 ) )  e.  NN )
180179adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( F `
 ( k  +  1 ) )  e.  NN )
181 pceq0 13173 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  ( F `  ( k  +  1 ) )  e.  NN )  -> 
( ( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0  <->  -.  P  ||  ( F `  ( k  +  1 ) ) ) )
182162, 180, 181syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( ( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0  <->  -.  P  ||  ( F `  ( k  +  1 ) ) ) )
183177, 182mpbird 224 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  ( k  +  1 )  e. 
Prime )  ->  ( P 
pCnt  ( F `  ( k  +  1 ) ) )  =  0 )
184 iffalse 3691 . . . . . . . . . . . . . . 15  |-  ( -.  ( k  +  1 )  e.  Prime  ->  if ( ( k  +  1 )  e.  Prime ,  ( ( k  +  1 ) ^ [_ ( k  +  1 )  /  n ]_ A ) ,  1 )  =  1 )
185174, 184sylan9eq 2441 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  -.  (
k  +  1 )  e.  Prime )  ->  ( F `  ( k  +  1 ) )  =  1 )
186185oveq2d 6038 . . . . . . . . . . . . 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 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  -.  (
k  +  1 )  e.  Prime )  ->  ( P  pCnt  1 )  =  0 )
189186, 188eqtrd 2421 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
k  e.  NN  /\  ( k  +  1 )  =/=  P ) )  /\  -.  (
k  +  1 )  e.  Prime )  ->  ( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0 )
190183, 189pm2.61dan 767 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  ( F `  ( k  +  1 ) ) )  =  0 )
191190oveq2d 6038 . . . . . . . . . 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 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  P  e.  Prime )
193135adantrr 698 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
(  seq  1 (  x.  ,  F ) `
 k )  e.  NN )
194192, 193pccld 13153 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  e.  NN0 )
195194nn0cnd 10210 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) )  e.  CC )
196195addid1d 9200 . . . . . . . . . 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 2425 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  pCnt  (  seq  1 (  x.  ,  F ) `  (
k  +  1 ) ) )  =  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  k
) ) )
198149adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  P  e.  NN )
199198nnred 9949 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  P  e.  RR )
200173nnred 9949 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( k  +  1 )  e.  RR )
201199, 200ltlend 9152 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <  (
k  +  1 )  <-> 
( P  <_  (
k  +  1 )  /\  ( k  +  1 )  =/=  P
) ) )
202 simprl 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
k  e.  NN )
203 nnleltp1 10263 . . . . . . . . . . . 12  |-  ( ( P  e.  NN  /\  k  e.  NN )  ->  ( P  <_  k  <->  P  <  ( k  +  1 ) ) )
204198, 202, 203syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <_  k  <->  P  <  ( k  +  1 ) ) )
205 simprr 734 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( k  +  1 )  =/=  P )
206205biantrud 494 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <_  (
k  +  1 )  <-> 
( P  <_  (
k  +  1 )  /\  ( k  +  1 )  =/=  P
) ) )
207201, 204, 2063bitr4rd 278 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  -> 
( P  <_  (
k  +  1 )  <-> 
P  <_  k )
)
208207ifbid 3702 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  NN  /\  ( k  +  1 )  =/= 
P ) )  ->  if ( P  <_  (
k  +  1 ) ,  B ,  0 )  =  if ( P  <_  k ,  B ,  0 ) )
209197, 208eqeq12d 2403 . . . . . . . 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 215 . . . . . . 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 599 . . . . . 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 2629 . . . . 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 425 . . . 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 24 . . 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 9952 . 2  |-  ( N  e.  NN  ->  ( ph  ->  ( P  pCnt  (  seq  1 (  x.  ,  F ) `  N ) )  =  if ( P  <_  N ,  B , 
0 ) ) )
2161, 215mpcom 34 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 177    /\ wa 359    = wceq 1649    e. wcel 1717    =/= wne 2552   A.wral 2651   _Vcvv 2901   [_csb 3196   ifcif 3684   class class class wbr 4155    e. cmpt 4209   -->wf 5392   ` cfv 5396  (class class class)co 6022   RRcr 8924   0cc0 8925   1c1 8926    + caddc 8928    x. cmul 8930    < clt 9055    <_ cle 9056   NNcn 9934   2c2 9983   NN0cn0 10155   ZZcz 10216   ZZ>=cuz 10422    seq cseq 11252   ^cexp 11311    || cdivides 12781   Primecprime 13008    pCnt cpc 13139
This theorem is referenced by:  pcmpt2  13191  pcprod  13193  1arithlem4  13223  chtublem  20864  bposlem3  20939
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-cnex 8981  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001  ax-pre-mulgt0 9002  ax-pre-sup 9003
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rmo 2659  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-int 3995  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-1st 6290  df-2nd 6291  df-riota 6487  df-recs 6571  df-rdg 6606  df-1o 6662  df-2o 6663  df-oadd 6666  df-er 6843  df-en 7048  df-dom 7049  df-sdom 7050  df-fin 7051  df-sup 7383  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061  df-sub 9227  df-neg 9228  df-div 9612  df-nn 9935  df-2 9992  df-3 9993  df-n0 10156  df-z 10217  df-uz 10423  df-q 10509  df-rp 10547  df-fz 10978  df-fl 11131  df-mod 11180  df-seq 11253  df-exp 11312  df-cj 11833  df-re 11834  df-im 11835  df-sqr 11969  df-abs 11970  df-dvds 12782  df-gcd 12936  df-prm 13009  df-pc 13140
  Copyright terms: Public domain W3C validator