Metamath Proof Explorer

Theorem pcmpt

Description: Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypotheses 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 pcmpt 
|- ( ph -> ( P pCnt ( seq 1 ( x. , F ) ` N ) ) = if ( P <_ N , B , 0 ) )

Proof

Step Hyp Ref Expression
1 pcmpt.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )
2 pcmpt.2 
 |-  ( ph -> A. n e. Prime A e. NN0 )
3 pcmpt.3 
 |-  ( ph -> N e. NN )
4 pcmpt.4 
 |-  ( ph -> P e. Prime )
5 pcmpt.5 
 |-  ( n = P -> A = B )
6 fveq2 
 |-  ( p = 1 -> ( seq 1 ( x. , F ) ` p ) = ( seq 1 ( x. , F ) ` 1 ) )
7 6 oveq2d 
 |-  ( p = 1 -> ( P pCnt ( seq 1 ( x. , F ) ` p ) ) = ( P pCnt ( seq 1 ( x. , F ) ` 1 ) ) )
8 breq2 
 |-  ( p = 1 -> ( P <_ p <-> P <_ 1 ) )
9 8 ifbid 
 |-  ( p = 1 -> if ( P <_ p , B , 0 ) = if ( P <_ 1 , B , 0 ) )
10 7 9 eqeq12d 
 |-  ( 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 ) ) )
11 10 imbi2d 
 |-  ( 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 ) ) ) )
12 fveq2 
 |-  ( p = k -> ( seq 1 ( x. , F ) ` p ) = ( seq 1 ( x. , F ) ` k ) )
13 12 oveq2d 
 |-  ( p = k -> ( P pCnt ( seq 1 ( x. , F ) ` p ) ) = ( P pCnt ( seq 1 ( x. , F ) ` k ) ) )
14 breq2 
 |-  ( p = k -> ( P <_ p <-> P <_ k ) )
15 14 ifbid 
 |-  ( p = k -> if ( P <_ p , B , 0 ) = if ( P <_ k , B , 0 ) )
16 13 15 eqeq12d 
 |-  ( 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 ) ) )
17 16 imbi2d 
 |-  ( 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 ) ) ) )
18 fveq2 
 |-  ( p = ( k + 1 ) -> ( seq 1 ( x. , F ) ` p ) = ( seq 1 ( x. , F ) ` ( k + 1 ) ) )
19 18 oveq2d 
 |-  ( p = ( k + 1 ) -> ( P pCnt ( seq 1 ( x. , F ) ` p ) ) = ( P pCnt ( seq 1 ( x. , F ) ` ( k + 1 ) ) ) )
20 breq2 
 |-  ( p = ( k + 1 ) -> ( P <_ p <-> P <_ ( k + 1 ) ) )
21 20 ifbid 
 |-  ( p = ( k + 1 ) -> if ( P <_ p , B , 0 ) = if ( P <_ ( k + 1 ) , B , 0 ) )
22 19 21 eqeq12d 
 |-  ( 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 ) ) )
23 22 imbi2d 
 |-  ( 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 ) ) ) )
24 fveq2 
 |-  ( p = N -> ( seq 1 ( x. , F ) ` p ) = ( seq 1 ( x. , F ) ` N ) )
25 24 oveq2d 
 |-  ( p = N -> ( P pCnt ( seq 1 ( x. , F ) ` p ) ) = ( P pCnt ( seq 1 ( x. , F ) ` N ) ) )
26 breq2 
 |-  ( p = N -> ( P <_ p <-> P <_ N ) )
27 26 ifbid 
 |-  ( p = N -> if ( P <_ p , B , 0 ) = if ( P <_ N , B , 0 ) )
28 25 27 eqeq12d 
 |-  ( 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 ) ) )
29 28 imbi2d 
 |-  ( 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 ) ) ) )
30 1z 
 |-  1 e. ZZ
31 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 ) )
32 30 31 ax-mp 
 |-  ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 )
33 1nn 
 |-  1 e. NN
34 1nprm 
 |-  -. 1 e. Prime
35 eleq1 
 |-  ( n = 1 -> ( n e. Prime <-> 1 e. Prime ) )
36 34 35 mtbiri 
 |-  ( n = 1 -> -. n e. Prime )
37 36 iffalsed 
 |-  ( n = 1 -> if ( n e. Prime , ( n ^ A ) , 1 ) = 1 )
38 1ex 
 |-  1 e. _V
39 37 1 38 fvmpt 
 |-  ( 1 e. NN -> ( F ` 1 ) = 1 )
40 33 39 ax-mp 
 |-  ( F ` 1 ) = 1
41 32 40 eqtri 
 |-  ( seq 1 ( x. , F ) ` 1 ) = 1
42 41 oveq2i 
 |-  ( P pCnt ( seq 1 ( x. , F ) ` 1 ) ) = ( P pCnt 1 )
43 pc1 
 |-  ( P e. Prime -> ( P pCnt 1 ) = 0 )
44 42 43 eqtrid 
 |-  ( P e. Prime -> ( P pCnt ( seq 1 ( x. , F ) ` 1 ) ) = 0 )
45 prmgt1 
 |-  ( P e. Prime -> 1 < P )
46 1re 
 |-  1 e. RR
47 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
48 eluzelre 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. RR )
49 47 48 syl 
 |-  ( P e. Prime -> P e. RR )
50 ltnle 
 |-  ( ( 1 e. RR /\ P e. RR ) -> ( 1 < P <-> -. P <_ 1 ) )
51 46 49 50 sylancr 
 |-  ( P e. Prime -> ( 1 < P <-> -. P <_ 1 ) )
52 45 51 mpbid 
 |-  ( P e. Prime -> -. P <_ 1 )
53 52 iffalsed 
 |-  ( P e. Prime -> if ( P <_ 1 , B , 0 ) = 0 )
54 44 53 eqtr4d 
 |-  ( P e. Prime -> ( P pCnt ( seq 1 ( x. , F ) ` 1 ) ) = if ( P <_ 1 , B , 0 ) )
55 4 54 syl 
 |-  ( ph -> ( P pCnt ( seq 1 ( x. , F ) ` 1 ) ) = if ( P <_ 1 , B , 0 ) )
56 4 adantr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> P e. Prime )
57 1 2 pcmptcl 
 |-  ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
58 57 simpld 
 |-  ( ph -> F : NN --> NN )
59 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
60 ffvelcdm 
 |-  ( ( F : NN --> NN /\ ( k + 1 ) e. NN ) -> ( F ` ( k + 1 ) ) e. NN )
61 58 59 60 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) e. NN )
62 61 adantrr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( F ` ( k + 1 ) ) e. NN )
63 56 62 pccld 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( P pCnt ( F ` ( k + 1 ) ) ) e. NN0 )
64 63 nn0cnd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( P pCnt ( F ` ( k + 1 ) ) ) e. CC )
65 64 addlidd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( 0 + ( P pCnt ( F ` ( k + 1 ) ) ) ) = ( P pCnt ( F ` ( k + 1 ) ) ) )
66 59 ad2antrl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( k + 1 ) e. NN )
67 ovex 
 |-  ( n ^ A ) e. _V
68 67 38 ifex 
 |-  if ( n e. Prime , ( n ^ A ) , 1 ) e. _V
69 68 csbex 
 |-  [_ ( k + 1 ) / n ]_ if ( n e. Prime , ( n ^ A ) , 1 ) e. _V
70 1 fvmpts 
 |-  ( ( ( 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 ) )
71 ovex 
 |-  ( k + 1 ) e. _V
72 nfv 
 |-  F/ n ( k + 1 ) e. Prime
73 nfcv 
 |-  F/_ n ( k + 1 )
74 nfcv 
 |-  F/_ n ^
75 nfcsb1v 
 |-  F/_ n [_ ( k + 1 ) / n ]_ A
76 73 74 75 nfov 
 |-  F/_ n ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A )
77 nfcv 
 |-  F/_ n 1
78 72 76 77 nfif 
 |-  F/_ n if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) , 1 )
79 eleq1 
 |-  ( n = ( k + 1 ) -> ( n e. Prime <-> ( k + 1 ) e. Prime ) )
80 id 
 |-  ( n = ( k + 1 ) -> n = ( k + 1 ) )
81 csbeq1a 
 |-  ( n = ( k + 1 ) -> A = [_ ( k + 1 ) / n ]_ A )
82 80 81 oveq12d 
 |-  ( n = ( k + 1 ) -> ( n ^ A ) = ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) )
83 79 82 ifbieq1d 
 |-  ( n = ( k + 1 ) -> if ( n e. Prime , ( n ^ A ) , 1 ) = if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) , 1 ) )
84 71 78 83 csbief 
 |-  [_ ( k + 1 ) / n ]_ if ( n e. Prime , ( n ^ A ) , 1 ) = if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) , 1 )
85 70 84 eqtrdi 
 |-  ( ( ( 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 ) )
86 66 69 85 sylancl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( F ` ( k + 1 ) ) = if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) , 1 ) )
87 simprr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( k + 1 ) = P )
88 87 56 eqeltrd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( k + 1 ) e. Prime )
89 88 iftrued 
 |-  ( ( 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 ) )
90 87 csbeq1d 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> [_ ( k + 1 ) / n ]_ A = [_ P / n ]_ A )
91 nfcvd 
 |-  ( P e. Prime -> F/_ n B )
92 91 5 csbiegf 
 |-  ( P e. Prime -> [_ P / n ]_ A = B )
93 56 92 syl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> [_ P / n ]_ A = B )
94 90 93 eqtrd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> [_ ( k + 1 ) / n ]_ A = B )
95 87 94 oveq12d 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) = ( P ^ B ) )
96 86 89 95 3eqtrd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( F ` ( k + 1 ) ) = ( P ^ B ) )
97 96 oveq2d 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( P pCnt ( F ` ( k + 1 ) ) ) = ( P pCnt ( P ^ B ) ) )
98 5 eleq1d 
 |-  ( n = P -> ( A e. NN0 <-> B e. NN0 ) )
99 98 rspcv 
 |-  ( P e. Prime -> ( A. n e. Prime A e. NN0 -> B e. NN0 ) )
100 4 2 99 sylc 
 |-  ( ph -> B e. NN0 )
101 100 adantr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> B e. NN0 )
102 pcidlem 
 |-  ( ( P e. Prime /\ B e. NN0 ) -> ( P pCnt ( P ^ B ) ) = B )
103 56 101 102 syl2anc 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( P pCnt ( P ^ B ) ) = B )
104 65 97 103 3eqtrd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( 0 + ( P pCnt ( F ` ( k + 1 ) ) ) ) = B )
105 oveq1 
 |-  ( ( 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 ) ) ) ) )
106 105 eqeq1d 
 |-  ( ( 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 ) )
107 104 106 syl5ibrcom 
 |-  ( ( 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 ) )
108 nnre 
 |-  ( k e. NN -> k e. RR )
109 108 ad2antrl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> k e. RR )
110 ltp1 
 |-  ( k e. RR -> k < ( k + 1 ) )
111 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
112 ltnle 
 |-  ( ( k e. RR /\ ( k + 1 ) e. RR ) -> ( k < ( k + 1 ) <-> -. ( k + 1 ) <_ k ) )
113 111 112 mpdan 
 |-  ( k e. RR -> ( k < ( k + 1 ) <-> -. ( k + 1 ) <_ k ) )
114 110 113 mpbid 
 |-  ( k e. RR -> -. ( k + 1 ) <_ k )
115 109 114 syl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> -. ( k + 1 ) <_ k )
116 87 breq1d 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> ( ( k + 1 ) <_ k <-> P <_ k ) )
117 115 116 mtbid 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> -. P <_ k )
118 117 iffalsed 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> if ( P <_ k , B , 0 ) = 0 )
119 118 eqeq2d 
 |-  ( ( 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 ) )
120 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
121 nnuz 
 |-  NN = ( ZZ>= ` 1 )
122 120 121 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
123 seqp1 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) = ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) )
124 122 123 syl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) = ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) )
125 124 oveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( P pCnt ( seq 1 ( x. , F ) ` ( k + 1 ) ) ) = ( P pCnt ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) ) )
126 4 adantr 
 |-  ( ( ph /\ k e. NN ) -> P e. Prime )
127 57 simprd 
 |-  ( ph -> seq 1 ( x. , F ) : NN --> NN )
128 127 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` k ) e. NN )
129 nnz 
 |-  ( ( seq 1 ( x. , F ) ` k ) e. NN -> ( seq 1 ( x. , F ) ` k ) e. ZZ )
130 nnne0 
 |-  ( ( seq 1 ( x. , F ) ` k ) e. NN -> ( seq 1 ( x. , F ) ` k ) =/= 0 )
131 129 130 jca 
 |-  ( ( seq 1 ( x. , F ) ` k ) e. NN -> ( ( seq 1 ( x. , F ) ` k ) e. ZZ /\ ( seq 1 ( x. , F ) ` k ) =/= 0 ) )
132 128 131 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) e. ZZ /\ ( seq 1 ( x. , F ) ` k ) =/= 0 ) )
133 nnz 
 |-  ( ( F ` ( k + 1 ) ) e. NN -> ( F ` ( k + 1 ) ) e. ZZ )
134 nnne0 
 |-  ( ( F ` ( k + 1 ) ) e. NN -> ( F ` ( k + 1 ) ) =/= 0 )
135 133 134 jca 
 |-  ( ( F ` ( k + 1 ) ) e. NN -> ( ( F ` ( k + 1 ) ) e. ZZ /\ ( F ` ( k + 1 ) ) =/= 0 ) )
136 61 135 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` ( k + 1 ) ) e. ZZ /\ ( F ` ( k + 1 ) ) =/= 0 ) )
137 pcmul 
 |-  ( ( 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 ) ) ) ) )
138 126 132 136 137 syl3anc 
 |-  ( ( 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 ) ) ) ) )
139 125 138 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( P pCnt ( seq 1 ( x. , F ) ` ( k + 1 ) ) ) = ( ( P pCnt ( seq 1 ( x. , F ) ` k ) ) + ( P pCnt ( F ` ( k + 1 ) ) ) ) )
140 139 adantrr 
 |-  ( ( 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 ) ) ) ) )
141 prmnn 
 |-  ( P e. Prime -> P e. NN )
142 4 141 syl 
 |-  ( ph -> P e. NN )
143 142 nnred 
 |-  ( ph -> P e. RR )
144 143 adantr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> P e. RR )
145 144 leidd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> P <_ P )
146 145 87 breqtrrd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> P <_ ( k + 1 ) )
147 146 iftrued 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) = P ) ) -> if ( P <_ ( k + 1 ) , B , 0 ) = B )
148 140 147 eqeq12d 
 |-  ( ( 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 ) )
149 107 119 148 3imtr4d 
 |-  ( ( 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 ) ) )
150 149 expr 
 |-  ( ( 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 ) ) ) )
151 139 adantrr 
 |-  ( ( 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 ) ) ) ) )
152 simplrr 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( k + 1 ) =/= P )
153 152 necomd 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> P =/= ( k + 1 ) )
154 4 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> P e. Prime )
155 simpr 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( k + 1 ) e. Prime )
156 2 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> A. n e. Prime A e. NN0 )
157 75 nfel1 
 |-  F/ n [_ ( k + 1 ) / n ]_ A e. NN0
158 81 eleq1d 
 |-  ( n = ( k + 1 ) -> ( A e. NN0 <-> [_ ( k + 1 ) / n ]_ A e. NN0 ) )
159 157 158 rspc 
 |-  ( ( k + 1 ) e. Prime -> ( A. n e. Prime A e. NN0 -> [_ ( k + 1 ) / n ]_ A e. NN0 ) )
160 155 156 159 sylc 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> [_ ( k + 1 ) / n ]_ A e. NN0 )
161 prmdvdsexpr 
 |-  ( ( P e. Prime /\ ( k + 1 ) e. Prime /\ [_ ( k + 1 ) / n ]_ A e. NN0 ) -> ( P || ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) -> P = ( k + 1 ) ) )
162 154 155 160 161 syl3anc 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( P || ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) -> P = ( k + 1 ) ) )
163 162 necon3ad 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( P =/= ( k + 1 ) -> -. P || ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) ) )
164 153 163 mpd 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> -. P || ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) )
165 59 ad2antrl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( k + 1 ) e. NN )
166 165 69 85 sylancl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( F ` ( k + 1 ) ) = if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) , 1 ) )
167 iftrue 
 |-  ( ( k + 1 ) e. Prime -> if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) , 1 ) = ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) )
168 166 167 sylan9eq 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( F ` ( k + 1 ) ) = ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) )
169 168 breq2d 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( P || ( F ` ( k + 1 ) ) <-> P || ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) ) )
170 164 169 mtbird 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> -. P || ( F ` ( k + 1 ) ) )
171 58 adantr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> F : NN --> NN )
172 171 165 60 syl2anc 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( F ` ( k + 1 ) ) e. NN )
173 172 adantr 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( F ` ( k + 1 ) ) e. NN )
174 pceq0 
 |-  ( ( P e. Prime /\ ( F ` ( k + 1 ) ) e. NN ) -> ( ( P pCnt ( F ` ( k + 1 ) ) ) = 0 <-> -. P || ( F ` ( k + 1 ) ) ) )
175 154 173 174 syl2anc 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( ( P pCnt ( F ` ( k + 1 ) ) ) = 0 <-> -. P || ( F ` ( k + 1 ) ) ) )
176 170 175 mpbird 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ ( k + 1 ) e. Prime ) -> ( P pCnt ( F ` ( k + 1 ) ) ) = 0 )
177 iffalse 
 |-  ( -. ( k + 1 ) e. Prime -> if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ [_ ( k + 1 ) / n ]_ A ) , 1 ) = 1 )
178 166 177 sylan9eq 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ -. ( k + 1 ) e. Prime ) -> ( F ` ( k + 1 ) ) = 1 )
179 178 oveq2d 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ -. ( k + 1 ) e. Prime ) -> ( P pCnt ( F ` ( k + 1 ) ) ) = ( P pCnt 1 ) )
180 4 43 syl 
 |-  ( ph -> ( P pCnt 1 ) = 0 )
181 180 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ -. ( k + 1 ) e. Prime ) -> ( P pCnt 1 ) = 0 )
182 179 181 eqtrd 
 |-  ( ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) /\ -. ( k + 1 ) e. Prime ) -> ( P pCnt ( F ` ( k + 1 ) ) ) = 0 )
183 176 182 pm2.61dan 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P pCnt ( F ` ( k + 1 ) ) ) = 0 )
184 183 oveq2d 
 |-  ( ( 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 ) )
185 4 adantr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> P e. Prime )
186 128 adantrr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( seq 1 ( x. , F ) ` k ) e. NN )
187 185 186 pccld 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P pCnt ( seq 1 ( x. , F ) ` k ) ) e. NN0 )
188 187 nn0cnd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P pCnt ( seq 1 ( x. , F ) ` k ) ) e. CC )
189 188 addridd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( ( P pCnt ( seq 1 ( x. , F ) ` k ) ) + 0 ) = ( P pCnt ( seq 1 ( x. , F ) ` k ) ) )
190 151 184 189 3eqtrd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P pCnt ( seq 1 ( x. , F ) ` ( k + 1 ) ) ) = ( P pCnt ( seq 1 ( x. , F ) ` k ) ) )
191 142 adantr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> P e. NN )
192 191 nnred 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> P e. RR )
193 165 nnred 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( k + 1 ) e. RR )
194 192 193 ltlend 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P < ( k + 1 ) <-> ( P <_ ( k + 1 ) /\ ( k + 1 ) =/= P ) ) )
195 simprl 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> k e. NN )
196 nnleltp1 
 |-  ( ( P e. NN /\ k e. NN ) -> ( P <_ k <-> P < ( k + 1 ) ) )
197 191 195 196 syl2anc 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P <_ k <-> P < ( k + 1 ) ) )
198 simprr 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( k + 1 ) =/= P )
199 198 biantrud 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P <_ ( k + 1 ) <-> ( P <_ ( k + 1 ) /\ ( k + 1 ) =/= P ) ) )
200 194 197 199 3bitr4rd 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> ( P <_ ( k + 1 ) <-> P <_ k ) )
201 200 ifbid 
 |-  ( ( ph /\ ( k e. NN /\ ( k + 1 ) =/= P ) ) -> if ( P <_ ( k + 1 ) , B , 0 ) = if ( P <_ k , B , 0 ) )
202 190 201 eqeq12d 
 |-  ( ( 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 ) ) )
203 202 biimprd 
 |-  ( ( 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 ) ) )
204 203 expr 
 |-  ( ( 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 ) ) ) )
205 150 204 pm2.61dne 
 |-  ( ( 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 ) ) )
206 205 expcom 
 |-  ( 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 ) ) ) )
207 206 a2d 
 |-  ( 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 ) ) ) )
208 11 17 23 29 55 207 nnind 
 |-  ( N e. NN -> ( ph -> ( P pCnt ( seq 1 ( x. , F ) ` N ) ) = if ( P <_ N , B , 0 ) ) )
209 3 208 mpcom 
 |-  ( ph -> ( P pCnt ( seq 1 ( x. , F ) ` N ) ) = if ( P <_ N , B , 0 ) )