| Step | Hyp | Ref
| Expression |
| 1 | | 3anrot 1100 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈
ℤ)) |
| 2 | | lgsdilem 27368 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1))) |
| 3 | 1, 2 | sylanb 581 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1))) |
| 4 | | ancom 460 |
. . . . 5
⊢ (((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ (𝑀 · 𝑁) < 0)) |
| 5 | | ifbi 4548 |
. . . . 5
⊢ ((((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ (𝑀 · 𝑁) < 0)) → if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1)) |
| 6 | 4, 5 | ax-mp 5 |
. . . 4
⊢
if(((𝑀 ·
𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ (𝑀 · 𝑁) < 0), -1, 1) |
| 7 | | ancom 460 |
. . . . . 6
⊢ ((𝑀 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑀 < 0)) |
| 8 | | ifbi 4548 |
. . . . . 6
⊢ (((𝑀 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑀 < 0)) → if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1)) |
| 9 | 7, 8 | ax-mp 5 |
. . . . 5
⊢ if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) |
| 10 | | ancom 460 |
. . . . . 6
⊢ ((𝑁 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑁 < 0)) |
| 11 | | ifbi 4548 |
. . . . . 6
⊢ (((𝑁 < 0 ∧ 𝐴 < 0) ↔ (𝐴 < 0 ∧ 𝑁 < 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1)) |
| 12 | 10, 11 | ax-mp 5 |
. . . . 5
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1) |
| 13 | 9, 12 | oveq12i 7443 |
. . . 4
⊢
(if((𝑀 < 0 ∧
𝐴 < 0), -1, 1) ·
if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = (if((𝐴 < 0 ∧ 𝑀 < 0), -1, 1) · if((𝐴 < 0 ∧ 𝑁 < 0), -1, 1)) |
| 14 | 3, 6, 13 | 3eqtr4g 2802 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))) |
| 15 | | simpl2 1193 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℤ) |
| 16 | | simpl3 1194 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℤ) |
| 17 | 15, 16 | zmulcld 12728 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ∈ ℤ) |
| 18 | 15 | zcnd 12723 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ∈ ℂ) |
| 19 | 16 | zcnd 12723 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ∈ ℂ) |
| 20 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑀 ≠ 0) |
| 21 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝑁 ≠ 0) |
| 22 | 18, 19, 20, 21 | mulne0d 11915 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) ≠ 0) |
| 23 | | nnabscl 15364 |
. . . . . . 7
⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
| 24 | 17, 22, 23 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) ∈ ℕ) |
| 25 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 26 | 24, 25 | eleqtrdi 2851 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) ∈
(ℤ≥‘1)) |
| 27 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → 𝐴 ∈ ℤ) |
| 28 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)) |
| 29 | 28 | lgsfcl3 27362 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)),
1)):ℕ⟶ℤ) |
| 30 | 27, 15, 20, 29 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)),
1)):ℕ⟶ℤ) |
| 31 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈ ℕ) |
| 32 | | ffvelcdm 7101 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ) |
| 33 | 30, 31, 32 | syl2an 596 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ) |
| 34 | 33 | zcnd 12723 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℂ) |
| 35 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
| 36 | 35 | lgsfcl3 27362 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
| 37 | 27, 16, 21, 36 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)),
1)):ℕ⟶ℤ) |
| 38 | | ffvelcdm 7101 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
| 39 | 37, 31, 38 | syl2an 596 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
| 40 | 39 | zcnd 12723 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
| 41 | | simpr 484 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈
ℙ) |
| 42 | 15 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈
ℤ) |
| 43 | 20 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ≠ 0) |
| 44 | 16 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈
ℤ) |
| 45 | 21 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0) |
| 46 | | pcmul 16889 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt (𝑀 · 𝑁)) = ((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))) |
| 47 | 41, 42, 43, 44, 45, 46 | syl122anc 1381 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (𝑀 · 𝑁)) = ((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) = ((𝐴 /L 𝑘)↑((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁)))) |
| 49 | 27 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈
ℤ) |
| 50 | | prmz 16712 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℤ) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈
ℤ) |
| 52 | | lgscl 27355 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈
ℤ) |
| 53 | 49, 51, 52 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℤ) |
| 54 | 53 | zcnd 12723 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈
ℂ) |
| 55 | | pczcl 16886 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
| 56 | 41, 44, 45, 55 | syl12anc 837 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈
ℕ0) |
| 57 | | pczcl 16886 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝑘 pCnt 𝑀) ∈
ℕ0) |
| 58 | 41, 42, 43, 57 | syl12anc 837 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑀) ∈
ℕ0) |
| 59 | 54, 56, 58 | expaddd 14188 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑((𝑘 pCnt 𝑀) + (𝑘 pCnt 𝑁))) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 60 | 48, 59 | eqtrd 2777 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 61 | | iftrue 4531 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁)))) |
| 62 | 61 | adantl 481 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁)))) |
| 63 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀))) |
| 64 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℙ → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 65 | 63, 64 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℙ → (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 66 | 65 | adantl 481 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) · ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)))) |
| 67 | 60, 62, 66 | 3eqtr4rd 2788 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
| 68 | | 1t1e1 12428 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
| 69 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) = 1) |
| 70 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑁)), 1) = 1) |
| 71 | 69, 70 | oveq12d 7449 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ ℙ →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = (1 · 1)) |
| 72 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ ℙ →
if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) = 1) |
| 73 | 68, 71, 72 | 3eqtr4a 2803 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ ℙ →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
| 74 | 73 | adantl 481 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 ≠ 0
∧ 𝑁 ≠ 0)) ∧
𝑘 ∈
(1...(abs‘(𝑀 ·
𝑁)))) ∧ ¬ 𝑘 ∈ ℙ) →
(if(𝑘 ∈ ℙ,
((𝐴 /L
𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
| 75 | 67, 74 | pm2.61dan 813 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
| 76 | 31 | adantl 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℕ) |
| 77 | | eleq1w 2824 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
| 78 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘)) |
| 79 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑀) = (𝑘 pCnt 𝑀)) |
| 80 | 78, 79 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀))) |
| 81 | 77, 80 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
| 82 | | ovex 7464 |
. . . . . . . . . 10
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ V |
| 83 | | 1ex 11257 |
. . . . . . . . . 10
⊢ 1 ∈
V |
| 84 | 82, 83 | ifex 4576 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) ∈ V |
| 85 | 81, 28, 84 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1)) |
| 86 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁)) |
| 87 | 78, 86 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁))) |
| 88 | 77, 87 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 89 | | ovex 7464 |
. . . . . . . . . 10
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)) ∈ V |
| 90 | 89, 83 | ifex 4576 |
. . . . . . . . 9
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1) ∈ V |
| 91 | 88, 35, 90 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1)) |
| 92 | 85, 91 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 93 | 76, 92 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘)) = (if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) · if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑁)), 1))) |
| 94 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 pCnt (𝑀 · 𝑁)) = (𝑘 pCnt (𝑀 · 𝑁))) |
| 95 | 78, 94 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))) = ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁)))) |
| 96 | 77, 95 | ifbieq1d 4550 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
| 97 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)) |
| 98 | | ovex 7464 |
. . . . . . . . 9
⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))) ∈ V |
| 99 | 98, 83 | ifex 4576 |
. . . . . . . 8
⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1) ∈ V |
| 100 | 96, 97, 99 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
| 101 | 76, 100 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt (𝑀 · 𝑁))), 1)) |
| 102 | 75, 93, 101 | 3eqtr4rd 2788 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘(𝑀 · 𝑁)))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1))‘𝑘) = (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) · ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘))) |
| 103 | 26, 34, 40, 102 | prodfmul 15926 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁))) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))))) |
| 104 | 27, 15, 16, 20, 21, 28 | lgsdilem2 27377 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁)))) |
| 105 | 27, 16, 15, 21, 20, 35 | lgsdilem2 27377 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑁 · 𝑀)))) |
| 106 | 18, 19 | mulcomd 11282 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
| 107 | 106 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘(𝑀 · 𝑁)) = (abs‘(𝑁 · 𝑀))) |
| 108 | 107 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑁 · 𝑀)))) |
| 109 | 105, 108 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁)))) |
| 110 | 104, 109 | oveq12d 7449 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘(𝑀 · 𝑁))) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘(𝑀 · 𝑁))))) |
| 111 | 103, 110 | eqtr4d 2780 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 112 | 14, 111 | oveq12d 7449 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁)))) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
| 113 | 97 | lgsval4 27361 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (𝐴 /L (𝑀 · 𝑁)) = (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))))) |
| 114 | 27, 17, 22, 113 | syl3anc 1373 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = (if(((𝑀 · 𝑁) < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt (𝑀 · 𝑁))), 1)))‘(abs‘(𝑀 · 𝑁))))) |
| 115 | 28 | lgsval4 27361 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝐴 /L 𝑀) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)))) |
| 116 | 27, 15, 20, 115 | syl3anc 1373 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L 𝑀) = (if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)))) |
| 117 | 35 | lgsval4 27361 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 118 | 27, 16, 21, 117 | syl3anc 1373 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) |
| 119 | 116, 118 | oveq12d 7449 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀))) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
| 120 | | neg1cn 12380 |
. . . . . 6
⊢ -1 ∈
ℂ |
| 121 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 122 | 120, 121 | ifcli 4573 |
. . . . 5
⊢ if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
| 123 | 122 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
| 124 | | nnabscl 15364 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈
ℕ) |
| 125 | 15, 20, 124 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑀) ∈
ℕ) |
| 126 | 125, 25 | eleqtrdi 2851 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑀) ∈
(ℤ≥‘1)) |
| 127 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘𝑀)) → 𝑘 ∈ ℕ) |
| 128 | 30, 127, 32 | syl2an 596 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑀))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℤ) |
| 129 | 128 | zcnd 12723 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑀))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))‘𝑘) ∈ ℂ) |
| 130 | | mulcl 11239 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
| 131 | 130 | adantl 481 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
| 132 | 126, 129,
131 | seqcl 14063 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) ∈ ℂ) |
| 133 | 120, 121 | ifcli 4573 |
. . . . 5
⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ |
| 134 | 133 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈
ℂ) |
| 135 | | nnabscl 15364 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
| 136 | 16, 21, 135 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑁) ∈
ℕ) |
| 137 | 136, 25 | eleqtrdi 2851 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (abs‘𝑁) ∈
(ℤ≥‘1)) |
| 138 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(abs‘𝑁)) → 𝑘 ∈ ℕ) |
| 139 | 37, 138, 38 | syl2an 596 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℤ) |
| 140 | 139 | zcnd 12723 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) ∧ 𝑘 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑘) ∈ ℂ) |
| 141 | 137, 140,
131 | seqcl 14063 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ) |
| 142 | 123, 132,
134, 141 | mul4d 11473 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀))) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
| 143 | 119, 142 | eqtrd 2777 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)) = ((if((𝑀 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · ((seq1( ·
, (𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
((𝐴 /L
𝑛)↑(𝑛 pCnt 𝑀)), 1)))‘(abs‘𝑀)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))) |
| 144 | 112, 114,
143 | 3eqtr4d 2787 |
1
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁))) |