| Step | Hyp | Ref
| Expression |
| 1 | | fprodabs.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
| 2 | | fprodabs.1 |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 3 | 1, 2 | eleqtrdi 2851 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 4 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑎 = 𝑀 → (𝑀...𝑎) = (𝑀...𝑀)) |
| 5 | 4 | prodeq1d 15956 |
. . . . . 6
⊢ (𝑎 = 𝑀 → ∏𝑘 ∈ (𝑀...𝑎)𝐴 = ∏𝑘 ∈ (𝑀...𝑀)𝐴) |
| 6 | 5 | fveq2d 6910 |
. . . . 5
⊢ (𝑎 = 𝑀 → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = (abs‘∏𝑘 ∈ (𝑀...𝑀)𝐴)) |
| 7 | 4 | prodeq1d 15956 |
. . . . 5
⊢ (𝑎 = 𝑀 → ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) = ∏𝑘 ∈ (𝑀...𝑀)(abs‘𝐴)) |
| 8 | 6, 7 | eqeq12d 2753 |
. . . 4
⊢ (𝑎 = 𝑀 → ((abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) ↔ (abs‘∏𝑘 ∈ (𝑀...𝑀)𝐴) = ∏𝑘 ∈ (𝑀...𝑀)(abs‘𝐴))) |
| 9 | 8 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑀 → ((𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴)) ↔ (𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑀)𝐴) = ∏𝑘 ∈ (𝑀...𝑀)(abs‘𝐴)))) |
| 10 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑎 = 𝑛 → (𝑀...𝑎) = (𝑀...𝑛)) |
| 11 | 10 | prodeq1d 15956 |
. . . . . 6
⊢ (𝑎 = 𝑛 → ∏𝑘 ∈ (𝑀...𝑎)𝐴 = ∏𝑘 ∈ (𝑀...𝑛)𝐴) |
| 12 | 11 | fveq2d 6910 |
. . . . 5
⊢ (𝑎 = 𝑛 → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴)) |
| 13 | 10 | prodeq1d 15956 |
. . . . 5
⊢ (𝑎 = 𝑛 → ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) |
| 14 | 12, 13 | eqeq12d 2753 |
. . . 4
⊢ (𝑎 = 𝑛 → ((abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) ↔ (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴))) |
| 15 | 14 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑛 → ((𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴)) ↔ (𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)))) |
| 16 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑎 = (𝑛 + 1) → (𝑀...𝑎) = (𝑀...(𝑛 + 1))) |
| 17 | 16 | prodeq1d 15956 |
. . . . . 6
⊢ (𝑎 = (𝑛 + 1) → ∏𝑘 ∈ (𝑀...𝑎)𝐴 = ∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) |
| 18 | 17 | fveq2d 6910 |
. . . . 5
⊢ (𝑎 = (𝑛 + 1) → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴)) |
| 19 | 16 | prodeq1d 15956 |
. . . . 5
⊢ (𝑎 = (𝑛 + 1) → ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) = ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴)) |
| 20 | 18, 19 | eqeq12d 2753 |
. . . 4
⊢ (𝑎 = (𝑛 + 1) → ((abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) ↔ (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) = ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴))) |
| 21 | 20 | imbi2d 340 |
. . 3
⊢ (𝑎 = (𝑛 + 1) → ((𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴)) ↔ (𝜑 → (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) = ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴)))) |
| 22 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑎 = 𝑁 → (𝑀...𝑎) = (𝑀...𝑁)) |
| 23 | 22 | prodeq1d 15956 |
. . . . . 6
⊢ (𝑎 = 𝑁 → ∏𝑘 ∈ (𝑀...𝑎)𝐴 = ∏𝑘 ∈ (𝑀...𝑁)𝐴) |
| 24 | 23 | fveq2d 6910 |
. . . . 5
⊢ (𝑎 = 𝑁 → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = (abs‘∏𝑘 ∈ (𝑀...𝑁)𝐴)) |
| 25 | 22 | prodeq1d 15956 |
. . . . 5
⊢ (𝑎 = 𝑁 → ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) = ∏𝑘 ∈ (𝑀...𝑁)(abs‘𝐴)) |
| 26 | 24, 25 | eqeq12d 2753 |
. . . 4
⊢ (𝑎 = 𝑁 → ((abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴) ↔ (abs‘∏𝑘 ∈ (𝑀...𝑁)𝐴) = ∏𝑘 ∈ (𝑀...𝑁)(abs‘𝐴))) |
| 27 | 26 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑁 → ((𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑎)𝐴) = ∏𝑘 ∈ (𝑀...𝑎)(abs‘𝐴)) ↔ (𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑁)𝐴) = ∏𝑘 ∈ (𝑀...𝑁)(abs‘𝐴)))) |
| 28 | | csbfv2g 6955 |
. . . . . 6
⊢ (𝑀 ∈ ℤ →
⦋𝑀 / 𝑘⦌(abs‘𝐴) =
(abs‘⦋𝑀
/ 𝑘⦌𝐴)) |
| 29 | 28 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ⦋𝑀 / 𝑘⦌(abs‘𝐴) = (abs‘⦋𝑀 / 𝑘⦌𝐴)) |
| 30 | | fzsn 13606 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
| 31 | 30 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝑀...𝑀) = {𝑀}) |
| 32 | 31 | prodeq1d 15956 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ (𝑀...𝑀)(abs‘𝐴) = ∏𝑘 ∈ {𝑀} (abs‘𝐴)) |
| 33 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ) |
| 34 | | uzid 12893 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
| 35 | 34, 2 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ 𝑍) |
| 36 | | fprodabs.3 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
| 37 | 36 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 𝐴 ∈ ℂ) |
| 38 | | nfcsb1v 3923 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋𝑀 / 𝑘⦌𝐴 |
| 39 | 38 | nfel1 2922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ |
| 40 | | csbeq1a 3913 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑀 → 𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
| 41 | 40 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑀 → (𝐴 ∈ ℂ ↔ ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ)) |
| 42 | 39, 41 | rspc 3610 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 𝐴 ∈ ℂ → ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ)) |
| 43 | 37, 42 | mpan9 506 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑍) → ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ) |
| 44 | 35, 43 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ) |
| 45 | 44 | abscld 15475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) →
(abs‘⦋𝑀
/ 𝑘⦌𝐴) ∈
ℝ) |
| 46 | 45 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) →
(abs‘⦋𝑀
/ 𝑘⦌𝐴) ∈
ℂ) |
| 47 | 29, 46 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ⦋𝑀 / 𝑘⦌(abs‘𝐴) ∈ ℂ) |
| 48 | | prodsns 16008 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧
⦋𝑀 / 𝑘⦌(abs‘𝐴) ∈ ℂ) →
∏𝑘 ∈ {𝑀} (abs‘𝐴) = ⦋𝑀 / 𝑘⦌(abs‘𝐴)) |
| 49 | 33, 47, 48 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ {𝑀} (abs‘𝐴) = ⦋𝑀 / 𝑘⦌(abs‘𝐴)) |
| 50 | 32, 49 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ (𝑀...𝑀)(abs‘𝐴) = ⦋𝑀 / 𝑘⦌(abs‘𝐴)) |
| 51 | 30 | prodeq1d 15956 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
∏𝑘 ∈ (𝑀...𝑀)𝐴 = ∏𝑘 ∈ {𝑀}𝐴) |
| 52 | 51 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ (𝑀...𝑀)𝐴 = ∏𝑘 ∈ {𝑀}𝐴) |
| 53 | | prodsns 16008 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧
⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
| 54 | 33, 44, 53 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ {𝑀}𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
| 55 | 52, 54 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ (𝑀...𝑀)𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
| 56 | 55 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) →
(abs‘∏𝑘 ∈
(𝑀...𝑀)𝐴) = (abs‘⦋𝑀 / 𝑘⦌𝐴)) |
| 57 | 29, 50, 56 | 3eqtr4rd 2788 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) →
(abs‘∏𝑘 ∈
(𝑀...𝑀)𝐴) = ∏𝑘 ∈ (𝑀...𝑀)(abs‘𝐴)) |
| 58 | 57 | expcom 413 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑀)𝐴) = ∏𝑘 ∈ (𝑀...𝑀)(abs‘𝐴))) |
| 59 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) → (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) |
| 60 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑛 + 1) ∈ V |
| 61 | | csbfv2g 6955 |
. . . . . . . . . . 11
⊢ ((𝑛 + 1) ∈ V →
⦋(𝑛 + 1) /
𝑘⦌(abs‘𝐴) = (abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴)) |
| 62 | 60, 61 | ax-mp 5 |
. . . . . . . . . 10
⊢
⦋(𝑛 +
1) / 𝑘⦌(abs‘𝐴) = (abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴) |
| 63 | 62 | eqcomi 2746 |
. . . . . . . . 9
⊢
(abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴) = ⦋(𝑛 + 1) / 𝑘⦌(abs‘𝐴) |
| 64 | 63 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) → (abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴) = ⦋(𝑛 + 1) / 𝑘⦌(abs‘𝐴)) |
| 65 | 59, 64 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) → ((abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) · (abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴)) = (∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴) · ⦋(𝑛 + 1) / 𝑘⦌(abs‘𝐴))) |
| 66 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
| 67 | | elfzuz 13560 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...(𝑛 + 1)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 68 | 67, 2 | eleqtrrdi 2852 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...(𝑛 + 1)) → 𝑘 ∈ 𝑍) |
| 69 | 68, 36 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑛 + 1))) → 𝐴 ∈ ℂ) |
| 70 | 69 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ (𝑀...(𝑛 + 1))) → 𝐴 ∈ ℂ) |
| 71 | 66, 70 | fprodp1s 16007 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴 = (∏𝑘 ∈ (𝑀...𝑛)𝐴 · ⦋(𝑛 + 1) / 𝑘⦌𝐴)) |
| 72 | 71 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) →
(abs‘∏𝑘 ∈
(𝑀...(𝑛 + 1))𝐴) = (abs‘(∏𝑘 ∈ (𝑀...𝑛)𝐴 · ⦋(𝑛 + 1) / 𝑘⦌𝐴))) |
| 73 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝑀...𝑛) ∈ Fin) |
| 74 | | elfzuz 13560 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...𝑛) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 75 | 74, 2 | eleqtrrdi 2852 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...𝑛) → 𝑘 ∈ 𝑍) |
| 76 | 75, 36 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝐴 ∈ ℂ) |
| 77 | 76 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝐴 ∈ ℂ) |
| 78 | 73, 77 | fprodcl 15988 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ∏𝑘 ∈ (𝑀...𝑛)𝐴 ∈ ℂ) |
| 79 | | peano2uz 12943 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 + 1) ∈
(ℤ≥‘𝑀)) |
| 80 | 79, 2 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 + 1) ∈ 𝑍) |
| 81 | | nfcsb1v 3923 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋(𝑛 + 1) / 𝑘⦌𝐴 |
| 82 | 81 | nfel1 2922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋(𝑛 + 1) / 𝑘⦌𝐴 ∈ ℂ |
| 83 | | csbeq1a 3913 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → 𝐴 = ⦋(𝑛 + 1) / 𝑘⦌𝐴) |
| 84 | 83 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 + 1) → (𝐴 ∈ ℂ ↔ ⦋(𝑛 + 1) / 𝑘⦌𝐴 ∈ ℂ)) |
| 85 | 82, 84 | rspc 3610 |
. . . . . . . . . . . 12
⊢ ((𝑛 + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 𝐴 ∈ ℂ → ⦋(𝑛 + 1) / 𝑘⦌𝐴 ∈ ℂ)) |
| 86 | 37, 85 | mpan9 506 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → ⦋(𝑛 + 1) / 𝑘⦌𝐴 ∈ ℂ) |
| 87 | 80, 86 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ⦋(𝑛 + 1) / 𝑘⦌𝐴 ∈ ℂ) |
| 88 | 78, 87 | absmuld 15493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) →
(abs‘(∏𝑘 ∈
(𝑀...𝑛)𝐴 · ⦋(𝑛 + 1) / 𝑘⦌𝐴)) = ((abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) · (abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴))) |
| 89 | 72, 88 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) →
(abs‘∏𝑘 ∈
(𝑀...(𝑛 + 1))𝐴) = ((abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) · (abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴))) |
| 90 | 89 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) → (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) = ((abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) · (abs‘⦋(𝑛 + 1) / 𝑘⦌𝐴))) |
| 91 | 70 | abscld 15475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ (𝑀...(𝑛 + 1))) → (abs‘𝐴) ∈ ℝ) |
| 92 | 91 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ (𝑀...(𝑛 + 1))) → (abs‘𝐴) ∈ ℂ) |
| 93 | 66, 92 | fprodp1s 16007 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴) = (∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴) · ⦋(𝑛 + 1) / 𝑘⦌(abs‘𝐴))) |
| 94 | 93 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) → ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴) = (∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴) · ⦋(𝑛 + 1) / 𝑘⦌(abs‘𝐴))) |
| 95 | 65, 90, 94 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀) ∧ (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) → (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) = ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴)) |
| 96 | 95 | 3exp 1120 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑀) →
((abs‘∏𝑘 ∈
(𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴) → (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) = ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴)))) |
| 97 | 96 | com12 32 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝜑 → ((abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴) → (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) = ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴)))) |
| 98 | 97 | a2d 29 |
. . 3
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑛)𝐴) = ∏𝑘 ∈ (𝑀...𝑛)(abs‘𝐴)) → (𝜑 → (abs‘∏𝑘 ∈ (𝑀...(𝑛 + 1))𝐴) = ∏𝑘 ∈ (𝑀...(𝑛 + 1))(abs‘𝐴)))) |
| 99 | 9, 15, 21, 27, 58, 98 | uzind4 12948 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑁)𝐴) = ∏𝑘 ∈ (𝑀...𝑁)(abs‘𝐴))) |
| 100 | 3, 99 | mpcom 38 |
1
⊢ (𝜑 → (abs‘∏𝑘 ∈ (𝑀...𝑁)𝐴) = ∏𝑘 ∈ (𝑀...𝑁)(abs‘𝐴)) |