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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ 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 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑘 + 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 addid2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑘 + 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 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 addid1d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑘 + 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 ) )