Step | Hyp | Ref
| Expression |
1 | | prodmo.1 |
. . 3
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) |
2 | | prodmo.2 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
3 | | prodmolem2.7 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) |
4 | | prodmolem2.9 |
. . . . . . 7
⊢ (𝜑 → 𝐾 Isom < , < ((1...(#‘𝐴)), 𝐴)) |
5 | | prodmolem2.8 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴) |
6 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ∈
V |
7 | 6 | f1oen 7976 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...𝑁)–1-1-onto→𝐴 → (1...𝑁) ≈ 𝐴) |
8 | 5, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) ≈ 𝐴) |
9 | | fzfid 12772 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
10 | 8 | ensymd 8007 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≈ (1...𝑁)) |
11 | | enfii 8177 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ Fin
∧ 𝐴 ≈ (1...𝑁)) → 𝐴 ∈ Fin) |
12 | 9, 10, 11 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ Fin) |
13 | | hashen 13135 |
. . . . . . . . . . . 12
⊢
(((1...𝑁) ∈ Fin
∧ 𝐴 ∈ Fin) →
((#‘(1...𝑁)) =
(#‘𝐴) ↔
(1...𝑁) ≈ 𝐴)) |
14 | 9, 12, 13 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘(1...𝑁)) = (#‘𝐴) ↔ (1...𝑁) ≈ 𝐴)) |
15 | 8, 14 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(1...𝑁)) = (#‘𝐴)) |
16 | | prodmolem2.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
17 | 16 | nnnn0d 11351 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
18 | | hashfz1 13134 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(1...𝑁)) = 𝑁) |
20 | 15, 19 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐴) = 𝑁) |
21 | 20 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝜑 → (1...(#‘𝐴)) = (1...𝑁)) |
22 | | isoeq4 6570 |
. . . . . . . 8
⊢
((1...(#‘𝐴)) =
(1...𝑁) → (𝐾 Isom < , <
((1...(#‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐾 Isom < , < ((1...(#‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
24 | 4, 23 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
25 | | isof1o 6573 |
. . . . . 6
⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
26 | | f1of 6137 |
. . . . . 6
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴) |
27 | 24, 25, 26 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴) |
28 | | nnuz 11723 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
29 | 16, 28 | syl6eleq 2711 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
30 | | eluzfz2 12349 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
32 | 27, 31 | ffvelrnd 6360 |
. . . 4
⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴) |
33 | 3, 32 | sseldd 3604 |
. . 3
⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀)) |
34 | 3 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ (ℤ≥‘𝑀)) |
35 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
36 | | f1ocnvfv2 6533 |
. . . . . . . . 9
⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑗 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑗)) = 𝑗) |
37 | 35, 36 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑗)) = 𝑗) |
38 | | f1ocnv 6149 |
. . . . . . . . . . . 12
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁)) |
39 | | f1of 6137 |
. . . . . . . . . . . 12
⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁)) |
40 | 35, 38, 39 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁)) |
41 | 40 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (◡𝐾‘𝑗) ∈ (1...𝑁)) |
42 | | elfzle2 12345 |
. . . . . . . . . 10
⊢ ((◡𝐾‘𝑗) ∈ (1...𝑁) → (◡𝐾‘𝑗) ≤ 𝑁) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (◡𝐾‘𝑗) ≤ 𝑁) |
44 | 24 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
45 | | fzssuz 12382 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
(ℤ≥‘1) |
46 | | uzssz 11707 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) ⊆ ℤ |
47 | | zssre 11384 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
48 | 46, 47 | sstri 3612 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘1) ⊆ ℝ |
49 | 45, 48 | sstri 3612 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
ℝ |
50 | | ressxr 10083 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
51 | 49, 50 | sstri 3612 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℝ* |
52 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (1...𝑁) ⊆
ℝ*) |
53 | | uzssz 11707 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
54 | 53, 47 | sstri 3612 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
55 | 54, 50 | sstri 3612 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑀) ⊆
ℝ* |
56 | 3, 55 | syl6ss 3615 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
57 | 56 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐴 ⊆
ℝ*) |
58 | 31 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑁 ∈ (1...𝑁)) |
59 | | leisorel 13244 |
. . . . . . . . . 10
⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*)
∧ ((◡𝐾‘𝑗) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑗) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑗)) ≤ (𝐾‘𝑁))) |
60 | 44, 52, 57, 41, 58, 59 | syl122anc 1335 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((◡𝐾‘𝑗) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑗)) ≤ (𝐾‘𝑁))) |
61 | 43, 60 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑗)) ≤ (𝐾‘𝑁)) |
62 | 37, 61 | eqbrtrrd 4677 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ≤ (𝐾‘𝑁)) |
63 | 3, 53 | syl6ss 3615 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℤ) |
64 | 63 | sselda 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ ℤ) |
65 | | eluzelz 11697 |
. . . . . . . . . 10
⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ) |
66 | 33, 65 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ) |
67 | 66 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ) |
68 | | eluz 11701 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑗) ↔ 𝑗 ≤ (𝐾‘𝑁))) |
69 | 64, 67, 68 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑗) ↔ 𝑗 ≤ (𝐾‘𝑁))) |
70 | 62, 69 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑗)) |
71 | | elfzuzb 12336 |
. . . . . 6
⊢ (𝑗 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑗 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑗))) |
72 | 34, 70, 71 | sylanbrc 698 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ (𝑀...(𝐾‘𝑁))) |
73 | 72 | ex 450 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐴 → 𝑗 ∈ (𝑀...(𝐾‘𝑁)))) |
74 | 73 | ssrdv 3609 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁))) |
75 | 1, 2, 33, 74 | fprodcvg 14660 |
. 2
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾‘𝑁))) |
76 | | mulid2 10038 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (1
· 𝑚) = 𝑚) |
77 | 76 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚) |
78 | | mulid1 10037 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚) |
79 | 78 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚) |
80 | | mulcl 10020 |
. . . . 5
⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ) |
81 | 80 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ) |
82 | | 1cnd 10056 |
. . . 4
⊢ (𝜑 → 1 ∈
ℂ) |
83 | 31, 21 | eleqtrrd 2704 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (1...(#‘𝐴))) |
84 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
85 | 84 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
86 | 85, 2 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
87 | 86 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)) |
88 | | iffalse 4095 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
89 | | ax-1cn 9994 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
90 | 88, 89 | syl6eqel 2709 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
91 | 87, 90 | pm2.61d1 171 |
. . . . . . 7
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
92 | 91 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
93 | 92, 1 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → 𝐹:ℤ⟶ℂ) |
94 | | elfzelz 12342 |
. . . . 5
⊢ (𝑚 ∈ (𝑀...(𝐾‘(#‘𝐴))) → 𝑚 ∈ ℤ) |
95 | | ffvelrn 6357 |
. . . . 5
⊢ ((𝐹:ℤ⟶ℂ ∧
𝑚 ∈ ℤ) →
(𝐹‘𝑚) ∈ ℂ) |
96 | 93, 94, 95 | syl2an 494 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀...(𝐾‘(#‘𝐴)))) → (𝐹‘𝑚) ∈ ℂ) |
97 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) |
98 | 97 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 1 ↔ (𝐹‘𝑚) = 1)) |
99 | | fzssuz 12382 |
. . . . . . . . . 10
⊢ (𝑀...(𝐾‘(#‘𝐴))) ⊆
(ℤ≥‘𝑀) |
100 | 99, 53 | sstri 3612 |
. . . . . . . . 9
⊢ (𝑀...(𝐾‘(#‘𝐴))) ⊆ ℤ |
101 | | eldifi 3732 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(#‘𝐴)))) |
102 | 100, 101 | sseldi 3601 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ) |
103 | | eldifn 3733 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
104 | 103, 88 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
105 | 104, 89 | syl6eqel 2709 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
106 | 1 | fvmpt2 6291 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
107 | 102, 105,
106 | syl2anc 693 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
108 | 107, 104 | eqtrd 2656 |
. . . . . 6
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 1) |
109 | 98, 108 | vtoclga 3272 |
. . . . 5
⊢ (𝑚 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 1) |
110 | 109 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 1) |
111 | | isof1o 6573 |
. . . . . . . 8
⊢ (𝐾 Isom < , <
((1...(#‘𝐴)), 𝐴) → 𝐾:(1...(#‘𝐴))–1-1-onto→𝐴) |
112 | | f1of 6137 |
. . . . . . . 8
⊢ (𝐾:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(#‘𝐴))⟶𝐴) |
113 | 4, 111, 112 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐾:(1...(#‘𝐴))⟶𝐴) |
114 | 113 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴) |
115 | 114 | iftrued 4094 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
116 | 63 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → 𝐴 ⊆ ℤ) |
117 | 116, 114 | sseldd 3604 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐾‘𝑥) ∈ ℤ) |
118 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝜑 |
119 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴 |
120 | | nfcsb1v 3549 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 |
121 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘1 |
122 | 119, 120,
121 | nfif 4115 |
. . . . . . . . . 10
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) |
123 | 122 | nfel1 2779 |
. . . . . . . . 9
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ |
124 | 118, 123 | nfim 1825 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) |
125 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐾‘𝑥) ∈ V |
126 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
127 | | csbeq1a 3542 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
128 | 126, 127 | ifbieq1d 4109 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
129 | 128 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)) |
130 | 129 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) ↔ (𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ))) |
131 | 124, 125,
130, 91 | vtoclf 3258 |
. . . . . . 7
⊢ (𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) |
132 | 131 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) |
133 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
134 | | csbeq1 3536 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
135 | 133, 134 | ifbieq1d 4109 |
. . . . . . 7
⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
136 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 1) |
137 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ 𝐴 |
138 | | nfcsb1v 3549 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵 |
139 | 137, 138,
121 | nfif 4115 |
. . . . . . . . 9
⊢
Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) |
140 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴)) |
141 | | csbeq1a 3542 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵) |
142 | 140, 141 | ifbieq1d 4109 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
143 | 136, 139,
142 | cbvmpt 4749 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
144 | 1, 143 | eqtri 2644 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
145 | 135, 144 | fvmptg 6280 |
. . . . . 6
⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
146 | 117, 132,
145 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
147 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑥 ∈ (1...(#‘𝐴)) → 𝑥 ∈ ℕ) |
148 | 147 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → 𝑥 ∈ ℕ) |
149 | 115, 132 | eqeltrrd 2702 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ) |
150 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → (𝐾‘𝑗) = (𝐾‘𝑥)) |
151 | 150 | csbeq1d 3540 |
. . . . . . 7
⊢ (𝑗 = 𝑥 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
152 | | prodmolem2.4 |
. . . . . . 7
⊢ 𝐻 = (𝑗 ∈ ℕ ↦ ⦋(𝐾‘𝑗) / 𝑘⦌𝐵) |
153 | 151, 152 | fvmptg 6280 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧
⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
154 | 148, 149,
153 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
155 | 115, 146,
154 | 3eqtr4rd 2667 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥))) |
156 | 77, 79, 81, 82, 4, 83, 3, 96, 110, 155 | seqcoll 13248 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐻)‘𝑁)) |
157 | | prodmo.3 |
. . . 4
⊢ 𝐺 = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵) |
158 | 16, 16 | jca 554 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
159 | 1, 2, 157, 152, 158, 5, 35 | prodmolem3 14663 |
. . 3
⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁)) |
160 | 156, 159 | eqtr4d 2659 |
. 2
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐺)‘𝑁)) |
161 | 75, 160 | breqtrd 4679 |
1
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁)) |