| Step | Hyp | Ref
| Expression |
| 1 | | mulrid 11259 |
. . 3
⊢ (𝑘 ∈ ℂ → (𝑘 · 1) = 𝑘) |
| 2 | 1 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℂ) → (𝑘 · 1) = 𝑘) |
| 3 | | lgsdilem2.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 4 | | lgsdilem2.4 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ 0) |
| 5 | | nnabscl 15364 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) |
| 6 | 3, 4, 5 | syl2anc 584 |
. . 3
⊢ (𝜑 → (abs‘𝑀) ∈
ℕ) |
| 7 | | nnuz 12921 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
| 8 | 6, 7 | eleqtrdi 2851 |
. 2
⊢ (𝜑 → (abs‘𝑀) ∈
(ℤ≥‘1)) |
| 9 | 6 | nnzd 12640 |
. . 3
⊢ (𝜑 → (abs‘𝑀) ∈
ℤ) |
| 10 | | lgsdilem2.3 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 11 | 3, 10 | zmulcld 12728 |
. . . . 5
⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℤ) |
| 12 | 3 | zcnd 12723 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 13 | 10 | zcnd 12723 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 14 | | lgsdilem2.5 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) |
| 15 | 12, 13, 4, 14 | mulne0d 11915 |
. . . . 5
⊢ (𝜑 → (𝑀 · 𝑁) ≠ 0) |
| 16 | | nnabscl 15364 |
. . . . 5
⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
| 17 | 11, 15, 16 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
| 18 | 17 | nnzd 12640 |
. . 3
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈ ℤ) |
| 19 | 12 | abscld 15475 |
. . . . 5
⊢ (𝜑 → (abs‘𝑀) ∈
ℝ) |
| 20 | 13 | abscld 15475 |
. . . . 5
⊢ (𝜑 → (abs‘𝑁) ∈
ℝ) |
| 21 | 12 | absge0d 15483 |
. . . . 5
⊢ (𝜑 → 0 ≤ (abs‘𝑀)) |
| 22 | | nnabscl 15364 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
| 23 | 10, 14, 22 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (abs‘𝑁) ∈
ℕ) |
| 24 | 23 | nnge1d 12314 |
. . . . 5
⊢ (𝜑 → 1 ≤ (abs‘𝑁)) |
| 25 | 19, 20, 21, 24 | lemulge11d 12205 |
. . . 4
⊢ (𝜑 → (abs‘𝑀) ≤ ((abs‘𝑀) · (abs‘𝑁))) |
| 26 | 12, 13 | absmuld 15493 |
. . . 4
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) = ((abs‘𝑀) · (abs‘𝑁))) |
| 27 | 25, 26 | breqtrrd 5171 |
. . 3
⊢ (𝜑 → (abs‘𝑀) ≤ (abs‘(𝑀 · 𝑁))) |
| 28 | | eluz2 12884 |
. . 3
⊢
((abs‘(𝑀
· 𝑁)) ∈
(ℤ≥‘(abs‘𝑀)) ↔ ((abs‘𝑀) ∈ ℤ ∧ (abs‘(𝑀 · 𝑁)) ∈ ℤ ∧ (abs‘𝑀) ≤ (abs‘(𝑀 · 𝑁)))) |
| 29 | 9, 18, 27, 28 | syl3anbrc 1344 |
. 2
⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈
(ℤ≥‘(abs‘𝑀))) |
| 30 | | lgsdilem2.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 31 | | lgsdilem2.6 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) |
| 32 | 31 | lgsfcl3 27362 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → 𝐹:ℕ⟶ℤ) |
| 33 | 30, 3, 4, 32 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → 𝐹:ℕ⟶ℤ) |
| 34 | | elfznn 13593 |
. . . . 5
⊢ (𝑘 ∈ (1...(abs‘𝑀)) → 𝑘 ∈ ℕ) |
| 35 | | ffvelcdm 7101 |
. . . . 5
⊢ ((𝐹:ℕ⟶ℤ ∧
𝑘 ∈ ℕ) →
(𝐹‘𝑘) ∈ ℤ) |
| 36 | 33, 34, 35 | syl2an 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(abs‘𝑀))) → (𝐹‘𝑘) ∈ ℤ) |
| 37 | 36 | zcnd 12723 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(abs‘𝑀))) → (𝐹‘𝑘) ∈ ℂ) |
| 38 | | mulcl 11239 |
. . . 4
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
| 39 | 38 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
| 40 | 8, 37, 39 | seqcl 14063 |
. 2
⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) ∈
ℂ) |
| 41 | 6 | peano2nnd 12283 |
. . . . 5
⊢ (𝜑 → ((abs‘𝑀) + 1) ∈
ℕ) |
| 42 | | elfzuz 13560 |
. . . . 5
⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈
(ℤ≥‘((abs‘𝑀) + 1))) |
| 43 | | eluznn 12960 |
. . . . 5
⊢
((((abs‘𝑀) +
1) ∈ ℕ ∧ 𝑘
∈ (ℤ≥‘((abs‘𝑀) + 1))) → 𝑘 ∈ ℕ) |
| 44 | 41, 42, 43 | syl2an 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℕ) |
| 45 | | eleq1w 2824 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
| 46 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘)) |
| 47 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑀) = (𝑘 pCnt 𝑀)) |
| 48 | 46, 47 | oveq12d 7449 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀))) |
| 49 | 45, 48 | ifbieq1d 4550 |
. . . . 5
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
| 50 | | ovex 7464 |
. . . . . 6
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ V |
| 51 | | 1ex 11257 |
. . . . . 6
⊢ 1 ∈
V |
| 52 | 50, 51 | ifex 4576 |
. . . . 5
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) ∈ V |
| 53 | 49, 31, 52 | fvmpt 7016 |
. . . 4
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
| 54 | 44, 53 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
| 55 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ) |
| 56 | 3 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈ ℤ) |
| 57 | | zq 12996 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℚ) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈ ℚ) |
| 59 | | pcabs 16913 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℙ ∧ 𝑀 ∈ ℚ) → (𝑘 pCnt (abs‘𝑀)) = (𝑘 pCnt 𝑀)) |
| 60 | 55, 58, 59 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑀)) = (𝑘 pCnt 𝑀)) |
| 61 | | elfzle1 13567 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → ((abs‘𝑀) + 1) ≤ 𝑘) |
| 62 | 61 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) + 1) ≤ 𝑘) |
| 63 | | elfzelz 13564 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈ ℤ) |
| 64 | | zltp1le 12667 |
. . . . . . . . . . . . . 14
⊢
(((abs‘𝑀)
∈ ℤ ∧ 𝑘
∈ ℤ) → ((abs‘𝑀) < 𝑘 ↔ ((abs‘𝑀) + 1) ≤ 𝑘)) |
| 65 | 9, 63, 64 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) < 𝑘 ↔ ((abs‘𝑀) + 1) ≤ 𝑘)) |
| 66 | 62, 65 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (abs‘𝑀) < 𝑘) |
| 67 | 19 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (abs‘𝑀) ∈ ℝ) |
| 68 | 63 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℤ) |
| 69 | 68 | zred 12722 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℝ) |
| 70 | 67, 69 | ltnled 11408 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ (abs‘𝑀))) |
| 71 | 66, 70 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ¬ 𝑘 ≤ (abs‘𝑀)) |
| 72 | 71 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ≤ (abs‘𝑀)) |
| 73 | | prmz 16712 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℤ) |
| 74 | 73 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ) |
| 75 | 4 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ≠ 0) |
| 76 | 56, 75, 5 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (abs‘𝑀) ∈
ℕ) |
| 77 | | dvdsle 16347 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧
(abs‘𝑀) ∈
ℕ) → (𝑘 ∥
(abs‘𝑀) → 𝑘 ≤ (abs‘𝑀))) |
| 78 | 74, 76, 77 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ (abs‘𝑀) → 𝑘 ≤ (abs‘𝑀))) |
| 79 | 72, 78 | mtod 198 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ (abs‘𝑀)) |
| 80 | | pceq0 16909 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℙ ∧
(abs‘𝑀) ∈
ℕ) → ((𝑘 pCnt
(abs‘𝑀)) = 0 ↔
¬ 𝑘 ∥
(abs‘𝑀))) |
| 81 | 55, 76, 80 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑀)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑀))) |
| 82 | 79, 81 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑀)) = 0) |
| 83 | 60, 82 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑀) = 0) |
| 84 | 83 | oveq2d 7447 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑0)) |
| 85 | 30 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ) |
| 86 | | lgscl 27355 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈
ℤ) |
| 87 | 85, 74, 86 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℤ) |
| 88 | 87 | zcnd 12723 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℂ) |
| 89 | 88 | exp0d 14180 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑0) = 1) |
| 90 | 84, 89 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) = 1) |
| 91 | 90 | ifeq1da 4557 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, 1, 1)) |
| 92 | | ifid 4566 |
. . . 4
⊢ if(𝑘 ∈ ℙ, 1, 1) =
1 |
| 93 | 91, 92 | eqtrdi 2793 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = 1) |
| 94 | 54, 93 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (𝐹‘𝑘) = 1) |
| 95 | 2, 8, 29, 40, 94 | seqid2 14089 |
1
⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁)))) |