MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prodmolem2a Structured version   Visualization version   GIF version

Theorem prodmolem2a 15125
Description: Lemma for prodmo 15127. (Contributed by Scott Fenton, 4-Dec-2017.)
Hypotheses
Ref Expression
prodmo.1 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
prodmo.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
prodmo.3 𝐺 = (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵)
prodmolem2.4 𝐻 = (𝑗 ∈ ℕ ↦ (𝐾𝑗) / 𝑘𝐵)
prodmolem2.5 (𝜑𝑁 ∈ ℕ)
prodmolem2.6 (𝜑𝑀 ∈ ℤ)
prodmolem2.7 (𝜑𝐴 ⊆ (ℤ𝑀))
prodmolem2.8 (𝜑𝑓:(1...𝑁)–1-1-onto𝐴)
prodmolem2.9 (𝜑𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))
Assertion
Ref Expression
prodmolem2a (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))
Distinct variable groups:   𝐴,𝑘   𝑘,𝐹   𝜑,𝑘   𝐴,𝑗   𝐵,𝑗   𝑓,𝑗,𝑘   𝑗,𝐺   𝑗,𝑘,𝜑   𝑗,𝐾,𝑘   𝑗,𝑀,𝑘   𝑗,𝑁,𝑘
Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑓)   𝐵(𝑓,𝑘)   𝐹(𝑓,𝑗)   𝐺(𝑓,𝑘)   𝐻(𝑓,𝑗,𝑘)   𝐾(𝑓)   𝑀(𝑓)   𝑁(𝑓)

Proof of Theorem prodmolem2a
Dummy variables 𝑛 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodmo.1 . . 3 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
2 prodmo.2 . . 3 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
3 prodmolem2.7 . . . 4 (𝜑𝐴 ⊆ (ℤ𝑀))
4 prodmolem2.9 . . . . . . 7 (𝜑𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))
5 fzfid 13195 . . . . . . . . . . 11 (𝜑 → (1...𝑁) ∈ Fin)
6 prodmolem2.8 . . . . . . . . . . 11 (𝜑𝑓:(1...𝑁)–1-1-onto𝐴)
75, 6hasheqf1od 13568 . . . . . . . . . 10 (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
8 prodmolem2.5 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
98nnnn0d 11809 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ0)
10 hashfz1 13560 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
119, 10syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(1...𝑁)) = 𝑁)
127, 11eqtr3d 2835 . . . . . . . . 9 (𝜑 → (♯‘𝐴) = 𝑁)
1312oveq2d 7039 . . . . . . . 8 (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
14 isoeq4 6943 . . . . . . . 8 ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
1513, 14syl 17 . . . . . . 7 (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
164, 15mpbid 233 . . . . . 6 (𝜑𝐾 Isom < , < ((1...𝑁), 𝐴))
17 isof1o 6946 . . . . . 6 (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto𝐴)
18 f1of 6490 . . . . . 6 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:(1...𝑁)⟶𝐴)
1916, 17, 183syl 18 . . . . 5 (𝜑𝐾:(1...𝑁)⟶𝐴)
20 nnuz 12134 . . . . . . 7 ℕ = (ℤ‘1)
218, 20syl6eleq 2895 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘1))
22 eluzfz2 12769 . . . . . 6 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2321, 22syl 17 . . . . 5 (𝜑𝑁 ∈ (1...𝑁))
2419, 23ffvelrnd 6724 . . . 4 (𝜑 → (𝐾𝑁) ∈ 𝐴)
253, 24sseldd 3896 . . 3 (𝜑 → (𝐾𝑁) ∈ (ℤ𝑀))
263sselda 3895 . . . . . 6 ((𝜑𝑗𝐴) → 𝑗 ∈ (ℤ𝑀))
2716, 17syl 17 . . . . . . . . 9 (𝜑𝐾:(1...𝑁)–1-1-onto𝐴)
28 f1ocnvfv2 6906 . . . . . . . . 9 ((𝐾:(1...𝑁)–1-1-onto𝐴𝑗𝐴) → (𝐾‘(𝐾𝑗)) = 𝑗)
2927, 28sylan 580 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝐾‘(𝐾𝑗)) = 𝑗)
30 f1ocnv 6502 . . . . . . . . . . . 12 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:𝐴1-1-onto→(1...𝑁))
31 f1of 6490 . . . . . . . . . . . 12 (𝐾:𝐴1-1-onto→(1...𝑁) → 𝐾:𝐴⟶(1...𝑁))
3227, 30, 313syl 18 . . . . . . . . . . 11 (𝜑𝐾:𝐴⟶(1...𝑁))
3332ffvelrnda 6723 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝐾𝑗) ∈ (1...𝑁))
34 elfzle2 12765 . . . . . . . . . 10 ((𝐾𝑗) ∈ (1...𝑁) → (𝐾𝑗) ≤ 𝑁)
3533, 34syl 17 . . . . . . . . 9 ((𝜑𝑗𝐴) → (𝐾𝑗) ≤ 𝑁)
3616adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
37 fzssuz 12802 . . . . . . . . . . . . 13 (1...𝑁) ⊆ (ℤ‘1)
38 uzssz 12117 . . . . . . . . . . . . . 14 (ℤ‘1) ⊆ ℤ
39 zssre 11842 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
4038, 39sstri 3904 . . . . . . . . . . . . 13 (ℤ‘1) ⊆ ℝ
4137, 40sstri 3904 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
42 ressxr 10538 . . . . . . . . . . . 12 ℝ ⊆ ℝ*
4341, 42sstri 3904 . . . . . . . . . . 11 (1...𝑁) ⊆ ℝ*
4443a1i 11 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (1...𝑁) ⊆ ℝ*)
45 uzssz 12117 . . . . . . . . . . . . . 14 (ℤ𝑀) ⊆ ℤ
4645, 39sstri 3904 . . . . . . . . . . . . 13 (ℤ𝑀) ⊆ ℝ
4746, 42sstri 3904 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℝ*
483, 47syl6ss 3907 . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℝ*)
4948adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐴 ⊆ ℝ*)
5023adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝑁 ∈ (1...𝑁))
51 leisorel 13670 . . . . . . . . . 10 ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ ((𝐾𝑗) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((𝐾𝑗) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑗)) ≤ (𝐾𝑁)))
5236, 44, 49, 33, 50, 51syl122anc 1372 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝐾𝑗) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑗)) ≤ (𝐾𝑁)))
5335, 52mpbid 233 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝐾‘(𝐾𝑗)) ≤ (𝐾𝑁))
5429, 53eqbrtrrd 4992 . . . . . . 7 ((𝜑𝑗𝐴) → 𝑗 ≤ (𝐾𝑁))
553, 45syl6ss 3907 . . . . . . . . 9 (𝜑𝐴 ⊆ ℤ)
5655sselda 3895 . . . . . . . 8 ((𝜑𝑗𝐴) → 𝑗 ∈ ℤ)
57 eluzelz 12107 . . . . . . . . . 10 ((𝐾𝑁) ∈ (ℤ𝑀) → (𝐾𝑁) ∈ ℤ)
5825, 57syl 17 . . . . . . . . 9 (𝜑 → (𝐾𝑁) ∈ ℤ)
5958adantr 481 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝐾𝑁) ∈ ℤ)
60 eluz 12111 . . . . . . . 8 ((𝑗 ∈ ℤ ∧ (𝐾𝑁) ∈ ℤ) → ((𝐾𝑁) ∈ (ℤ𝑗) ↔ 𝑗 ≤ (𝐾𝑁)))
6156, 59, 60syl2anc 584 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐾𝑁) ∈ (ℤ𝑗) ↔ 𝑗 ≤ (𝐾𝑁)))
6254, 61mpbird 258 . . . . . 6 ((𝜑𝑗𝐴) → (𝐾𝑁) ∈ (ℤ𝑗))
63 elfzuzb 12756 . . . . . 6 (𝑗 ∈ (𝑀...(𝐾𝑁)) ↔ (𝑗 ∈ (ℤ𝑀) ∧ (𝐾𝑁) ∈ (ℤ𝑗)))
6426, 62, 63sylanbrc 583 . . . . 5 ((𝜑𝑗𝐴) → 𝑗 ∈ (𝑀...(𝐾𝑁)))
6564ex 413 . . . 4 (𝜑 → (𝑗𝐴𝑗 ∈ (𝑀...(𝐾𝑁))))
6665ssrdv 3901 . . 3 (𝜑𝐴 ⊆ (𝑀...(𝐾𝑁)))
671, 2, 25, 66fprodcvg 15121 . 2 (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾𝑁)))
68 mulid2 10493 . . . . 5 (𝑚 ∈ ℂ → (1 · 𝑚) = 𝑚)
6968adantl 482 . . . 4 ((𝜑𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚)
70 mulid1 10492 . . . . 5 (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚)
7170adantl 482 . . . 4 ((𝜑𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚)
72 mulcl 10474 . . . . 5 ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ)
7372adantl 482 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ)
74 1cnd 10489 . . . 4 (𝜑 → 1 ∈ ℂ)
7523, 13eleqtrrd 2888 . . . 4 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
76 iftrue 4393 . . . . . . . . . . 11 (𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) = 𝐵)
7776adantl 482 . . . . . . . . . 10 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 1) = 𝐵)
7877, 2eqeltrd 2885 . . . . . . . . 9 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
7978ex 413 . . . . . . . 8 (𝜑 → (𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ))
80 iffalse 4396 . . . . . . . . 9 𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) = 1)
81 ax-1cn 10448 . . . . . . . . 9 1 ∈ ℂ
8280, 81syl6eqel 2893 . . . . . . . 8 𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
8379, 82pm2.61d1 181 . . . . . . 7 (𝜑 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
8483adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℤ) → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
8584, 1fmptd 6748 . . . . 5 (𝜑𝐹:ℤ⟶ℂ)
86 elfzelz 12762 . . . . 5 (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
87 ffvelrn 6721 . . . . 5 ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹𝑚) ∈ ℂ)
8885, 86, 87syl2an 595 . . . 4 ((𝜑𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴)))) → (𝐹𝑚) ∈ ℂ)
89 fveqeq2 6554 . . . . . 6 (𝑘 = 𝑚 → ((𝐹𝑘) = 1 ↔ (𝐹𝑚) = 1))
90 fzssz 12763 . . . . . . . . 9 (𝑀...(𝐾‘(♯‘𝐴))) ⊆ ℤ
91 eldifi 4030 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
9290, 91sseldi 3893 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
93 eldifn 4031 . . . . . . . . . 10 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘𝐴)
9493, 80syl 17 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 1) = 1)
9594, 81syl6eqel 2893 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
961fvmpt2 6652 . . . . . . . 8 ((𝑘 ∈ ℤ ∧ if(𝑘𝐴, 𝐵, 1) ∈ ℂ) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
9792, 95, 96syl2anc 584 . . . . . . 7 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
9897, 94eqtrd 2833 . . . . . 6 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = 1)
9989, 98vtoclga 3519 . . . . 5 (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑚) = 1)
10099adantl 482 . . . 4 ((𝜑𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑚) = 1)
101 isof1o 6946 . . . . . . . 8 (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto𝐴)
102 f1of 6490 . . . . . . . 8 (𝐾:(1...(♯‘𝐴))–1-1-onto𝐴𝐾:(1...(♯‘𝐴))⟶𝐴)
1034, 101, 1023syl 18 . . . . . . 7 (𝜑𝐾:(1...(♯‘𝐴))⟶𝐴)
104103ffvelrnda 6723 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ 𝐴)
105104iftrued 4395 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) = (𝐾𝑥) / 𝑘𝐵)
10655adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ)
107106, 104sseldd 3896 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ ℤ)
108 nfv 1896 . . . . . . . . 9 𝑘𝜑
109 nfv 1896 . . . . . . . . . . 11 𝑘(𝐾𝑥) ∈ 𝐴
110 nfcsb1v 3839 . . . . . . . . . . 11 𝑘(𝐾𝑥) / 𝑘𝐵
111 nfcv 2951 . . . . . . . . . . 11 𝑘1
112109, 110, 111nfif 4416 . . . . . . . . . 10 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1)
113112nfel1 2965 . . . . . . . . 9 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ
114108, 113nfim 1882 . . . . . . . 8 𝑘(𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)
115 fvex 6558 . . . . . . . 8 (𝐾𝑥) ∈ V
116 eleq1 2872 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → (𝑘𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
117 csbeq1a 3830 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → 𝐵 = (𝐾𝑥) / 𝑘𝐵)
118116, 117ifbieq1d 4410 . . . . . . . . . 10 (𝑘 = (𝐾𝑥) → if(𝑘𝐴, 𝐵, 1) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
119118eleq1d 2869 . . . . . . . . 9 (𝑘 = (𝐾𝑥) → (if(𝑘𝐴, 𝐵, 1) ∈ ℂ ↔ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ))
120119imbi2d 342 . . . . . . . 8 (𝑘 = (𝐾𝑥) → ((𝜑 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ) ↔ (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)))
121114, 115, 120, 83vtoclf 3504 . . . . . . 7 (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)
122121adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)
123 eleq1 2872 . . . . . . . 8 (𝑛 = (𝐾𝑥) → (𝑛𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
124 csbeq1 3820 . . . . . . . 8 (𝑛 = (𝐾𝑥) → 𝑛 / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
125123, 124ifbieq1d 4410 . . . . . . 7 (𝑛 = (𝐾𝑥) → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
126 nfcv 2951 . . . . . . . . 9 𝑛if(𝑘𝐴, 𝐵, 1)
127 nfv 1896 . . . . . . . . . 10 𝑘 𝑛𝐴
128 nfcsb1v 3839 . . . . . . . . . 10 𝑘𝑛 / 𝑘𝐵
129127, 128, 111nfif 4416 . . . . . . . . 9 𝑘if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1)
130 eleq1 2872 . . . . . . . . . 10 (𝑘 = 𝑛 → (𝑘𝐴𝑛𝐴))
131 csbeq1a 3830 . . . . . . . . . 10 (𝑘 = 𝑛𝐵 = 𝑛 / 𝑘𝐵)
132130, 131ifbieq1d 4410 . . . . . . . . 9 (𝑘 = 𝑛 → if(𝑘𝐴, 𝐵, 1) = if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1))
133126, 129, 132cbvmpt 5067 . . . . . . . 8 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1))
1341, 133eqtri 2821 . . . . . . 7 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1))
135125, 134fvmptg 6640 . . . . . 6 (((𝐾𝑥) ∈ ℤ ∧ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
136107, 122, 135syl2anc 584 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
137 elfznn 12790 . . . . . 6 (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
138105, 122eqeltrrd 2886 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) / 𝑘𝐵 ∈ ℂ)
139 fveq2 6545 . . . . . . . 8 (𝑗 = 𝑥 → (𝐾𝑗) = (𝐾𝑥))
140139csbeq1d 3821 . . . . . . 7 (𝑗 = 𝑥(𝐾𝑗) / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
141 prodmolem2.4 . . . . . . 7 𝐻 = (𝑗 ∈ ℕ ↦ (𝐾𝑗) / 𝑘𝐵)
142140, 141fvmptg 6640 . . . . . 6 ((𝑥 ∈ ℕ ∧ (𝐾𝑥) / 𝑘𝐵 ∈ ℂ) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
143137, 138, 142syl2an2 682 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
144105, 136, 1433eqtr4rd 2844 . . . 4 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐹‘(𝐾𝑥)))
14569, 71, 73, 74, 4, 75, 3, 88, 100, 144seqcoll 13674 . . 3 (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾𝑁)) = (seq1( · , 𝐻)‘𝑁))
146 prodmo.3 . . . 4 𝐺 = (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵)
1478, 8jca 512 . . . 4 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
1481, 2, 146, 141, 147, 6, 27prodmolem3 15124 . . 3 (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁))
149145, 148eqtr4d 2836 . 2 (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾𝑁)) = (seq1( · , 𝐺)‘𝑁))
15067, 149breqtrd 4994 1 (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1525  wcel 2083  csb 3817  cdif 3862  wss 3865  ifcif 4387   class class class wbr 4968  cmpt 5047  ccnv 5449  wf 6228  1-1-ontowf1o 6231  cfv 6232   Isom wiso 6233  (class class class)co 7023  Fincfn 8364  cc 10388  cr 10389  1c1 10391   · cmul 10395  *cxr 10527   < clt 10528  cle 10529  cn 11492  0cn0 11751  cz 11835  cuz 12097  ...cfz 12746  seqcseq 13223  chash 13544  cli 14679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-n0 11752  df-z 11836  df-uz 12098  df-rp 12244  df-fz 12747  df-fzo 12888  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-clim 14683
This theorem is referenced by:  prodmolem2  15126  zprod  15128
  Copyright terms: Public domain W3C validator