Step | Hyp | Ref
| Expression |
1 | | iprodmul.1 |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | iprodmul.2 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | iprodmul.3 |
. . . 4
⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) |
4 | | iprodmul.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) |
5 | | iprodmul.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
6 | 4, 5 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
7 | | iprodmul.6 |
. . . 4
⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∃𝑧(𝑧 ≠ 0 ∧ seq𝑚( · , 𝐺) ⇝ 𝑧)) |
8 | | iprodmul.7 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵) |
9 | | iprodmul.8 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) |
10 | 8, 9 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) |
11 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑎 = 𝑘 → (𝐹‘𝑎) = (𝐹‘𝑘)) |
12 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑎 = 𝑘 → (𝐺‘𝑎) = (𝐺‘𝑘)) |
13 | 11, 12 | oveq12d 6567 |
. . . . . 6
⊢ (𝑎 = 𝑘 → ((𝐹‘𝑎) · (𝐺‘𝑎)) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
14 | | eqid 2610 |
. . . . . 6
⊢ (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎))) = (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎))) |
15 | | ovex 6577 |
. . . . . 6
⊢ ((𝐹‘𝑘) · (𝐺‘𝑘)) ∈ V |
16 | 13, 14, 15 | fvmpt 6191 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 → ((𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
17 | 16 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
18 | 1, 3, 6, 7, 10, 17 | ntrivcvgmul 14473 |
. . 3
⊢ (𝜑 → ∃𝑝 ∈ 𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑝( · , (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))) ⇝ 𝑤)) |
19 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑎 → (𝐹‘𝑚) = (𝐹‘𝑎)) |
20 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑎 → (𝐺‘𝑚) = (𝐺‘𝑎)) |
21 | 19, 20 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑚 = 𝑎 → ((𝐹‘𝑚) · (𝐺‘𝑚)) = ((𝐹‘𝑎) · (𝐺‘𝑎))) |
22 | 21 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚))) = (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎))) |
23 | | seqeq3 12668 |
. . . . . . . 8
⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚))) = (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎))) → seq𝑝( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) = seq𝑝( · , (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎))))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
⊢ seq𝑝( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) = seq𝑝( · , (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))) |
25 | 24 | breq1i 4590 |
. . . . . 6
⊢ (seq𝑝( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ⇝ 𝑤 ↔ seq𝑝( · , (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))) ⇝ 𝑤) |
26 | 25 | anbi2i 726 |
. . . . 5
⊢ ((𝑤 ≠ 0 ∧ seq𝑝( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ⇝ 𝑤) ↔ (𝑤 ≠ 0 ∧ seq𝑝( · , (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))) ⇝ 𝑤)) |
27 | 26 | exbii 1764 |
. . . 4
⊢
(∃𝑤(𝑤 ≠ 0 ∧ seq𝑝( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ⇝ 𝑤) ↔ ∃𝑤(𝑤 ≠ 0 ∧ seq𝑝( · , (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))) ⇝ 𝑤)) |
28 | 27 | rexbii 3023 |
. . 3
⊢
(∃𝑝 ∈
𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑝( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ⇝ 𝑤) ↔ ∃𝑝 ∈ 𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑝( · , (𝑎 ∈ 𝑍 ↦ ((𝐹‘𝑎) · (𝐺‘𝑎)))) ⇝ 𝑤)) |
29 | 18, 28 | sylibr 223 |
. 2
⊢ (𝜑 → ∃𝑝 ∈ 𝑍 ∃𝑤(𝑤 ≠ 0 ∧ seq𝑝( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ⇝ 𝑤)) |
30 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
31 | 6, 10 | mulcld 9939 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) · (𝐺‘𝑘)) ∈ ℂ) |
32 | | fveq2 6103 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
33 | | fveq2 6103 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘)) |
34 | 32, 33 | oveq12d 6567 |
. . . . 5
⊢ (𝑚 = 𝑘 → ((𝐹‘𝑚) · (𝐺‘𝑚)) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
35 | | eqid 2610 |
. . . . 5
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚))) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚))) |
36 | 34, 35 | fvmptg 6189 |
. . . 4
⊢ ((𝑘 ∈ 𝑍 ∧ ((𝐹‘𝑘) · (𝐺‘𝑘)) ∈ ℂ) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
37 | 30, 31, 36 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
38 | 4, 8 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) · (𝐺‘𝑘)) = (𝐴 · 𝐵)) |
39 | 37, 38 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))‘𝑘) = (𝐴 · 𝐵)) |
40 | 5, 9 | mulcld 9939 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴 · 𝐵) ∈ ℂ) |
41 | 1, 2, 3, 4, 5 | iprodclim2 14569 |
. . 3
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ∏𝑘 ∈ 𝑍 𝐴) |
42 | | seqex 12665 |
. . . 4
⊢ seq𝑀( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ∈ V |
43 | 42 | a1i 11 |
. . 3
⊢ (𝜑 → seq𝑀( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ∈ V) |
44 | 1, 2, 7, 8, 9 | iprodclim2 14569 |
. . 3
⊢ (𝜑 → seq𝑀( · , 𝐺) ⇝ ∏𝑘 ∈ 𝑍 𝐵) |
45 | 1, 2, 6 | prodf 14458 |
. . . 4
⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ) |
46 | 45 | ffvelrnda 6267 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( · , 𝐹)‘𝑗) ∈ ℂ) |
47 | 1, 2, 10 | prodf 14458 |
. . . 4
⊢ (𝜑 → seq𝑀( · , 𝐺):𝑍⟶ℂ) |
48 | 47 | ffvelrnda 6267 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( · , 𝐺)‘𝑗) ∈ ℂ) |
49 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
50 | 49, 1 | syl6eleq 2698 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
51 | | elfzuz 12209 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) |
52 | 51, 1 | syl6eleqr 2699 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) |
53 | 52, 6 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
54 | 53 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
55 | 52, 10 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐺‘𝑘) ∈ ℂ) |
56 | 55 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐺‘𝑘) ∈ ℂ) |
57 | 37 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
58 | 52, 57 | sylan2 490 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → ((𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) |
59 | 50, 54, 56, 58 | prodfmul 14461 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚))))‘𝑗) = ((seq𝑀( · , 𝐹)‘𝑗) · (seq𝑀( · , 𝐺)‘𝑗))) |
60 | 1, 2, 41, 43, 44, 46, 48, 59 | climmul 14211 |
. 2
⊢ (𝜑 → seq𝑀( · , (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚) · (𝐺‘𝑚)))) ⇝ (∏𝑘 ∈ 𝑍 𝐴 · ∏𝑘 ∈ 𝑍 𝐵)) |
61 | 1, 2, 29, 39, 40, 60 | iprodclim 14568 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝑍 (𝐴 · 𝐵) = (∏𝑘 ∈ 𝑍 𝐴 · ∏𝑘 ∈ 𝑍 𝐵)) |