Step | Hyp | Ref
| Expression |
1 | | mulid1 7906 |
. . 3
⊢ (𝑘 ∈ ℂ → (𝑘 · 1) = 𝑘) |
2 | 1 | adantl 275 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℂ) → (𝑘 · 1) = 𝑘) |
3 | | lgsdilem2.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | lgsdilem2.4 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ 0) |
5 | | nnabscl 11053 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) |
6 | 3, 4, 5 | syl2anc 409 |
. . 3
⊢ (𝜑 → (abs‘𝑀) ∈
ℕ) |
7 | | nnuz 9511 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
8 | 6, 7 | eleqtrdi 2263 |
. 2
⊢ (𝜑 → (abs‘𝑀) ∈
(ℤ≥‘1)) |
9 | 6 | nnzd 9322 |
. . 3
⊢ (𝜑 → (abs‘𝑀) ∈
ℤ) |
10 | | lgsdilem2.3 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | 3, 10 | zmulcld 9329 |
. . . . 5
⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℤ) |
12 | 3 | zcnd 9324 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
13 | 10 | zcnd 9324 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
14 | | 0z 9212 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
15 | | zapne 9275 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑀 # 0
↔ 𝑀 ≠
0)) |
16 | 3, 14, 15 | sylancl 411 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 # 0 ↔ 𝑀 ≠ 0)) |
17 | 4, 16 | mpbird 166 |
. . . . . . 7
⊢ (𝜑 → 𝑀 # 0) |
18 | | lgsdilem2.5 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ≠ 0) |
19 | | zapne 9275 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑁 # 0
↔ 𝑁 ≠
0)) |
20 | 10, 14, 19 | sylancl 411 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 # 0 ↔ 𝑁 ≠ 0)) |
21 | 18, 20 | mpbird 166 |
. . . . . . 7
⊢ (𝜑 → 𝑁 # 0) |
22 | 12, 13, 17, 21 | mulap0d 8565 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑁) # 0) |
23 | | zapne 9275 |
. . . . . . 7
⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑀 · 𝑁) # 0 ↔ (𝑀 · 𝑁) ≠ 0)) |
24 | 11, 14, 23 | sylancl 411 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑁) # 0 ↔ (𝑀 · 𝑁) ≠ 0)) |
25 | 22, 24 | mpbid 146 |
. . . . 5
⊢ (𝜑 → (𝑀 · 𝑁) ≠ 0) |
26 | | nnabscl 11053 |
. . . . 5
⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
27 | 11, 25, 26 | syl2anc 409 |
. . . 4
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
28 | 27 | nnzd 9322 |
. . 3
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈ ℤ) |
29 | 12 | abscld 11134 |
. . . . 5
⊢ (𝜑 → (abs‘𝑀) ∈
ℝ) |
30 | 13 | abscld 11134 |
. . . . 5
⊢ (𝜑 → (abs‘𝑁) ∈
ℝ) |
31 | 12 | absge0d 11137 |
. . . . 5
⊢ (𝜑 → 0 ≤ (abs‘𝑀)) |
32 | | nnabscl 11053 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
33 | 10, 18, 32 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (abs‘𝑁) ∈
ℕ) |
34 | 33 | nnge1d 8910 |
. . . . 5
⊢ (𝜑 → 1 ≤ (abs‘𝑁)) |
35 | 29, 30, 31, 34 | lemulge11d 8842 |
. . . 4
⊢ (𝜑 → (abs‘𝑀) ≤ ((abs‘𝑀) · (abs‘𝑁))) |
36 | 12, 13 | absmuld 11147 |
. . . 4
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) = ((abs‘𝑀) · (abs‘𝑁))) |
37 | 35, 36 | breqtrrd 4015 |
. . 3
⊢ (𝜑 → (abs‘𝑀) ≤ (abs‘(𝑀 · 𝑁))) |
38 | | eluz2 9482 |
. . 3
⊢
((abs‘(𝑀
· 𝑁)) ∈
(ℤ≥‘(abs‘𝑀)) ↔ ((abs‘𝑀) ∈ ℤ ∧ (abs‘(𝑀 · 𝑁)) ∈ ℤ ∧ (abs‘𝑀) ≤ (abs‘(𝑀 · 𝑁)))) |
39 | 9, 28, 37, 38 | syl3anbrc 1176 |
. 2
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈
(ℤ≥‘(abs‘𝑀))) |
40 | | 1zzd 9228 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
41 | | lgsdilem2.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℤ) |
42 | | lgsdilem2.6 |
. . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) |
43 | 42 | lgsfcl3 13677 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → 𝐹:ℕ⟶ℤ) |
44 | 41, 3, 4, 43 | syl3anc 1233 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶ℤ) |
45 | 44 | ffvelrnda 5629 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℤ) |
46 | | zmulcl 9254 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ) |
47 | 46 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ) |
48 | 7, 40, 45, 47 | seqf 10406 |
. . . 4
⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℤ) |
49 | 48, 6 | ffvelrnd 5630 |
. . 3
⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) ∈
ℤ) |
50 | 49 | zcnd 9324 |
. 2
⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) ∈
ℂ) |
51 | | eleq1w 2231 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
52 | | oveq2 5859 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘)) |
53 | | oveq1 5858 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑀) = (𝑘 pCnt 𝑀)) |
54 | 52, 53 | oveq12d 5869 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀))) |
55 | 51, 54 | ifbieq1d 3547 |
. . . 4
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
56 | 6 | peano2nnd 8882 |
. . . . 5
⊢ (𝜑 → ((abs‘𝑀) + 1) ∈
ℕ) |
57 | | elfzuz 9966 |
. . . . 5
⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈
(ℤ≥‘((abs‘𝑀) + 1))) |
58 | | eluznn 9548 |
. . . . 5
⊢
((((abs‘𝑀) +
1) ∈ ℕ ∧ 𝑘
∈ (ℤ≥‘((abs‘𝑀) + 1))) → 𝑘 ∈ ℕ) |
59 | 56, 57, 58 | syl2an 287 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℕ) |
60 | 41 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ) |
61 | | prmz 12054 |
. . . . . . . 8
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℤ) |
62 | 61 | adantl 275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ) |
63 | | lgscl 13670 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈
ℤ) |
64 | 60, 62, 63 | syl2anc 409 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℤ) |
65 | | simpr 109 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ) |
66 | 3 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈ ℤ) |
67 | 4 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ≠ 0) |
68 | | pczcl 12241 |
. . . . . . 7
⊢ ((𝑘 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝑘 pCnt 𝑀) ∈
ℕ0) |
69 | 65, 66, 67, 68 | syl12anc 1231 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑀) ∈
ℕ0) |
70 | | zexpcl 10480 |
. . . . . 6
⊢ (((𝐴 /L 𝑘) ∈ ℤ ∧ (𝑘 pCnt 𝑀) ∈ ℕ0) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ ℤ) |
71 | 64, 69, 70 | syl2anc 409 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ ℤ) |
72 | | 1zzd 9228 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈
ℤ) |
73 | | prmdc 12073 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
DECID 𝑘
∈ ℙ) |
74 | 59, 73 | syl 14 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → DECID 𝑘 ∈
ℙ) |
75 | 71, 72, 74 | ifcldadc 3554 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) ∈ ℤ) |
76 | 42, 55, 59, 75 | fvmptd3 5587 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
77 | | zq 9574 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℚ) |
78 | 66, 77 | syl 14 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈ ℚ) |
79 | | pcabs 12268 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℙ ∧ 𝑀 ∈ ℚ) → (𝑘 pCnt (abs‘𝑀)) = (𝑘 pCnt 𝑀)) |
80 | 65, 78, 79 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑀)) = (𝑘 pCnt 𝑀)) |
81 | | elfzle1 9972 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → ((abs‘𝑀) + 1) ≤ 𝑘) |
82 | 81 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) + 1) ≤ 𝑘) |
83 | | elfzelz 9970 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈ ℤ) |
84 | | zltp1le 9255 |
. . . . . . . . . . . . . 14
⊢
(((abs‘𝑀)
∈ ℤ ∧ 𝑘
∈ ℤ) → ((abs‘𝑀) < 𝑘 ↔ ((abs‘𝑀) + 1) ≤ 𝑘)) |
85 | 9, 83, 84 | syl2an 287 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) < 𝑘 ↔ ((abs‘𝑀) + 1) ≤ 𝑘)) |
86 | 82, 85 | mpbird 166 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (abs‘𝑀) < 𝑘) |
87 | | zltnle 9247 |
. . . . . . . . . . . . 13
⊢
(((abs‘𝑀)
∈ ℤ ∧ 𝑘
∈ ℤ) → ((abs‘𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ (abs‘𝑀))) |
88 | 9, 83, 87 | syl2an 287 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ (abs‘𝑀))) |
89 | 86, 88 | mpbid 146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ¬ 𝑘 ≤ (abs‘𝑀)) |
90 | 89 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ≤ (abs‘𝑀)) |
91 | 66, 67, 5 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (abs‘𝑀) ∈
ℕ) |
92 | | dvdsle 11793 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧
(abs‘𝑀) ∈
ℕ) → (𝑘 ∥
(abs‘𝑀) → 𝑘 ≤ (abs‘𝑀))) |
93 | 62, 91, 92 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ (abs‘𝑀) → 𝑘 ≤ (abs‘𝑀))) |
94 | 90, 93 | mtod 658 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ (abs‘𝑀)) |
95 | | pceq0 12264 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℙ ∧
(abs‘𝑀) ∈
ℕ) → ((𝑘 pCnt
(abs‘𝑀)) = 0 ↔
¬ 𝑘 ∥
(abs‘𝑀))) |
96 | 65, 91, 95 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑀)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑀))) |
97 | 94, 96 | mpbird 166 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑀)) = 0) |
98 | 80, 97 | eqtr3d 2205 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑀) = 0) |
99 | 98 | oveq2d 5867 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑0)) |
100 | 64 | zcnd 9324 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℂ) |
101 | 100 | exp0d 10592 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑0) = 1) |
102 | 99, 101 | eqtrd 2203 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) = 1) |
103 | 102, 74 | ifeq1dadc 3555 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, 1, 1)) |
104 | | ifiddc 3558 |
. . . . 5
⊢
(DECID 𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, 1, 1) = 1) |
105 | 74, 104 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, 1, 1) = 1) |
106 | 103, 105 | eqtrd 2203 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = 1) |
107 | 76, 106 | eqtrd 2203 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (𝐹‘𝑘) = 1) |
108 | 44 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝐹:ℕ⟶ℤ) |
109 | | elnnuz 9512 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
110 | 109 | biimpri 132 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘1) → 𝑘 ∈ ℕ) |
111 | 110 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝑘 ∈
ℕ) |
112 | 108, 111 | ffvelrnd 5630 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (𝐹‘𝑘) ∈
ℤ) |
113 | 112 | zcnd 9324 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (𝐹‘𝑘) ∈
ℂ) |
114 | | mulcl 7890 |
. . 3
⊢ ((𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑘 · 𝑣) ∈ ℂ) |
115 | 114 | adantl 275 |
. 2
⊢ ((𝜑 ∧ (𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑘 · 𝑣) ∈ ℂ) |
116 | 2, 8, 39, 50, 107, 113, 115 | seq3id2 10454 |
1
⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁)))) |