| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pcmpt.3 | . 2
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 2 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 1 → (seq1( · ,
𝐹)‘𝑝) = (seq1( · , 𝐹)‘1)) | 
| 3 | 2 | oveq2d 7448 | . . . . 5
⊢ (𝑝 = 1 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘1))) | 
| 4 |  | breq2 5146 | . . . . . 6
⊢ (𝑝 = 1 → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ 1)) | 
| 5 | 4 | ifbid 4548 | . . . . 5
⊢ (𝑝 = 1 → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ 1, 𝐵, 0)) | 
| 6 | 3, 5 | eqeq12d 2752 | . . . 4
⊢ (𝑝 = 1 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘1)) = if(𝑃 ≤ 1, 𝐵, 0))) | 
| 7 | 6 | imbi2d 340 | . . 3
⊢ (𝑝 = 1 → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘1)) = if(𝑃 ≤ 1, 𝐵, 0)))) | 
| 8 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 𝑘 → (seq1( · , 𝐹)‘𝑝) = (seq1( · , 𝐹)‘𝑘)) | 
| 9 | 8 | oveq2d 7448 | . . . . 5
⊢ (𝑝 = 𝑘 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑘))) | 
| 10 |  | breq2 5146 | . . . . . 6
⊢ (𝑝 = 𝑘 → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ 𝑘)) | 
| 11 | 10 | ifbid 4548 | . . . . 5
⊢ (𝑝 = 𝑘 → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ 𝑘, 𝐵, 0)) | 
| 12 | 9, 11 | eqeq12d 2752 | . . . 4
⊢ (𝑝 = 𝑘 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0))) | 
| 13 | 12 | imbi2d 340 | . . 3
⊢ (𝑝 = 𝑘 → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0)))) | 
| 14 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = (𝑘 + 1) → (seq1( · , 𝐹)‘𝑝) = (seq1( · , 𝐹)‘(𝑘 + 1))) | 
| 15 | 14 | oveq2d 7448 | . . . . 5
⊢ (𝑝 = (𝑘 + 1) → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1)))) | 
| 16 |  | breq2 5146 | . . . . . 6
⊢ (𝑝 = (𝑘 + 1) → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ (𝑘 + 1))) | 
| 17 | 16 | ifbid 4548 | . . . . 5
⊢ (𝑝 = (𝑘 + 1) → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)) | 
| 18 | 15, 17 | eqeq12d 2752 | . . . 4
⊢ (𝑝 = (𝑘 + 1) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) | 
| 19 | 18 | imbi2d 340 | . . 3
⊢ (𝑝 = (𝑘 + 1) → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) | 
| 20 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 𝑁 → (seq1( · , 𝐹)‘𝑝) = (seq1( · , 𝐹)‘𝑁)) | 
| 21 | 20 | oveq2d 7448 | . . . . 5
⊢ (𝑝 = 𝑁 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑁))) | 
| 22 |  | breq2 5146 | . . . . . 6
⊢ (𝑝 = 𝑁 → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ 𝑁)) | 
| 23 | 22 | ifbid 4548 | . . . . 5
⊢ (𝑝 = 𝑁 → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ 𝑁, 𝐵, 0)) | 
| 24 | 21, 23 | eqeq12d 2752 | . . . 4
⊢ (𝑝 = 𝑁 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))) | 
| 25 | 24 | imbi2d 340 | . . 3
⊢ (𝑝 = 𝑁 → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)))) | 
| 26 |  | pcmpt.4 | . . . 4
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 27 |  | 1z 12649 | . . . . . . . . 9
⊢ 1 ∈
ℤ | 
| 28 |  | seq1 14056 | . . . . . . . . 9
⊢ (1 ∈
ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1)) | 
| 29 | 27, 28 | ax-mp 5 | . . . . . . . 8
⊢ (seq1(
· , 𝐹)‘1) =
(𝐹‘1) | 
| 30 |  | 1nn 12278 | . . . . . . . . 9
⊢ 1 ∈
ℕ | 
| 31 |  | 1nprm 16717 | . . . . . . . . . . . 12
⊢  ¬ 1
∈ ℙ | 
| 32 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑛 = 1 → (𝑛 ∈ ℙ ↔ 1 ∈
ℙ)) | 
| 33 | 31, 32 | mtbiri 327 | . . . . . . . . . . 11
⊢ (𝑛 = 1 → ¬ 𝑛 ∈
ℙ) | 
| 34 | 33 | iffalsed 4535 | . . . . . . . . . 10
⊢ (𝑛 = 1 → if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) = 1) | 
| 35 |  | pcmpt.1 | . . . . . . . . . 10
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) | 
| 36 |  | 1ex 11258 | . . . . . . . . . 10
⊢ 1 ∈
V | 
| 37 | 34, 35, 36 | fvmpt 7015 | . . . . . . . . 9
⊢ (1 ∈
ℕ → (𝐹‘1)
= 1) | 
| 38 | 30, 37 | ax-mp 5 | . . . . . . . 8
⊢ (𝐹‘1) = 1 | 
| 39 | 29, 38 | eqtri 2764 | . . . . . . 7
⊢ (seq1(
· , 𝐹)‘1) =
1 | 
| 40 | 39 | oveq2i 7443 | . . . . . 6
⊢ (𝑃 pCnt (seq1( · , 𝐹)‘1)) = (𝑃 pCnt 1) | 
| 41 |  | pc1 16894 | . . . . . 6
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) | 
| 42 | 40, 41 | eqtrid 2788 | . . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt (seq1( · , 𝐹)‘1)) =
0) | 
| 43 |  | prmgt1 16735 | . . . . . . 7
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) | 
| 44 |  | 1re 11262 | . . . . . . . 8
⊢ 1 ∈
ℝ | 
| 45 |  | prmuz2 16734 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 46 |  | eluzelre 12890 | . . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℝ) | 
| 47 | 45, 46 | syl 17 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) | 
| 48 |  | ltnle 11341 | . . . . . . . 8
⊢ ((1
∈ ℝ ∧ 𝑃
∈ ℝ) → (1 < 𝑃 ↔ ¬ 𝑃 ≤ 1)) | 
| 49 | 44, 47, 48 | sylancr 587 | . . . . . . 7
⊢ (𝑃 ∈ ℙ → (1 <
𝑃 ↔ ¬ 𝑃 ≤ 1)) | 
| 50 | 43, 49 | mpbid 232 | . . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ≤ 1) | 
| 51 | 50 | iffalsed 4535 | . . . . 5
⊢ (𝑃 ∈ ℙ → if(𝑃 ≤ 1, 𝐵, 0) = 0) | 
| 52 | 42, 51 | eqtr4d 2779 | . . . 4
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt (seq1( · , 𝐹)‘1)) = if(𝑃 ≤ 1, 𝐵, 0)) | 
| 53 | 26, 52 | syl 17 | . . 3
⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘1)) = if(𝑃 ≤ 1, 𝐵, 0)) | 
| 54 | 26 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ∈ ℙ) | 
| 55 |  | pcmpt.2 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) | 
| 56 | 35, 55 | pcmptcl 16930 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( ·
, 𝐹):ℕ⟶ℕ)) | 
| 57 | 56 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℕ⟶ℕ) | 
| 58 |  | peano2nn 12279 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) | 
| 59 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶ℕ ∧
(𝑘 + 1) ∈ ℕ)
→ (𝐹‘(𝑘 + 1)) ∈
ℕ) | 
| 60 | 57, 58, 59 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ) | 
| 61 | 60 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝐹‘(𝑘 + 1)) ∈ ℕ) | 
| 62 | 54, 61 | pccld 16889 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) ∈
ℕ0) | 
| 63 | 62 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) ∈ ℂ) | 
| 64 | 63 | addlidd 11463 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = (𝑃 pCnt (𝐹‘(𝑘 + 1)))) | 
| 65 | 58 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑘 + 1) ∈ ℕ) | 
| 66 |  | ovex 7465 | . . . . . . . . . . . . . . 15
⊢ (𝑛↑𝐴) ∈ V | 
| 67 | 66, 36 | ifex 4575 | . . . . . . . . . . . . . 14
⊢ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) ∈ V | 
| 68 | 67 | csbex 5310 | . . . . . . . . . . . . 13
⊢
⦋(𝑘 +
1) / 𝑛⦌if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) ∈ V | 
| 69 | 35 | fvmpts 7018 | . . . . . . . . . . . . . 14
⊢ (((𝑘 + 1) ∈ ℕ ∧
⦋(𝑘 + 1) /
𝑛⦌if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) ∈ V) → (𝐹‘(𝑘 + 1)) = ⦋(𝑘 + 1) / 𝑛⦌if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) | 
| 70 |  | ovex 7465 | . . . . . . . . . . . . . . 15
⊢ (𝑘 + 1) ∈ V | 
| 71 |  | nfv 1913 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛(𝑘 + 1) ∈
ℙ | 
| 72 |  | nfcv 2904 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(𝑘 + 1) | 
| 73 |  | nfcv 2904 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛↑ | 
| 74 |  | nfcsb1v 3922 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛⦋(𝑘 + 1) / 𝑛⦌𝐴 | 
| 75 | 72, 73, 74 | nfov 7462 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) | 
| 76 |  | nfcv 2904 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛1 | 
| 77 | 71, 75, 76 | nfif 4555 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) | 
| 78 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → (𝑛 ∈ ℙ ↔ (𝑘 + 1) ∈ ℙ)) | 
| 79 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1)) | 
| 80 |  | csbeq1a 3912 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → 𝐴 = ⦋(𝑘 + 1) / 𝑛⦌𝐴) | 
| 81 | 79, 80 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → (𝑛↑𝐴) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) | 
| 82 | 78, 81 | ifbieq1d 4549 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑘 + 1) → if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) | 
| 83 | 70, 77, 82 | csbief 3932 | . . . . . . . . . . . . . 14
⊢
⦋(𝑘 +
1) / 𝑛⦌if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) | 
| 84 | 69, 83 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (((𝑘 + 1) ∈ ℕ ∧
⦋(𝑘 + 1) /
𝑛⦌if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) ∈ V) → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) | 
| 85 | 65, 68, 84 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) | 
| 86 |  | simprr 772 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑘 + 1) = 𝑃) | 
| 87 | 86, 54 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑘 + 1) ∈ ℙ) | 
| 88 | 87 | iftrued 4532 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) | 
| 89 | 86 | csbeq1d 3902 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ⦋(𝑘 + 1) / 𝑛⦌𝐴 = ⦋𝑃 / 𝑛⦌𝐴) | 
| 90 |  | nfcvd 2905 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ →
Ⅎ𝑛𝐵) | 
| 91 |  | pcmpt.5 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) | 
| 92 | 90, 91 | csbiegf 3931 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ →
⦋𝑃 / 𝑛⦌𝐴 = 𝐵) | 
| 93 | 54, 92 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ⦋𝑃 / 𝑛⦌𝐴 = 𝐵) | 
| 94 | 89, 93 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ⦋(𝑘 + 1) / 𝑛⦌𝐴 = 𝐵) | 
| 95 | 86, 94 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) = (𝑃↑𝐵)) | 
| 96 | 85, 88, 95 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝐹‘(𝑘 + 1)) = (𝑃↑𝐵)) | 
| 97 | 96 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = (𝑃 pCnt (𝑃↑𝐵))) | 
| 98 | 91 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑃 → (𝐴 ∈ ℕ0 ↔ 𝐵 ∈
ℕ0)) | 
| 99 | 98 | rspcv 3617 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ →
(∀𝑛 ∈ ℙ
𝐴 ∈
ℕ0 → 𝐵 ∈
ℕ0)) | 
| 100 | 26, 55, 99 | sylc 65 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℕ0) | 
| 101 | 100 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝐵 ∈
ℕ0) | 
| 102 |  | pcidlem 16911 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℕ0)
→ (𝑃 pCnt (𝑃↑𝐵)) = 𝐵) | 
| 103 | 54, 101, 102 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝑃↑𝐵)) = 𝐵) | 
| 104 | 64, 97, 103 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵) | 
| 105 |  | oveq1 7439 | . . . . . . . . . 10
⊢ ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) | 
| 106 | 105 | eqeq1d 2738 | . . . . . . . . 9
⊢ ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0 → (((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵 ↔ (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵)) | 
| 107 | 104, 106 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵)) | 
| 108 |  | nnre 12274 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) | 
| 109 | 108 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑘 ∈ ℝ) | 
| 110 |  | ltp1 12108 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ → 𝑘 < (𝑘 + 1)) | 
| 111 |  | peano2re 11435 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) | 
| 112 |  | ltnle 11341 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) | 
| 113 | 111, 112 | mpdan 687 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) | 
| 114 | 110, 113 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℝ → ¬
(𝑘 + 1) ≤ 𝑘) | 
| 115 | 109, 114 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ¬ (𝑘 + 1) ≤ 𝑘) | 
| 116 | 86 | breq1d 5152 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑘 + 1) ≤ 𝑘 ↔ 𝑃 ≤ 𝑘)) | 
| 117 | 115, 116 | mtbid 324 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ¬ 𝑃 ≤ 𝑘) | 
| 118 | 117 | iffalsed 4535 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → if(𝑃 ≤ 𝑘, 𝐵, 0) = 0) | 
| 119 | 118 | eqeq2d 2747 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0)) | 
| 120 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) | 
| 121 |  | nnuz 12922 | . . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) | 
| 122 | 120, 121 | eleqtrdi 2850 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) | 
| 123 |  | seqp1 14058 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) | 
| 124 | 122, 123 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘(𝑘 + 1)) = ((seq1( · ,
𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) | 
| 125 | 124 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = (𝑃 pCnt ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))) | 
| 126 | 26 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℙ) | 
| 127 | 56 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ) | 
| 128 | 127 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘𝑘) ∈ ℕ) | 
| 129 |  | nnz 12636 | . . . . . . . . . . . . . 14
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → (seq1(
· , 𝐹)‘𝑘) ∈
ℤ) | 
| 130 |  | nnne0 12301 | . . . . . . . . . . . . . 14
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → (seq1(
· , 𝐹)‘𝑘) ≠ 0) | 
| 131 | 129, 130 | jca 511 | . . . . . . . . . . . . 13
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → ((seq1(
· , 𝐹)‘𝑘) ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑘) ≠ 0)) | 
| 132 | 128, 131 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( · ,
𝐹)‘𝑘) ∈ ℤ ∧ (seq1( · ,
𝐹)‘𝑘) ≠ 0)) | 
| 133 |  | nnz 12636 | . . . . . . . . . . . . . 14
⊢ ((𝐹‘(𝑘 + 1)) ∈ ℕ → (𝐹‘(𝑘 + 1)) ∈ ℤ) | 
| 134 |  | nnne0 12301 | . . . . . . . . . . . . . 14
⊢ ((𝐹‘(𝑘 + 1)) ∈ ℕ → (𝐹‘(𝑘 + 1)) ≠ 0) | 
| 135 | 133, 134 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝐹‘(𝑘 + 1)) ∈ ℕ → ((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ (𝐹‘(𝑘 + 1)) ≠ 0)) | 
| 136 | 60, 135 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ (𝐹‘(𝑘 + 1)) ≠ 0)) | 
| 137 |  | pcmul 16890 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ ((seq1(
· , 𝐹)‘𝑘) ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑘) ≠ 0) ∧ ((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ (𝐹‘(𝑘 + 1)) ≠ 0)) → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) | 
| 138 | 126, 132,
136, 137 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) | 
| 139 | 125, 138 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) | 
| 140 | 139 | adantrr 717 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) | 
| 141 |  | prmnn 16712 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 142 | 26, 141 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 143 | 142 | nnred 12282 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 144 | 143 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ∈ ℝ) | 
| 145 | 144 | leidd 11830 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ≤ 𝑃) | 
| 146 | 145, 86 | breqtrrd 5170 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ≤ (𝑘 + 1)) | 
| 147 | 146 | iftrued 4532 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) = 𝐵) | 
| 148 | 140, 147 | eqeq12d 2752 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) ↔ ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵)) | 
| 149 | 107, 119,
148 | 3imtr4d 294 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) | 
| 150 | 149 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) = 𝑃 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) | 
| 151 | 139 | adantrr 717 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) | 
| 152 |  | simplrr 777 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑘 + 1) ≠ 𝑃) | 
| 153 | 152 | necomd 2995 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → 𝑃 ≠ (𝑘 + 1)) | 
| 154 | 26 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → 𝑃 ∈
ℙ) | 
| 155 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑘 + 1) ∈
ℙ) | 
| 156 | 55 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) | 
| 157 | 74 | nfel1 2921 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛⦋(𝑘 + 1) / 𝑛⦌𝐴 ∈ ℕ0 | 
| 158 | 80 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑘 + 1) → (𝐴 ∈ ℕ0 ↔
⦋(𝑘 + 1) /
𝑛⦌𝐴 ∈
ℕ0)) | 
| 159 | 157, 158 | rspc 3609 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 + 1) ∈ ℙ →
(∀𝑛 ∈ ℙ
𝐴 ∈
ℕ0 → ⦋(𝑘 + 1) / 𝑛⦌𝐴 ∈
ℕ0)) | 
| 160 | 155, 156,
159 | sylc 65 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) →
⦋(𝑘 + 1) /
𝑛⦌𝐴 ∈
ℕ0) | 
| 161 |  | prmdvdsexpr 16755 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ (𝑘 + 1) ∈ ℙ ∧
⦋(𝑘 + 1) /
𝑛⦌𝐴 ∈ ℕ0)
→ (𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) → 𝑃 = (𝑘 + 1))) | 
| 162 | 154, 155,
160, 161 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) → 𝑃 = (𝑘 + 1))) | 
| 163 | 162 | necon3ad 2952 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 ≠ (𝑘 + 1) → ¬ 𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴))) | 
| 164 | 153, 163 | mpd 15 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ¬ 𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) | 
| 165 | 58 | ad2antrl 728 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑘 + 1) ∈ ℕ) | 
| 166 | 165, 68, 84 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) | 
| 167 |  | iftrue 4530 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 + 1) ∈ ℙ →
if((𝑘 + 1) ∈ ℙ,
((𝑘 +
1)↑⦋(𝑘 +
1) / 𝑛⦌𝐴), 1) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) | 
| 168 | 166, 167 | sylan9eq 2796 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) | 
| 169 | 168 | breq2d 5154 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 ∥ (𝐹‘(𝑘 + 1)) ↔ 𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴))) | 
| 170 | 164, 169 | mtbird 325 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ¬ 𝑃 ∥ (𝐹‘(𝑘 + 1))) | 
| 171 | 57 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝐹:ℕ⟶ℕ) | 
| 172 | 171, 165,
59 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝐹‘(𝑘 + 1)) ∈ ℕ) | 
| 173 | 172 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ∈ ℕ) | 
| 174 |  | pceq0 16910 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝐹‘(𝑘 + 1)) ∈ ℕ) → ((𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0 ↔ ¬ 𝑃 ∥ (𝐹‘(𝑘 + 1)))) | 
| 175 | 154, 173,
174 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ((𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0 ↔ ¬ 𝑃 ∥ (𝐹‘(𝑘 + 1)))) | 
| 176 | 170, 175 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0) | 
| 177 |  | iffalse 4533 | . . . . . . . . . . . . . . 15
⊢ (¬
(𝑘 + 1) ∈ ℙ
→ if((𝑘 + 1) ∈
ℙ, ((𝑘 +
1)↑⦋(𝑘 +
1) / 𝑛⦌𝐴), 1) = 1) | 
| 178 | 166, 177 | sylan9eq 2796 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = 1) | 
| 179 | 178 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = (𝑃 pCnt 1)) | 
| 180 | 26, 41 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 pCnt 1) = 0) | 
| 181 | 180 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt 1) = 0) | 
| 182 | 179, 181 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0) | 
| 183 | 176, 182 | pm2.61dan 812 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0) | 
| 184 | 183 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + 0)) | 
| 185 | 26 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝑃 ∈ ℙ) | 
| 186 | 128 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ) | 
| 187 | 185, 186 | pccld 16889 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) ∈
ℕ0) | 
| 188 | 187 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) ∈ ℂ) | 
| 189 | 188 | addridd 11462 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + 0) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑘))) | 
| 190 | 151, 184,
189 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑘))) | 
| 191 | 142 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝑃 ∈ ℕ) | 
| 192 | 191 | nnred 12282 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝑃 ∈ ℝ) | 
| 193 | 165 | nnred 12282 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑘 + 1) ∈ ℝ) | 
| 194 | 192, 193 | ltlend 11407 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 < (𝑘 + 1) ↔ (𝑃 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≠ 𝑃))) | 
| 195 |  | simprl 770 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝑘 ∈ ℕ) | 
| 196 |  | nnleltp1 12675 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑃 ≤ 𝑘 ↔ 𝑃 < (𝑘 + 1))) | 
| 197 | 191, 195,
196 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 ≤ 𝑘 ↔ 𝑃 < (𝑘 + 1))) | 
| 198 |  | simprr 772 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑘 + 1) ≠ 𝑃) | 
| 199 | 198 | biantrud 531 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 ≤ (𝑘 + 1) ↔ (𝑃 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≠ 𝑃))) | 
| 200 | 194, 197,
199 | 3bitr4rd 312 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 ≤ (𝑘 + 1) ↔ 𝑃 ≤ 𝑘)) | 
| 201 | 200 | ifbid 4548 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) = if(𝑃 ≤ 𝑘, 𝐵, 0)) | 
| 202 | 190, 201 | eqeq12d 2752 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0))) | 
| 203 | 202 | biimprd 248 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) | 
| 204 | 203 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) ≠ 𝑃 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) | 
| 205 | 150, 204 | pm2.61dne 3027 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) | 
| 206 | 205 | expcom 413 | . . . 4
⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) | 
| 207 | 206 | a2d 29 | . . 3
⊢ (𝑘 ∈ ℕ → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0)) → (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) | 
| 208 | 7, 13, 19, 25, 53, 207 | nnind 12285 | . 2
⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))) | 
| 209 | 1, 208 | mpcom 38 | 1
⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) |