Step | Hyp | Ref
| Expression |
1 | | pcmpt.3 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | fveq2 5494 |
. . . . . 6
⊢ (𝑝 = 1 → (seq1( · ,
𝐹)‘𝑝) = (seq1( · , 𝐹)‘1)) |
3 | 2 | oveq2d 5867 |
. . . . 5
⊢ (𝑝 = 1 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘1))) |
4 | | breq2 3991 |
. . . . . 6
⊢ (𝑝 = 1 → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ 1)) |
5 | 4 | ifbid 3546 |
. . . . 5
⊢ (𝑝 = 1 → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ 1, 𝐵, 0)) |
6 | 3, 5 | eqeq12d 2185 |
. . . 4
⊢ (𝑝 = 1 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘1)) = if(𝑃 ≤ 1, 𝐵, 0))) |
7 | 6 | imbi2d 229 |
. . 3
⊢ (𝑝 = 1 → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘1)) = if(𝑃 ≤ 1, 𝐵, 0)))) |
8 | | fveq2 5494 |
. . . . . 6
⊢ (𝑝 = 𝑘 → (seq1( · , 𝐹)‘𝑝) = (seq1( · , 𝐹)‘𝑘)) |
9 | 8 | oveq2d 5867 |
. . . . 5
⊢ (𝑝 = 𝑘 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑘))) |
10 | | breq2 3991 |
. . . . . 6
⊢ (𝑝 = 𝑘 → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ 𝑘)) |
11 | 10 | ifbid 3546 |
. . . . 5
⊢ (𝑝 = 𝑘 → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ 𝑘, 𝐵, 0)) |
12 | 9, 11 | eqeq12d 2185 |
. . . 4
⊢ (𝑝 = 𝑘 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0))) |
13 | 12 | imbi2d 229 |
. . 3
⊢ (𝑝 = 𝑘 → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0)))) |
14 | | fveq2 5494 |
. . . . . 6
⊢ (𝑝 = (𝑘 + 1) → (seq1( · , 𝐹)‘𝑝) = (seq1( · , 𝐹)‘(𝑘 + 1))) |
15 | 14 | oveq2d 5867 |
. . . . 5
⊢ (𝑝 = (𝑘 + 1) → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1)))) |
16 | | breq2 3991 |
. . . . . 6
⊢ (𝑝 = (𝑘 + 1) → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ (𝑘 + 1))) |
17 | 16 | ifbid 3546 |
. . . . 5
⊢ (𝑝 = (𝑘 + 1) → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)) |
18 | 15, 17 | eqeq12d 2185 |
. . . 4
⊢ (𝑝 = (𝑘 + 1) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) |
19 | 18 | imbi2d 229 |
. . 3
⊢ (𝑝 = (𝑘 + 1) → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) |
20 | | fveq2 5494 |
. . . . . 6
⊢ (𝑝 = 𝑁 → (seq1( · , 𝐹)‘𝑝) = (seq1( · , 𝐹)‘𝑁)) |
21 | 20 | oveq2d 5867 |
. . . . 5
⊢ (𝑝 = 𝑁 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑁))) |
22 | | breq2 3991 |
. . . . . 6
⊢ (𝑝 = 𝑁 → (𝑃 ≤ 𝑝 ↔ 𝑃 ≤ 𝑁)) |
23 | 22 | ifbid 3546 |
. . . . 5
⊢ (𝑝 = 𝑁 → if(𝑃 ≤ 𝑝, 𝐵, 0) = if(𝑃 ≤ 𝑁, 𝐵, 0)) |
24 | 21, 23 | eqeq12d 2185 |
. . . 4
⊢ (𝑝 = 𝑁 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))) |
25 | 24 | imbi2d 229 |
. . 3
⊢ (𝑝 = 𝑁 → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑝)) = if(𝑃 ≤ 𝑝, 𝐵, 0)) ↔ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)))) |
26 | | pcmpt.4 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℙ) |
27 | | pc1 12252 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) |
28 | 26, 27 | syl 14 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt 1) = 0) |
29 | | 1zzd 9232 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
30 | | elnnuz 9516 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ ↔ 𝑖 ∈
(ℤ≥‘1)) |
31 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
32 | 31 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑖 ∈ ℙ) → 𝑖 ∈ ℕ) |
33 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑖 ∈ ℙ) → 𝑖 ∈ ℙ) |
34 | | pcmpt.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) |
35 | 34 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑖 ∈ ℙ) → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) |
36 | | nfcsb1v 3082 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 |
37 | 36 | nfel1 2323 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 ∈ ℕ0 |
38 | | csbeq1a 3058 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
39 | 38 | eleq1d 2239 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → (𝐴 ∈ ℕ0 ↔
⦋𝑖 / 𝑛⦌𝐴 ∈
ℕ0)) |
40 | 37, 39 | rspc 2828 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℙ →
(∀𝑛 ∈ ℙ
𝐴 ∈
ℕ0 → ⦋𝑖 / 𝑛⦌𝐴 ∈
ℕ0)) |
41 | 33, 35, 40 | sylc 62 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑖 ∈ ℙ) → ⦋𝑖 / 𝑛⦌𝐴 ∈
ℕ0) |
42 | 32, 41 | nnexpcld 10624 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑖 ∈ ℙ) → (𝑖↑⦋𝑖 / 𝑛⦌𝐴) ∈ ℕ) |
43 | | 1nn 8882 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
44 | 43 | a1i 9 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ ¬ 𝑖 ∈ ℙ) → 1 ∈
ℕ) |
45 | | prmdc 12077 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ →
DECID 𝑖
∈ ℙ) |
46 | 45 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → DECID
𝑖 ∈
ℙ) |
47 | 42, 44, 46 | ifcldadc 3554 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → if(𝑖 ∈ ℙ, (𝑖↑⦋𝑖 / 𝑛⦌𝐴), 1) ∈ ℕ) |
48 | | nfcv 2312 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛𝑖 |
49 | 48 | nfel1 2323 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛 𝑖 ∈ ℙ |
50 | | nfcv 2312 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛↑ |
51 | 48, 50, 36 | nfov 5881 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑖↑⦋𝑖 / 𝑛⦌𝐴) |
52 | | nfcv 2312 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛1 |
53 | 49, 51, 52 | nfif 3553 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛if(𝑖 ∈ ℙ, (𝑖↑⦋𝑖 / 𝑛⦌𝐴), 1) |
54 | | eleq1 2233 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑖 → (𝑛 ∈ ℙ ↔ 𝑖 ∈ ℙ)) |
55 | | id 19 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑖 → 𝑛 = 𝑖) |
56 | 55, 38 | oveq12d 5869 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑖 → (𝑛↑𝐴) = (𝑖↑⦋𝑖 / 𝑛⦌𝐴)) |
57 | 54, 56 | ifbieq1d 3547 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) = if(𝑖 ∈ ℙ, (𝑖↑⦋𝑖 / 𝑛⦌𝐴), 1)) |
58 | | pcmpt.1 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) |
59 | 48, 53, 57, 58 | fvmptf 5586 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℕ ∧ if(𝑖 ∈ ℙ, (𝑖↑⦋𝑖 / 𝑛⦌𝐴), 1) ∈ ℕ) → (𝐹‘𝑖) = if(𝑖 ∈ ℙ, (𝑖↑⦋𝑖 / 𝑛⦌𝐴), 1)) |
60 | 31, 47, 59 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = if(𝑖 ∈ ℙ, (𝑖↑⦋𝑖 / 𝑛⦌𝐴), 1)) |
61 | 60, 47 | eqeltrd 2247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℕ) |
62 | 30, 61 | sylan2br 286 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘1))
→ (𝐹‘𝑖) ∈
ℕ) |
63 | | nnmulcl 8892 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑖 · 𝑗) ∈ ℕ) |
64 | 63 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ) |
65 | 29, 62, 64 | seq3-1 10409 |
. . . . . 6
⊢ (𝜑 → (seq1( · , 𝐹)‘1) = (𝐹‘1)) |
66 | | 1nprm 12061 |
. . . . . . . . . 10
⊢ ¬ 1
∈ ℙ |
67 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → (𝑛 ∈ ℙ ↔ 1 ∈
ℙ)) |
68 | 66, 67 | mtbiri 670 |
. . . . . . . . 9
⊢ (𝑛 = 1 → ¬ 𝑛 ∈
ℙ) |
69 | 68 | iffalsed 3535 |
. . . . . . . 8
⊢ (𝑛 = 1 → if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) = 1) |
70 | | 1ex 7908 |
. . . . . . . 8
⊢ 1 ∈
V |
71 | 69, 58, 70 | fvmpt 5571 |
. . . . . . 7
⊢ (1 ∈
ℕ → (𝐹‘1)
= 1) |
72 | 43, 71 | ax-mp 5 |
. . . . . 6
⊢ (𝐹‘1) = 1 |
73 | 65, 72 | eqtrdi 2219 |
. . . . 5
⊢ (𝜑 → (seq1( · , 𝐹)‘1) = 1) |
74 | 73 | oveq2d 5867 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘1)) = (𝑃 pCnt 1)) |
75 | | prmgt1 12079 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
76 | | 1z 9231 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
77 | | prmz 12058 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
78 | | zltnle 9251 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ 𝑃
∈ ℤ) → (1 < 𝑃 ↔ ¬ 𝑃 ≤ 1)) |
79 | 76, 77, 78 | sylancr 412 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → (1 <
𝑃 ↔ ¬ 𝑃 ≤ 1)) |
80 | 75, 79 | mpbid 146 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ≤ 1) |
81 | 80 | iffalsed 3535 |
. . . . 5
⊢ (𝑃 ∈ ℙ → if(𝑃 ≤ 1, 𝐵, 0) = 0) |
82 | 26, 81 | syl 14 |
. . . 4
⊢ (𝜑 → if(𝑃 ≤ 1, 𝐵, 0) = 0) |
83 | 28, 74, 82 | 3eqtr4d 2213 |
. . 3
⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘1)) = if(𝑃 ≤ 1, 𝐵, 0)) |
84 | 26 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ∈ ℙ) |
85 | 58, 34 | pcmptcl 12287 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( ·
, 𝐹):ℕ⟶ℕ)) |
86 | 85 | simpld 111 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℕ⟶ℕ) |
87 | | peano2nn 8883 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
88 | | ffvelrn 5627 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶ℕ ∧
(𝑘 + 1) ∈ ℕ)
→ (𝐹‘(𝑘 + 1)) ∈
ℕ) |
89 | 86, 87, 88 | syl2an 287 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ) |
90 | 89 | adantrr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝐹‘(𝑘 + 1)) ∈ ℕ) |
91 | 84, 90 | pccld 12247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) ∈
ℕ0) |
92 | 91 | nn0cnd 9183 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) ∈ ℂ) |
93 | 92 | addid2d 8062 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = (𝑃 pCnt (𝐹‘(𝑘 + 1)))) |
94 | 87 | ad2antrl 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑘 + 1) ∈ ℕ) |
95 | 87 | ad2antlr 486 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝑘 + 1) ∈
ℕ) |
96 | | simpr 109 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝑘 + 1) ∈
ℙ) |
97 | 34 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) |
98 | | nfcsb1v 3082 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛⦋(𝑘 + 1) / 𝑛⦌𝐴 |
99 | 98 | nfel1 2323 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛⦋(𝑘 + 1) / 𝑛⦌𝐴 ∈ ℕ0 |
100 | | csbeq1a 3058 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑘 + 1) → 𝐴 = ⦋(𝑘 + 1) / 𝑛⦌𝐴) |
101 | 100 | eleq1d 2239 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑘 + 1) → (𝐴 ∈ ℕ0 ↔
⦋(𝑘 + 1) /
𝑛⦌𝐴 ∈
ℕ0)) |
102 | 99, 101 | rspc 2828 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ ℙ →
(∀𝑛 ∈ ℙ
𝐴 ∈
ℕ0 → ⦋(𝑘 + 1) / 𝑛⦌𝐴 ∈
ℕ0)) |
103 | 96, 97, 102 | sylc 62 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) →
⦋(𝑘 + 1) /
𝑛⦌𝐴 ∈
ℕ0) |
104 | 95, 103 | nnexpcld 10624 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) ∈ ℕ) |
105 | 43 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → 1
∈ ℕ) |
106 | 87 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
107 | | prmdc 12077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 + 1) ∈ ℕ →
DECID (𝑘 +
1) ∈ ℙ) |
108 | 106, 107 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → DECID
(𝑘 + 1) ∈
ℙ) |
109 | 104, 105,
108 | ifcldadc 3554 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) ∈ ℕ) |
110 | 109 | adantrr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) ∈ ℕ) |
111 | | nfcv 2312 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝑘 + 1) |
112 | | nfv 1521 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝑘 + 1) ∈
ℙ |
113 | 111, 50, 98 | nfov 5881 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) |
114 | 112, 113,
52 | nfif 3553 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) |
115 | | eleq1 2233 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑘 + 1) → (𝑛 ∈ ℙ ↔ (𝑘 + 1) ∈ ℙ)) |
116 | | id 19 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1)) |
117 | 116, 100 | oveq12d 5869 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑘 + 1) → (𝑛↑𝐴) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) |
118 | 115, 117 | ifbieq1d 3547 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑘 + 1) → if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) |
119 | 111, 114,
118, 58 | fvmptf 5586 |
. . . . . . . . . . . . 13
⊢ (((𝑘 + 1) ∈ ℕ ∧
if((𝑘 + 1) ∈ ℙ,
((𝑘 +
1)↑⦋(𝑘 +
1) / 𝑛⦌𝐴), 1) ∈ ℕ) →
(𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) |
120 | 94, 110, 119 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) |
121 | | simprr 527 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑘 + 1) = 𝑃) |
122 | 121, 84 | eqeltrd 2247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑘 + 1) ∈ ℙ) |
123 | 122 | iftrued 3532 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) |
124 | 121 | csbeq1d 3056 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ⦋(𝑘 + 1) / 𝑛⦌𝐴 = ⦋𝑃 / 𝑛⦌𝐴) |
125 | | nfcvd 2313 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ →
Ⅎ𝑛𝐵) |
126 | | pcmpt.5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) |
127 | 125, 126 | csbiegf 3092 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ →
⦋𝑃 / 𝑛⦌𝐴 = 𝐵) |
128 | 84, 127 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ⦋𝑃 / 𝑛⦌𝐴 = 𝐵) |
129 | 124, 128 | eqtrd 2203 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ⦋(𝑘 + 1) / 𝑛⦌𝐴 = 𝐵) |
130 | 121, 129 | oveq12d 5869 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) = (𝑃↑𝐵)) |
131 | 120, 123,
130 | 3eqtrd 2207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝐹‘(𝑘 + 1)) = (𝑃↑𝐵)) |
132 | 131 | oveq2d 5867 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = (𝑃 pCnt (𝑃↑𝐵))) |
133 | 126 | eleq1d 2239 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑃 → (𝐴 ∈ ℕ0 ↔ 𝐵 ∈
ℕ0)) |
134 | 133 | rspcv 2830 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ →
(∀𝑛 ∈ ℙ
𝐴 ∈
ℕ0 → 𝐵 ∈
ℕ0)) |
135 | 26, 34, 134 | sylc 62 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
136 | 135 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝐵 ∈
ℕ0) |
137 | | pcidlem 12269 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℕ0)
→ (𝑃 pCnt (𝑃↑𝐵)) = 𝐵) |
138 | 26, 136, 137 | syl2an2r 590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (𝑃↑𝐵)) = 𝐵) |
139 | 93, 132, 138 | 3eqtrd 2207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵) |
140 | | oveq1 5858 |
. . . . . . . . . 10
⊢ ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) |
141 | 140 | eqeq1d 2179 |
. . . . . . . . 9
⊢ ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0 → (((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵 ↔ (0 + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵)) |
142 | 139, 141 | syl5ibrcom 156 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵)) |
143 | | nnre 8878 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
144 | 143 | ltp1d 8839 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 < (𝑘 + 1)) |
145 | | nnz 9224 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
146 | 87 | nnzd 9326 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℤ) |
147 | | zltnle 9251 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 + 1) ∈ ℤ) →
(𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
148 | 145, 146,
147 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
149 | 144, 148 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → ¬
(𝑘 + 1) ≤ 𝑘) |
150 | 149 | ad2antrl 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ¬ (𝑘 + 1) ≤ 𝑘) |
151 | 121 | breq1d 3997 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑘 + 1) ≤ 𝑘 ↔ 𝑃 ≤ 𝑘)) |
152 | 150, 151 | mtbid 667 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ¬ 𝑃 ≤ 𝑘) |
153 | 152 | iffalsed 3535 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → if(𝑃 ≤ 𝑘, 𝐵, 0) = 0) |
154 | 153 | eqeq2d 2182 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = 0)) |
155 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
156 | | nnuz 9515 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
157 | 155, 156 | eleqtrdi 2263 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
158 | 62 | adantlr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 ∈ (ℤ≥‘1))
→ (𝐹‘𝑖) ∈
ℕ) |
159 | 63 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 · 𝑗) ∈ ℕ) |
160 | 157, 158,
159 | seq3p1 10411 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘(𝑘 + 1)) = ((seq1( · ,
𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) |
161 | 160 | oveq2d 5867 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = (𝑃 pCnt ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))))) |
162 | 26 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℙ) |
163 | 85 | simprd 113 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ) |
164 | 163 | ffvelrnda 5629 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘𝑘) ∈ ℕ) |
165 | | nnz 9224 |
. . . . . . . . . . . . . 14
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → (seq1(
· , 𝐹)‘𝑘) ∈
ℤ) |
166 | | nnne0 8899 |
. . . . . . . . . . . . . 14
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → (seq1(
· , 𝐹)‘𝑘) ≠ 0) |
167 | 165, 166 | jca 304 |
. . . . . . . . . . . . 13
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → ((seq1(
· , 𝐹)‘𝑘) ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑘) ≠ 0)) |
168 | 164, 167 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( · ,
𝐹)‘𝑘) ∈ ℤ ∧ (seq1( · ,
𝐹)‘𝑘) ≠ 0)) |
169 | | nnz 9224 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘(𝑘 + 1)) ∈ ℕ → (𝐹‘(𝑘 + 1)) ∈ ℤ) |
170 | | nnne0 8899 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘(𝑘 + 1)) ∈ ℕ → (𝐹‘(𝑘 + 1)) ≠ 0) |
171 | 169, 170 | jca 304 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘(𝑘 + 1)) ∈ ℕ → ((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ (𝐹‘(𝑘 + 1)) ≠ 0)) |
172 | 89, 171 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ (𝐹‘(𝑘 + 1)) ≠ 0)) |
173 | | pcmul 12248 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ ((seq1(
· , 𝐹)‘𝑘) ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑘) ≠ 0) ∧ ((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ (𝐹‘(𝑘 + 1)) ≠ 0)) → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) |
174 | 162, 168,
172, 173 | syl3anc 1233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) |
175 | 161, 174 | eqtrd 2203 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) |
176 | 175 | adantrr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) |
177 | | prmnn 12057 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
178 | 26, 177 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) |
179 | 178 | nnred 8884 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℝ) |
180 | 179 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ∈ ℝ) |
181 | 180 | leidd 8426 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ≤ 𝑃) |
182 | 181, 121 | breqtrrd 4015 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → 𝑃 ≤ (𝑘 + 1)) |
183 | 182 | iftrued 3532 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) = 𝐵) |
184 | 176, 183 | eqeq12d 2185 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) ↔ ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = 𝐵)) |
185 | 142, 154,
184 | 3imtr4d 202 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) = 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) |
186 | 185 | expr 373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) = 𝑃 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) |
187 | 175 | adantrr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1))))) |
188 | | simplrr 531 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑘 + 1) ≠ 𝑃) |
189 | 188 | necomd 2426 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → 𝑃 ≠ (𝑘 + 1)) |
190 | 26 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → 𝑃 ∈
ℙ) |
191 | | simpr 109 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑘 + 1) ∈
ℙ) |
192 | 34 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) |
193 | 191, 192,
102 | sylc 62 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) →
⦋(𝑘 + 1) /
𝑛⦌𝐴 ∈
ℕ0) |
194 | | prmdvdsexpr 12097 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ (𝑘 + 1) ∈ ℙ ∧
⦋(𝑘 + 1) /
𝑛⦌𝐴 ∈ ℕ0)
→ (𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) → 𝑃 = (𝑘 + 1))) |
195 | 190, 191,
193, 194 | syl3anc 1233 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴) → 𝑃 = (𝑘 + 1))) |
196 | 195 | necon3ad 2382 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 ≠ (𝑘 + 1) → ¬ 𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴))) |
197 | 189, 196 | mpd 13 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ¬ 𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) |
198 | 87 | ad2antrl 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑘 + 1) ∈ ℕ) |
199 | 109 | adantrr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1) ∈ ℕ) |
200 | 198, 199,
119 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴), 1)) |
201 | | iftrue 3530 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 + 1) ∈ ℙ →
if((𝑘 + 1) ∈ ℙ,
((𝑘 +
1)↑⦋(𝑘 +
1) / 𝑛⦌𝐴), 1) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) |
202 | 200, 201 | sylan9eq 2223 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴)) |
203 | 202 | breq2d 3999 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 ∥ (𝐹‘(𝑘 + 1)) ↔ 𝑃 ∥ ((𝑘 + 1)↑⦋(𝑘 + 1) / 𝑛⦌𝐴))) |
204 | 197, 203 | mtbird 668 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ¬ 𝑃 ∥ (𝐹‘(𝑘 + 1))) |
205 | 86, 198, 88 | syl2an2r 590 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝐹‘(𝑘 + 1)) ∈ ℕ) |
206 | 205 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ∈ ℕ) |
207 | | pceq0 12268 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝐹‘(𝑘 + 1)) ∈ ℕ) → ((𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0 ↔ ¬ 𝑃 ∥ (𝐹‘(𝑘 + 1)))) |
208 | 190, 206,
207 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → ((𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0 ↔ ¬ 𝑃 ∥ (𝐹‘(𝑘 + 1)))) |
209 | 204, 208 | mpbird 166 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0) |
210 | | iffalse 3533 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝑘 + 1) ∈ ℙ
→ if((𝑘 + 1) ∈
ℙ, ((𝑘 +
1)↑⦋(𝑘 +
1) / 𝑛⦌𝐴), 1) = 1) |
211 | 200, 210 | sylan9eq 2223 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = 1) |
212 | 211 | oveq2d 5867 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = (𝑃 pCnt 1)) |
213 | 28 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt 1) = 0) |
214 | 212, 213 | eqtrd 2203 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) ∧ ¬ (𝑘 + 1) ∈ ℙ) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0) |
215 | | exmiddc 831 |
. . . . . . . . . . . . 13
⊢
(DECID (𝑘 + 1) ∈ ℙ → ((𝑘 + 1) ∈ ℙ ∨ ¬
(𝑘 + 1) ∈
ℙ)) |
216 | 198, 107,
215 | 3syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑘 + 1) ∈ ℙ ∨ ¬ (𝑘 + 1) ∈
ℙ)) |
217 | 209, 214,
216 | mpjaodan 793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (𝐹‘(𝑘 + 1))) = 0) |
218 | 217 | oveq2d 5867 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + (𝑃 pCnt (𝐹‘(𝑘 + 1)))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + 0)) |
219 | 26 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝑃 ∈ ℙ) |
220 | 164 | adantrr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (seq1( · , 𝐹)‘𝑘) ∈ ℕ) |
221 | 219, 220 | pccld 12247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) ∈
ℕ0) |
222 | 221 | nn0cnd 9183 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) ∈ ℂ) |
223 | 222 | addid1d 8061 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) + 0) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑘))) |
224 | 187, 218,
223 | 3eqtrd 2207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = (𝑃 pCnt (seq1( · , 𝐹)‘𝑘))) |
225 | 219, 77 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝑃 ∈ ℤ) |
226 | 146 | ad2antrl 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑘 + 1) ∈ ℤ) |
227 | | zltlen 9283 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℤ ∧ (𝑘 + 1) ∈ ℤ) →
(𝑃 < (𝑘 + 1) ↔ (𝑃 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≠ 𝑃))) |
228 | 225, 226,
227 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 < (𝑘 + 1) ↔ (𝑃 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≠ 𝑃))) |
229 | | simprl 526 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → 𝑘 ∈ ℕ) |
230 | | nnleltp1 9264 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑃 ≤ 𝑘 ↔ 𝑃 < (𝑘 + 1))) |
231 | 178, 229,
230 | syl2an2r 590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 ≤ 𝑘 ↔ 𝑃 < (𝑘 + 1))) |
232 | | simprr 527 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑘 + 1) ≠ 𝑃) |
233 | 232 | biantrud 302 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 ≤ (𝑘 + 1) ↔ (𝑃 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≠ 𝑃))) |
234 | 228, 231,
233 | 3bitr4rd 220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → (𝑃 ≤ (𝑘 + 1) ↔ 𝑃 ≤ 𝑘)) |
235 | 234 | ifbid 3546 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) = if(𝑃 ≤ 𝑘, 𝐵, 0)) |
236 | 224, 235 | eqeq12d 2185 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0) ↔ (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0))) |
237 | 236 | biimprd 157 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑘 + 1) ≠ 𝑃)) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) |
238 | 237 | expr 373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) ≠ 𝑃 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) |
239 | 106 | nnzd 9326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ) |
240 | 162, 77 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℤ) |
241 | | zdceq 9280 |
. . . . . . . 8
⊢ (((𝑘 + 1) ∈ ℤ ∧ 𝑃 ∈ ℤ) →
DECID (𝑘 +
1) = 𝑃) |
242 | 239, 240,
241 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → DECID
(𝑘 + 1) = 𝑃) |
243 | | dcne 2351 |
. . . . . . 7
⊢
(DECID (𝑘 + 1) = 𝑃 ↔ ((𝑘 + 1) = 𝑃 ∨ (𝑘 + 1) ≠ 𝑃)) |
244 | 242, 243 | sylib 121 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) = 𝑃 ∨ (𝑘 + 1) ≠ 𝑃)) |
245 | 186, 238,
244 | mpjaod 713 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0))) |
246 | 245 | expcom 115 |
. . . 4
⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0) → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) |
247 | 246 | a2d 26 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑘)) = if(𝑃 ≤ 𝑘, 𝐵, 0)) → (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘(𝑘 + 1))) = if(𝑃 ≤ (𝑘 + 1), 𝐵, 0)))) |
248 | 7, 13, 19, 25, 83, 247 | nnind 8887 |
. 2
⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))) |
249 | 1, 248 | mpcom 36 |
1
⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) |