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=nifnnA1
pcmpt.2 φnA0
pcmpt.3 φN
pcmpt.4 φP
pcmpt.5 n=PA=B
Assertion pcmpt φPpCntseq1×FN=ifPNB0

Proof

Step Hyp Ref Expression
1 pcmpt.1 F=nifnnA1
2 pcmpt.2 φnA0
3 pcmpt.3 φN
4 pcmpt.4 φP
5 pcmpt.5 n=PA=B
6 fveq2 p=1seq1×Fp=seq1×F1
7 6 oveq2d p=1PpCntseq1×Fp=PpCntseq1×F1
8 breq2 p=1PpP1
9 8 ifbid p=1ifPpB0=ifP1B0
10 7 9 eqeq12d p=1PpCntseq1×Fp=ifPpB0PpCntseq1×F1=ifP1B0
11 10 imbi2d p=1φPpCntseq1×Fp=ifPpB0φPpCntseq1×F1=ifP1B0
12 fveq2 p=kseq1×Fp=seq1×Fk
13 12 oveq2d p=kPpCntseq1×Fp=PpCntseq1×Fk
14 breq2 p=kPpPk
15 14 ifbid p=kifPpB0=ifPkB0
16 13 15 eqeq12d p=kPpCntseq1×Fp=ifPpB0PpCntseq1×Fk=ifPkB0
17 16 imbi2d p=kφPpCntseq1×Fp=ifPpB0φPpCntseq1×Fk=ifPkB0
18 fveq2 p=k+1seq1×Fp=seq1×Fk+1
19 18 oveq2d p=k+1PpCntseq1×Fp=PpCntseq1×Fk+1
20 breq2 p=k+1PpPk+1
21 20 ifbid p=k+1ifPpB0=ifPk+1B0
22 19 21 eqeq12d p=k+1PpCntseq1×Fp=ifPpB0PpCntseq1×Fk+1=ifPk+1B0
23 22 imbi2d p=k+1φPpCntseq1×Fp=ifPpB0φPpCntseq1×Fk+1=ifPk+1B0
24 fveq2 p=Nseq1×Fp=seq1×FN
25 24 oveq2d p=NPpCntseq1×Fp=PpCntseq1×FN
26 breq2 p=NPpPN
27 26 ifbid p=NifPpB0=ifPNB0
28 25 27 eqeq12d p=NPpCntseq1×Fp=ifPpB0PpCntseq1×FN=ifPNB0
29 28 imbi2d p=NφPpCntseq1×Fp=ifPpB0φPpCntseq1×FN=ifPNB0
30 1z 1
31 seq1 1seq1×F1=F1
32 30 31 ax-mp seq1×F1=F1
33 1nn 1
34 1nprm ¬1
35 eleq1 n=1n1
36 34 35 mtbiri n=1¬n
37 36 iffalsed n=1ifnnA1=1
38 1ex 1V
39 37 1 38 fvmpt 1F1=1
40 33 39 ax-mp F1=1
41 32 40 eqtri seq1×F1=1
42 41 oveq2i PpCntseq1×F1=PpCnt1
43 pc1 PPpCnt1=0
44 42 43 eqtrid PPpCntseq1×F1=0
45 prmgt1 P1<P
46 1re 1
47 prmuz2 PP2
48 eluzelre P2P
49 47 48 syl PP
50 ltnle 1P1<P¬P1
51 46 49 50 sylancr P1<P¬P1
52 45 51 mpbid P¬P1
53 52 iffalsed PifP1B0=0
54 44 53 eqtr4d PPpCntseq1×F1=ifP1B0
55 4 54 syl φPpCntseq1×F1=ifP1B0
56 4 adantr φkk+1=PP
57 1 2 pcmptcl φF:seq1×F:
58 57 simpld φF:
59 peano2nn kk+1
60 ffvelrn F:k+1Fk+1
61 58 59 60 syl2an φkFk+1
62 61 adantrr φkk+1=PFk+1
63 56 62 pccld φkk+1=PPpCntFk+10
64 63 nn0cnd φkk+1=PPpCntFk+1
65 64 addid2d φkk+1=P0+PpCntFk+1=PpCntFk+1
66 59 ad2antrl φkk+1=Pk+1
67 ovex nAV
68 67 38 ifex ifnnA1V
69 68 csbex k+1/nifnnA1V
70 1 fvmpts k+1k+1/nifnnA1VFk+1=k+1/nifnnA1
71 ovex k+1V
72 nfv nk+1
73 nfcv _nk+1
74 nfcv _n^
75 nfcsb1v _nk+1/nA
76 73 74 75 nfov _nk+1k+1/nA
77 nfcv _n1
78 72 76 77 nfif _nifk+1k+1k+1/nA1
79 eleq1 n=k+1nk+1
80 id n=k+1n=k+1
81 csbeq1a n=k+1A=k+1/nA
82 80 81 oveq12d n=k+1nA=k+1k+1/nA
83 79 82 ifbieq1d n=k+1ifnnA1=ifk+1k+1k+1/nA1
84 71 78 83 csbief k+1/nifnnA1=ifk+1k+1k+1/nA1
85 70 84 eqtrdi k+1k+1/nifnnA1VFk+1=ifk+1k+1k+1/nA1
86 66 69 85 sylancl φkk+1=PFk+1=ifk+1k+1k+1/nA1
87 simprr φkk+1=Pk+1=P
88 87 56 eqeltrd φkk+1=Pk+1
89 88 iftrued φkk+1=Pifk+1k+1k+1/nA1=k+1k+1/nA
90 87 csbeq1d φkk+1=Pk+1/nA=P/nA
91 nfcvd P_nB
92 91 5 csbiegf PP/nA=B
93 56 92 syl φkk+1=PP/nA=B
94 90 93 eqtrd φkk+1=Pk+1/nA=B
95 87 94 oveq12d φkk+1=Pk+1k+1/nA=PB
96 86 89 95 3eqtrd φkk+1=PFk+1=PB
97 96 oveq2d φkk+1=PPpCntFk+1=PpCntPB
98 5 eleq1d n=PA0B0
99 98 rspcv PnA0B0
100 4 2 99 sylc φB0
101 100 adantr φkk+1=PB0
102 pcidlem PB0PpCntPB=B
103 56 101 102 syl2anc φkk+1=PPpCntPB=B
104 65 97 103 3eqtrd φkk+1=P0+PpCntFk+1=B
105 oveq1 PpCntseq1×Fk=0PpCntseq1×Fk+PpCntFk+1=0+PpCntFk+1
106 105 eqeq1d PpCntseq1×Fk=0PpCntseq1×Fk+PpCntFk+1=B0+PpCntFk+1=B
107 104 106 syl5ibrcom φkk+1=PPpCntseq1×Fk=0PpCntseq1×Fk+PpCntFk+1=B
108 nnre kk
109 108 ad2antrl φkk+1=Pk
110 ltp1 kk<k+1
111 peano2re kk+1
112 ltnle kk+1k<k+1¬k+1k
113 111 112 mpdan kk<k+1¬k+1k
114 110 113 mpbid k¬k+1k
115 109 114 syl φkk+1=P¬k+1k
116 87 breq1d φkk+1=Pk+1kPk
117 115 116 mtbid φkk+1=P¬Pk
118 117 iffalsed φkk+1=PifPkB0=0
119 118 eqeq2d φkk+1=PPpCntseq1×Fk=ifPkB0PpCntseq1×Fk=0
120 simpr φkk
121 nnuz =1
122 120 121 eleqtrdi φkk1
123 seqp1 k1seq1×Fk+1=seq1×FkFk+1
124 122 123 syl φkseq1×Fk+1=seq1×FkFk+1
125 124 oveq2d φkPpCntseq1×Fk+1=PpCntseq1×FkFk+1
126 4 adantr φkP
127 57 simprd φseq1×F:
128 127 ffvelrnda φkseq1×Fk
129 nnz seq1×Fkseq1×Fk
130 nnne0 seq1×Fkseq1×Fk0
131 129 130 jca seq1×Fkseq1×Fkseq1×Fk0
132 128 131 syl φkseq1×Fkseq1×Fk0
133 nnz Fk+1Fk+1
134 nnne0 Fk+1Fk+10
135 133 134 jca Fk+1Fk+1Fk+10
136 61 135 syl φkFk+1Fk+10
137 pcmul Pseq1×Fkseq1×Fk0Fk+1Fk+10PpCntseq1×FkFk+1=PpCntseq1×Fk+PpCntFk+1
138 126 132 136 137 syl3anc φkPpCntseq1×FkFk+1=PpCntseq1×Fk+PpCntFk+1
139 125 138 eqtrd φkPpCntseq1×Fk+1=PpCntseq1×Fk+PpCntFk+1
140 139 adantrr φkk+1=PPpCntseq1×Fk+1=PpCntseq1×Fk+PpCntFk+1
141 prmnn PP
142 4 141 syl φP
143 142 nnred φP
144 143 adantr φkk+1=PP
145 144 leidd φkk+1=PPP
146 145 87 breqtrrd φkk+1=PPk+1
147 146 iftrued φkk+1=PifPk+1B0=B
148 140 147 eqeq12d φkk+1=PPpCntseq1×Fk+1=ifPk+1B0PpCntseq1×Fk+PpCntFk+1=B
149 107 119 148 3imtr4d φkk+1=PPpCntseq1×Fk=ifPkB0PpCntseq1×Fk+1=ifPk+1B0
150 149 expr φkk+1=PPpCntseq1×Fk=ifPkB0PpCntseq1×Fk+1=ifPk+1B0
151 139 adantrr φkk+1PPpCntseq1×Fk+1=PpCntseq1×Fk+PpCntFk+1
152 simplrr φkk+1Pk+1k+1P
153 152 necomd φkk+1Pk+1Pk+1
154 4 ad2antrr φkk+1Pk+1P
155 simpr φkk+1Pk+1k+1
156 2 ad2antrr φkk+1Pk+1nA0
157 75 nfel1 nk+1/nA0
158 81 eleq1d n=k+1A0k+1/nA0
159 157 158 rspc k+1nA0k+1/nA0
160 155 156 159 sylc φkk+1Pk+1k+1/nA0
161 prmdvdsexpr Pk+1k+1/nA0Pk+1k+1/nAP=k+1
162 154 155 160 161 syl3anc φkk+1Pk+1Pk+1k+1/nAP=k+1
163 162 necon3ad φkk+1Pk+1Pk+1¬Pk+1k+1/nA
164 153 163 mpd φkk+1Pk+1¬Pk+1k+1/nA
165 59 ad2antrl φkk+1Pk+1
166 165 69 85 sylancl φkk+1PFk+1=ifk+1k+1k+1/nA1
167 iftrue k+1ifk+1k+1k+1/nA1=k+1k+1/nA
168 166 167 sylan9eq φkk+1Pk+1Fk+1=k+1k+1/nA
169 168 breq2d φkk+1Pk+1PFk+1Pk+1k+1/nA
170 164 169 mtbird φkk+1Pk+1¬PFk+1
171 58 adantr φkk+1PF:
172 171 165 60 syl2anc φkk+1PFk+1
173 172 adantr φkk+1Pk+1Fk+1
174 pceq0 PFk+1PpCntFk+1=0¬PFk+1
175 154 173 174 syl2anc φkk+1Pk+1PpCntFk+1=0¬PFk+1
176 170 175 mpbird φkk+1Pk+1PpCntFk+1=0
177 iffalse ¬k+1ifk+1k+1k+1/nA1=1
178 166 177 sylan9eq φkk+1P¬k+1Fk+1=1
179 178 oveq2d φkk+1P¬k+1PpCntFk+1=PpCnt1
180 4 43 syl φPpCnt1=0
181 180 ad2antrr φkk+1P¬k+1PpCnt1=0
182 179 181 eqtrd φkk+1P¬k+1PpCntFk+1=0
183 176 182 pm2.61dan φkk+1PPpCntFk+1=0
184 183 oveq2d φkk+1PPpCntseq1×Fk+PpCntFk+1=PpCntseq1×Fk+0
185 4 adantr φkk+1PP
186 128 adantrr φkk+1Pseq1×Fk
187 185 186 pccld φkk+1PPpCntseq1×Fk0
188 187 nn0cnd φkk+1PPpCntseq1×Fk
189 188 addid1d φkk+1PPpCntseq1×Fk+0=PpCntseq1×Fk
190 151 184 189 3eqtrd φkk+1PPpCntseq1×Fk+1=PpCntseq1×Fk
191 142 adantr φkk+1PP
192 191 nnred φkk+1PP
193 165 nnred φkk+1Pk+1
194 192 193 ltlend φkk+1PP<k+1Pk+1k+1P
195 simprl φkk+1Pk
196 nnleltp1 PkPkP<k+1
197 191 195 196 syl2anc φkk+1PPkP<k+1
198 simprr φkk+1Pk+1P
199 198 biantrud φkk+1PPk+1Pk+1k+1P
200 194 197 199 3bitr4rd φkk+1PPk+1Pk
201 200 ifbid φkk+1PifPk+1B0=ifPkB0
202 190 201 eqeq12d φkk+1PPpCntseq1×Fk+1=ifPk+1B0PpCntseq1×Fk=ifPkB0
203 202 biimprd φkk+1PPpCntseq1×Fk=ifPkB0PpCntseq1×Fk+1=ifPk+1B0
204 203 expr φkk+1PPpCntseq1×Fk=ifPkB0PpCntseq1×Fk+1=ifPk+1B0
205 150 204 pm2.61dne φkPpCntseq1×Fk=ifPkB0PpCntseq1×Fk+1=ifPk+1B0
206 205 expcom kφPpCntseq1×Fk=ifPkB0PpCntseq1×Fk+1=ifPk+1B0
207 206 a2d kφPpCntseq1×Fk=ifPkB0φPpCntseq1×Fk+1=ifPk+1B0
208 11 17 23 29 55 207 nnind NφPpCntseq1×FN=ifPNB0
209 3 208 mpcom φPpCntseq1×FN=ifPNB0