pcmpt

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

	Ref	Expression
Hypotheses	pcmpt.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, n^{A}, 1))$
	pcmpt.2	$⊢ φ \to \forall n \in ℙ A \in ℕ_{0}$
	pcmpt.3	$⊢ φ \to N \in ℕ$
	pcmpt.4	$⊢ φ \to P \in ℙ$
	pcmpt.5	$⊢ n = P \to A = B$
Assertion	pcmpt	$⊢ φ \to P pCnt seq 1 (\times F) (N) = if (P \leq N, B, 0)$

Proof

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

Metamath Proof Explorer

Theorem pcmpt

Proof