Theorem pcmpt

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

	Ref	Expression
Hypotheses	pcmpt.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) )
	pcmpt.2	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ 𝐴 ∈ ℕ0 )
	pcmpt.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	pcmpt.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	pcmpt.5	⊢ ( 𝑛 = 𝑃 → 𝐴 = 𝐵 )
Assertion	pcmpt	⊢ ( 𝜑 → ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) = if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) )

Proof

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