Step | Hyp | Ref
| Expression |
1 | | mulcl 7894 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑚 · 𝑦) ∈ ℂ) |
2 | 1 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑚 · 𝑦) ∈ ℂ) |
3 | | mulcom 7896 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑚 · 𝑦) = (𝑦 · 𝑚)) |
4 | 3 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑚 · 𝑦) = (𝑦 · 𝑚)) |
5 | | mulass 7898 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑥) = (𝑚 · (𝑦 · 𝑥))) |
6 | 5 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑚 · 𝑦) · 𝑥) = (𝑚 · (𝑦 · 𝑥))) |
7 | | prodmolem3.5 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
8 | 7 | simpld 111 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
9 | | nnuz 9515 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
10 | 8, 9 | eleqtrdi 2263 |
. . 3
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
11 | | prodmolem3.6 |
. . . . . 6
⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
12 | | f1ocnv 5453 |
. . . . . 6
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ (𝜑 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
14 | | prodmolem3.7 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
15 | | f1oco 5463 |
. . . . 5
⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
16 | 13, 14, 15 | syl2anc 409 |
. . . 4
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
17 | 7 | ancomd 265 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ)) |
18 | 17, 14, 11 | nnf1o 11332 |
. . . . . 6
⊢ (𝜑 → 𝑀 = 𝑁) |
19 | 18 | oveq2d 5867 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = (1...𝑁)) |
20 | 19 | f1oeq2d 5436 |
. . . 4
⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) |
21 | 16, 20 | mpbird 166 |
. . 3
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀)) |
22 | | prodmodc.3 |
. . . . 5
⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) |
23 | | breq1 3990 |
. . . . . 6
⊢ (𝑗 = 𝑚 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑚 ≤ (♯‘𝐴))) |
24 | | fveq2 5494 |
. . . . . . 7
⊢ (𝑗 = 𝑚 → (𝑓‘𝑗) = (𝑓‘𝑚)) |
25 | 24 | csbeq1d 3056 |
. . . . . 6
⊢ (𝑗 = 𝑚 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
26 | 23, 25 | ifbieq1d 3547 |
. . . . 5
⊢ (𝑗 = 𝑚 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 1)) |
27 | | elnnuz 9516 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈
(ℤ≥‘1)) |
28 | 27 | biimpri 132 |
. . . . . 6
⊢ (𝑚 ∈
(ℤ≥‘1) → 𝑚 ∈ ℕ) |
29 | 28 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ 𝑚 ∈
ℕ) |
30 | | f1of 5440 |
. . . . . . . . . 10
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴) |
31 | 11, 30 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴) |
32 | 31 | ad2antrr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑓:(1...𝑀)⟶𝐴) |
33 | | 1zzd 9232 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) → 1
∈ ℤ) |
34 | 8 | nnzd 9326 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
35 | 34 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑀 ∈
ℤ) |
36 | | eluzelz 9489 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(ℤ≥‘1) → 𝑚 ∈ ℤ) |
37 | 36 | ad2antlr 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑚 ∈
ℤ) |
38 | 33, 35, 37 | 3jca 1172 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
(1 ∈ ℤ ∧ 𝑀
∈ ℤ ∧ 𝑚
∈ ℤ)) |
39 | | eluzle 9492 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(ℤ≥‘1) → 1 ≤ 𝑚) |
40 | 39 | ad2antlr 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) → 1
≤ 𝑚) |
41 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑚 ≤ (♯‘𝐴)) |
42 | 8 | nnnn0d 9181 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
43 | | hashfz1 10710 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
44 | 42, 43 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
45 | | 1zzd 9232 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℤ) |
46 | 45, 34 | fzfigd 10380 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
47 | 46, 11 | fihasheqf1od 10717 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘𝐴)) |
48 | 44, 47 | eqtr3d 2205 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 = (♯‘𝐴)) |
49 | 48 | ad2antrr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑀 = (♯‘𝐴)) |
50 | 41, 49 | breqtrrd 4015 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑚 ≤ 𝑀) |
51 | 40, 50 | jca 304 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
(1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑀)) |
52 | | elfz2 9965 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤
𝑚 ∧ 𝑚 ≤ 𝑀))) |
53 | 38, 51, 52 | sylanbrc 415 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑚 ∈ (1...𝑀)) |
54 | 32, 53 | ffvelrnd 5630 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
(𝑓‘𝑚) ∈ 𝐴) |
55 | | prodmo.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
56 | 55 | ralrimiva 2543 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
57 | 56 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
58 | | nfcsb1v 3082 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 |
59 | 58 | nfel1 2323 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
60 | | csbeq1a 3058 |
. . . . . . . . 9
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
61 | 60 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
62 | 59, 61 | rspc 2828 |
. . . . . . 7
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
63 | 54, 57, 62 | sylc 62 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
64 | | 1cnd 7929 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ ¬ 𝑚 ≤
(♯‘𝐴)) → 1
∈ ℂ) |
65 | 29 | nnzd 9326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ 𝑚 ∈
ℤ) |
66 | 48, 34 | eqeltrrd 2248 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐴) ∈
ℤ) |
67 | 66 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (♯‘𝐴)
∈ ℤ) |
68 | | zdcle 9281 |
. . . . . . 7
⊢ ((𝑚 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → DECID 𝑚 ≤ (♯‘𝐴)) |
69 | 65, 67, 68 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ DECID 𝑚 ≤ (♯‘𝐴)) |
70 | 63, 64, 69 | ifcldadc 3554 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ if(𝑚 ≤
(♯‘𝐴),
⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 1) ∈ ℂ) |
71 | 22, 26, 29, 70 | fvmptd3 5587 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐺‘𝑚) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 1)) |
72 | 71, 70 | eqeltrd 2247 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐺‘𝑚) ∈
ℂ) |
73 | | prodmodclem3.4 |
. . . . 5
⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1)) |
74 | | fveq2 5494 |
. . . . . . 7
⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚)) |
75 | 74 | csbeq1d 3056 |
. . . . . 6
⊢ (𝑗 = 𝑚 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
76 | 23, 75 | ifbieq1d 3547 |
. . . . 5
⊢ (𝑗 = 𝑚 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1)) |
77 | 14 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝐾:(1...𝑁)–1-1-onto→𝐴) |
78 | | f1of 5440 |
. . . . . . . . 9
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴) |
79 | 77, 78 | syl 14 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝐾:(1...𝑁)⟶𝐴) |
80 | 19 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
(1...𝑀) = (1...𝑁)) |
81 | 53, 80 | eleqtrd 2249 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
𝑚 ∈ (1...𝑁)) |
82 | 79, 81 | ffvelrnd 5630 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
(𝐾‘𝑚) ∈ 𝐴) |
83 | | nfcsb1v 3082 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 |
84 | 83 | nfel1 2323 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
85 | | csbeq1a 3058 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
86 | 85 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
87 | 84, 86 | rspc 2828 |
. . . . . . 7
⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
88 | 82, 57, 87 | sylc 62 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤
(♯‘𝐴)) →
⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
89 | 88, 64, 69 | ifcldadc 3554 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ if(𝑚 ≤
(♯‘𝐴),
⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1) ∈ ℂ) |
90 | 73, 76, 29, 89 | fvmptd3 5587 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐻‘𝑚) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1)) |
91 | 90, 89 | eqeltrd 2247 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐻‘𝑚) ∈
ℂ) |
92 | 19 | f1oeq2d 5436 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) |
93 | 14, 92 | mpbird 166 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴) |
94 | | f1of 5440 |
. . . . . . . . 9
⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴) |
95 | 93, 94 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴) |
96 | | fvco3 5565 |
. . . . . . . 8
⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
97 | 95, 96 | sylan 281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
98 | 97 | fveq2d 5498 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖)))) |
99 | 11 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
100 | 95 | ffvelrnda 5629 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴) |
101 | | f1ocnvfv2 5755 |
. . . . . . 7
⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
102 | 99, 100, 101 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
103 | 98, 102 | eqtrd 2203 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝐾‘𝑖)) |
104 | 103 | csbeq1d 3056 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
105 | | breq1 3990 |
. . . . . . 7
⊢ (𝑗 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑗 ≤ (♯‘𝐴) ↔ ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ (♯‘𝐴))) |
106 | | fveq2 5494 |
. . . . . . . 8
⊢ (𝑗 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑗) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
107 | 106 | csbeq1d 3056 |
. . . . . . 7
⊢ (𝑗 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
108 | 105, 107 | ifbieq1d 3547 |
. . . . . 6
⊢ (𝑗 = ((◡𝑓 ∘ 𝐾)‘𝑖) → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ (♯‘𝐴), ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 1)) |
109 | | f1of 5440 |
. . . . . . . . 9
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
110 | 21, 109 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
111 | 110 | ffvelrnda 5629 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀)) |
112 | | elfznn 10003 |
. . . . . . 7
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) |
113 | 111, 112 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) |
114 | | elfzle2 9977 |
. . . . . . . . . 10
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀) |
115 | 111, 114 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀) |
116 | 48 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑀 = (♯‘𝐴)) |
117 | 115, 116 | breqtrd 4013 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ (♯‘𝐴)) |
118 | 117 | iftrued 3532 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ (♯‘𝐴), ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 1) = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
119 | 56 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
120 | | nfcsb1v 3082 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝐾‘𝑖) / 𝑘⦌𝐵 |
121 | 120 | nfel1 2323 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ |
122 | | csbeq1a 3058 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑖) → 𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
123 | 122 | eleq1d 2239 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑖) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ)) |
124 | 121, 123 | rspc 2828 |
. . . . . . . . 9
⊢ ((𝐾‘𝑖) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ)) |
125 | 100, 119,
124 | sylc 62 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ) |
126 | 104, 125 | eqeltrd 2247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵 ∈ ℂ) |
127 | 118, 126 | eqeltrd 2247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ (♯‘𝐴), ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 1) ∈ ℂ) |
128 | 22, 108, 113, 127 | fvmptd3 5587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ (♯‘𝐴), ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 1)) |
129 | 128, 118 | eqtrd 2203 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
130 | | breq1 3990 |
. . . . . . 7
⊢ (𝑗 = 𝑖 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑖 ≤ (♯‘𝐴))) |
131 | | fveq2 5494 |
. . . . . . . 8
⊢ (𝑗 = 𝑖 → (𝐾‘𝑗) = (𝐾‘𝑖)) |
132 | 131 | csbeq1d 3056 |
. . . . . . 7
⊢ (𝑗 = 𝑖 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
133 | 130, 132 | ifbieq1d 3547 |
. . . . . 6
⊢ (𝑗 = 𝑖 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 1)) |
134 | | elfznn 10003 |
. . . . . . 7
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
135 | 134 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ ℕ) |
136 | | elfzle2 9977 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀) |
137 | 136 | adantl 275 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ≤ 𝑀) |
138 | 137, 116 | breqtrd 4013 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ≤ (♯‘𝐴)) |
139 | 138 | iftrued 3532 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(𝑖 ≤ (♯‘𝐴), ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
140 | 139, 125 | eqeltrd 2247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(𝑖 ≤ (♯‘𝐴), ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 1) ∈ ℂ) |
141 | 73, 133, 135, 140 | fvmptd3 5587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 1)) |
142 | 141, 139 | eqtrd 2203 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
143 | 104, 129,
142 | 3eqtr4rd 2214 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
144 | 2, 4, 6, 10, 21, 72, 91, 143 | seq3f1o 10453 |
. 2
⊢ (𝜑 → (seq1( · , 𝐻)‘𝑀) = (seq1( · , 𝐺)‘𝑀)) |
145 | 18 | fveq2d 5498 |
. 2
⊢ (𝜑 → (seq1( · , 𝐻)‘𝑀) = (seq1( · , 𝐻)‘𝑁)) |
146 | 144, 145 | eqtr3d 2205 |
1
⊢ (𝜑 → (seq1( · , 𝐺)‘𝑀) = (seq1( · , 𝐻)‘𝑁)) |