| 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 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
| 6 | | prodmolem2.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴) |
| 7 | 5, 6 | hasheqf1od 14392 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴)) |
| 8 | | prodmolem2.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 9 | 8 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 10 | | hashfz1 14385 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) |
| 12 | 7, 11 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐴) = 𝑁) |
| 13 | 12 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁)) |
| 14 | | isoeq4 7340 |
. . . . . . . 8
⊢
((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
| 15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
| 16 | 4, 15 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
| 17 | | isof1o 7343 |
. . . . . 6
⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
| 18 | | f1of 6848 |
. . . . . 6
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴) |
| 19 | 16, 17, 18 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴) |
| 20 | | nnuz 12921 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
| 21 | 8, 20 | eleqtrdi 2851 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
| 22 | | eluzfz2 13572 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
| 23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
| 24 | 19, 23 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴) |
| 25 | 3, 24 | sseldd 3984 |
. . 3
⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀)) |
| 26 | 3 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 27 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
| 28 | | f1ocnvfv2 7297 |
. . . . . . . . 9
⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑗 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑗)) = 𝑗) |
| 29 | 27, 28 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑗)) = 𝑗) |
| 30 | | f1ocnv 6860 |
. . . . . . . . . . . 12
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁)) |
| 31 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁)) |
| 32 | 27, 30, 31 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁)) |
| 33 | 32 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (◡𝐾‘𝑗) ∈ (1...𝑁)) |
| 34 | | elfzle2 13568 |
. . . . . . . . . 10
⊢ ((◡𝐾‘𝑗) ∈ (1...𝑁) → (◡𝐾‘𝑗) ≤ 𝑁) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (◡𝐾‘𝑗) ≤ 𝑁) |
| 36 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
| 37 | | fzssuz 13605 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
(ℤ≥‘1) |
| 38 | | uzssz 12899 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) ⊆ ℤ |
| 39 | | zssre 12620 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
| 40 | 38, 39 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘1) ⊆ ℝ |
| 41 | 37, 40 | sstri 3993 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
ℝ |
| 42 | | ressxr 11305 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
| 43 | 41, 42 | sstri 3993 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℝ* |
| 44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (1...𝑁) ⊆
ℝ*) |
| 45 | | uzssz 12899 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 46 | 45, 39 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
| 47 | 46, 42 | sstri 3993 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑀) ⊆
ℝ* |
| 48 | 3, 47 | sstrdi 3996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
| 49 | 48 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐴 ⊆
ℝ*) |
| 50 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑁 ∈ (1...𝑁)) |
| 51 | | leisorel 14499 |
. . . . . . . . . 10
⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*)
∧ ((◡𝐾‘𝑗) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑗) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑗)) ≤ (𝐾‘𝑁))) |
| 52 | 36, 44, 49, 33, 50, 51 | syl122anc 1381 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((◡𝐾‘𝑗) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑗)) ≤ (𝐾‘𝑁))) |
| 53 | 35, 52 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑗)) ≤ (𝐾‘𝑁)) |
| 54 | 29, 53 | eqbrtrrd 5167 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ≤ (𝐾‘𝑁)) |
| 55 | 3, 45 | sstrdi 3996 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℤ) |
| 56 | 55 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ ℤ) |
| 57 | | eluzelz 12888 |
. . . . . . . . . 10
⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ) |
| 58 | 25, 57 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ) |
| 59 | 58 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ) |
| 60 | | eluz 12892 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑗) ↔ 𝑗 ≤ (𝐾‘𝑁))) |
| 61 | 56, 59, 60 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑗) ↔ 𝑗 ≤ (𝐾‘𝑁))) |
| 62 | 54, 61 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑗)) |
| 63 | | elfzuzb 13558 |
. . . . . 6
⊢ (𝑗 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑗 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑗))) |
| 64 | 26, 62, 63 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ (𝑀...(𝐾‘𝑁))) |
| 65 | 64 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐴 → 𝑗 ∈ (𝑀...(𝐾‘𝑁)))) |
| 66 | 65 | ssrdv 3989 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁))) |
| 67 | 1, 2, 25, 66 | fprodcvg 15966 |
. 2
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾‘𝑁))) |
| 68 | | mullid 11260 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (1
· 𝑚) = 𝑚) |
| 69 | 68 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚) |
| 70 | | mulrid 11259 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚) |
| 71 | 70 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚) |
| 72 | | mulcl 11239 |
. . . . 5
⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ) |
| 73 | 72 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ) |
| 74 | | 1cnd 11256 |
. . . 4
⊢ (𝜑 → 1 ∈
ℂ) |
| 75 | 23, 13 | eleqtrrd 2844 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴))) |
| 76 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
| 77 | 76 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵) |
| 78 | 77, 2 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
| 79 | 78 | ex 412 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)) |
| 80 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
| 81 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 82 | 80, 81 | eqeltrdi 2849 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
| 83 | 79, 82 | pm2.61d1 180 |
. . . . . . 7
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
| 84 | 83 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
| 85 | 84, 1 | fmptd 7134 |
. . . . 5
⊢ (𝜑 → 𝐹:ℤ⟶ℂ) |
| 86 | | elfzelz 13564 |
. . . . 5
⊢ (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ) |
| 87 | | ffvelcdm 7101 |
. . . . 5
⊢ ((𝐹:ℤ⟶ℂ ∧
𝑚 ∈ ℤ) →
(𝐹‘𝑚) ∈ ℂ) |
| 88 | 85, 86, 87 | syl2an 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴)))) → (𝐹‘𝑚) ∈ ℂ) |
| 89 | | fveqeq2 6915 |
. . . . . 6
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 1 ↔ (𝐹‘𝑚) = 1)) |
| 90 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴)))) |
| 91 | 90 | elfzelzd 13565 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ) |
| 92 | | eldifn 4132 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
| 93 | 92, 80 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1) |
| 94 | 93, 81 | eqeltrdi 2849 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) |
| 95 | 1 | fvmpt2 7027 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
| 96 | 91, 94, 95 | syl2anc 584 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) |
| 97 | 96, 93 | eqtrd 2777 |
. . . . . 6
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 1) |
| 98 | 89, 97 | vtoclga 3577 |
. . . . 5
⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 1) |
| 99 | 98 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 1) |
| 100 | | isof1o 7343 |
. . . . . . . 8
⊢ (𝐾 Isom < , <
((1...(♯‘𝐴)),
𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 101 | | f1of 6848 |
. . . . . . . 8
⊢ (𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(♯‘𝐴))⟶𝐴) |
| 102 | 4, 100, 101 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐾:(1...(♯‘𝐴))⟶𝐴) |
| 103 | 102 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴) |
| 104 | 103 | iftrued 4533 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
| 105 | 55 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ) |
| 106 | 105, 103 | sseldd 3984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ) |
| 107 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝜑 |
| 108 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴 |
| 109 | | nfcsb1v 3923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 |
| 110 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘1 |
| 111 | 108, 109,
110 | nfif 4556 |
. . . . . . . . . 10
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) |
| 112 | 111 | nfel1 2922 |
. . . . . . . . 9
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ |
| 113 | 107, 112 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) |
| 114 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐾‘𝑥) ∈ V |
| 115 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
| 116 | | csbeq1a 3913 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
| 117 | 115, 116 | ifbieq1d 4550 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
| 118 | 117 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)) |
| 119 | 118 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) ↔ (𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ))) |
| 120 | 113, 114,
119, 83 | vtoclf 3564 |
. . . . . . 7
⊢ (𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) |
| 121 | 120 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) |
| 122 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
| 123 | | csbeq1 3902 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
| 124 | 122, 123 | ifbieq1d 4550 |
. . . . . . 7
⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
| 125 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 1) |
| 126 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ 𝐴 |
| 127 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵 |
| 128 | 126, 127,
110 | nfif 4556 |
. . . . . . . . 9
⊢
Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1) |
| 129 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴)) |
| 130 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵) |
| 131 | 129, 130 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
| 132 | 125, 128,
131 | cbvmpt 5253 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
| 133 | 1, 132 | eqtri 2765 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 1)) |
| 134 | 124, 133 | fvmptg 7014 |
. . . . . 6
⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
| 135 | 106, 121,
134 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)) |
| 136 | | elfznn 13593 |
. . . . . 6
⊢ (𝑥 ∈
(1...(♯‘𝐴))
→ 𝑥 ∈
ℕ) |
| 137 | 104, 121 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ) |
| 138 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → (𝐾‘𝑗) = (𝐾‘𝑥)) |
| 139 | 138 | csbeq1d 3903 |
. . . . . . 7
⊢ (𝑗 = 𝑥 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
| 140 | | prodmolem2.4 |
. . . . . . 7
⊢ 𝐻 = (𝑗 ∈ ℕ ↦ ⦋(𝐾‘𝑗) / 𝑘⦌𝐵) |
| 141 | 139, 140 | fvmptg 7014 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧
⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
| 142 | 136, 137,
141 | syl2an2 686 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
| 143 | 104, 135,
142 | 3eqtr4rd 2788 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥))) |
| 144 | 69, 71, 73, 74, 4, 75, 3, 88, 99, 143 | seqcoll 14503 |
. . 3
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐻)‘𝑁)) |
| 145 | | prodmo.3 |
. . . 4
⊢ 𝐺 = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵) |
| 146 | 8, 8 | jca 511 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
| 147 | 1, 2, 145, 140, 146, 6, 27 | prodmolem3 15969 |
. . 3
⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁)) |
| 148 | 144, 147 | eqtr4d 2780 |
. 2
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐺)‘𝑁)) |
| 149 | 67, 148 | breqtrd 5169 |
1
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁)) |