Proof of Theorem fprodeq0
| Step | Hyp | Ref
| Expression |
| 1 | | eluzel2 12883 |
. . . . . . 7
⊢ (𝐾 ∈
(ℤ≥‘𝑁) → 𝑁 ∈ ℤ) |
| 2 | 1 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ ℤ) |
| 3 | 2 | zred 12722 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ ℝ) |
| 4 | 3 | ltp1d 12198 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑁 < (𝑁 + 1)) |
| 5 | | fzdisj 13591 |
. . . 4
⊢ (𝑁 < (𝑁 + 1) → ((𝑀...𝑁) ∩ ((𝑁 + 1)...𝐾)) = ∅) |
| 6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → ((𝑀...𝑁) ∩ ((𝑁 + 1)...𝐾)) = ∅) |
| 7 | | fprodeq0.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
| 8 | | eluzel2 12883 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 9 | | fprodeq0.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 10 | 8, 9 | eleq2s 2859 |
. . . . . . . 8
⊢ (𝑁 ∈ 𝑍 → 𝑀 ∈ ℤ) |
| 11 | 7, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℤ) |
| 13 | | eluzelz 12888 |
. . . . . . 7
⊢ (𝐾 ∈
(ℤ≥‘𝑁) → 𝐾 ∈ ℤ) |
| 14 | 13 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝐾 ∈ ℤ) |
| 15 | 12, 14, 2 | 3jca 1129 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → (𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
| 16 | | eluzle 12891 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
| 17 | 16, 9 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑁 ∈ 𝑍 → 𝑀 ≤ 𝑁) |
| 18 | 7, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
| 19 | | eluzle 12891 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝐾) |
| 20 | 18, 19 | anim12i 613 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝐾)) |
| 21 | | elfz2 13554 |
. . . . 5
⊢ (𝑁 ∈ (𝑀...𝐾) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝐾))) |
| 22 | 15, 20, 21 | sylanbrc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝐾)) |
| 23 | | fzsplit 13590 |
. . . 4
⊢ (𝑁 ∈ (𝑀...𝐾) → (𝑀...𝐾) = ((𝑀...𝑁) ∪ ((𝑁 + 1)...𝐾))) |
| 24 | 22, 23 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → (𝑀...𝐾) = ((𝑀...𝑁) ∪ ((𝑁 + 1)...𝐾))) |
| 25 | | fzfid 14014 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → (𝑀...𝐾) ∈ Fin) |
| 26 | | elfzuz 13560 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 27 | 26, 9 | eleqtrrdi 2852 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ 𝑍) |
| 28 | | fprodeq0.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
| 29 | 27, 28 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝐴 ∈ ℂ) |
| 30 | 29 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝐴 ∈ ℂ) |
| 31 | 6, 24, 25, 30 | fprodsplit 16002 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → ∏𝑘 ∈ (𝑀...𝐾)𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...𝐾)𝐴)) |
| 32 | 7, 9 | eleqtrdi 2851 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 33 | | elfzuz 13560 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 34 | 33, 9 | eleqtrrdi 2852 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ 𝑍) |
| 35 | 34, 28 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) |
| 36 | 32, 35 | fprodm1s 16006 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (∏𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 · ⦋𝑁 / 𝑘⦌𝐴)) |
| 37 | | fprodeq0.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 𝑁) → 𝐴 = 0) |
| 38 | 7, 37 | csbied 3935 |
. . . . . 6
⊢ (𝜑 → ⦋𝑁 / 𝑘⦌𝐴 = 0) |
| 39 | 38 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (∏𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 · ⦋𝑁 / 𝑘⦌𝐴) = (∏𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 · 0)) |
| 40 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (𝑀...(𝑁 − 1)) ∈ Fin) |
| 41 | | elfzuz 13560 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 42 | 41, 9 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ 𝑍) |
| 43 | 42, 28 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
| 44 | 40, 43 | fprodcl 15988 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 ∈ ℂ) |
| 45 | 44 | mul01d 11460 |
. . . . 5
⊢ (𝜑 → (∏𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 · 0) = 0) |
| 46 | 36, 39, 45 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = 0) |
| 47 | 46 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = 0) |
| 48 | 47 | oveq1d 7446 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ∏𝑘 ∈ ((𝑁 + 1)...𝐾)𝐴) = (0 · ∏𝑘 ∈ ((𝑁 + 1)...𝐾)𝐴)) |
| 49 | | fzfid 14014 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → ((𝑁 + 1)...𝐾) ∈ Fin) |
| 50 | 9 | peano2uzs 12944 |
. . . . . . . . 9
⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) |
| 51 | 7, 50 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈ 𝑍) |
| 52 | | elfzuz 13560 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑁 + 1)...𝐾) → 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) |
| 53 | 9 | uztrn2 12897 |
. . . . . . . 8
⊢ (((𝑁 + 1) ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) |
| 54 | 51, 52, 53 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑁 + 1)...𝐾)) → 𝑘 ∈ 𝑍) |
| 55 | 54 | adantrl 716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐾 ∈ (ℤ≥‘𝑁) ∧ 𝑘 ∈ ((𝑁 + 1)...𝐾))) → 𝑘 ∈ 𝑍) |
| 56 | 55, 28 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 ∈ (ℤ≥‘𝑁) ∧ 𝑘 ∈ ((𝑁 + 1)...𝐾))) → 𝐴 ∈ ℂ) |
| 57 | 56 | anassrs 467 |
. . . 4
⊢ (((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) ∧ 𝑘 ∈ ((𝑁 + 1)...𝐾)) → 𝐴 ∈ ℂ) |
| 58 | 49, 57 | fprodcl 15988 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → ∏𝑘 ∈ ((𝑁 + 1)...𝐾)𝐴 ∈ ℂ) |
| 59 | 58 | mul02d 11459 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → (0 ·
∏𝑘 ∈ ((𝑁 + 1)...𝐾)𝐴) = 0) |
| 60 | 31, 48, 59 | 3eqtrd 2781 |
1
⊢ ((𝜑 ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → ∏𝑘 ∈ (𝑀...𝐾)𝐴 = 0) |