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

Theorem prodmolem2a 15875
Description: Lemma for prodmo 15877. (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 13935 . . . . . . . . . . 11 (𝜑 → (1...𝑁) ∈ Fin)
6 prodmolem2.8 . . . . . . . . . . 11 (𝜑𝑓:(1...𝑁)–1-1-onto𝐴)
75, 6hasheqf1od 14310 . . . . . . . . . 10 (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
8 prodmolem2.5 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
98nnnn0d 12529 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ0)
10 hashfz1 14303 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
119, 10syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(1...𝑁)) = 𝑁)
127, 11eqtr3d 2766 . . . . . . . . 9 (𝜑 → (♯‘𝐴) = 𝑁)
1312oveq2d 7417 . . . . . . . 8 (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
14 isoeq4 7309 . . . . . . . 8 ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
1513, 14syl 17 . . . . . . 7 (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
164, 15mpbid 231 . . . . . 6 (𝜑𝐾 Isom < , < ((1...𝑁), 𝐴))
17 isof1o 7312 . . . . . 6 (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto𝐴)
18 f1of 6823 . . . . . 6 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:(1...𝑁)⟶𝐴)
1916, 17, 183syl 18 . . . . 5 (𝜑𝐾:(1...𝑁)⟶𝐴)
20 nnuz 12862 . . . . . . 7 ℕ = (ℤ‘1)
218, 20eleqtrdi 2835 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘1))
22 eluzfz2 13506 . . . . . 6 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2321, 22syl 17 . . . . 5 (𝜑𝑁 ∈ (1...𝑁))
2419, 23ffvelcdmd 7077 . . . 4 (𝜑 → (𝐾𝑁) ∈ 𝐴)
253, 24sseldd 3975 . . 3 (𝜑 → (𝐾𝑁) ∈ (ℤ𝑀))
263sselda 3974 . . . . . 6 ((𝜑𝑗𝐴) → 𝑗 ∈ (ℤ𝑀))
2716, 17syl 17 . . . . . . . . 9 (𝜑𝐾:(1...𝑁)–1-1-onto𝐴)
28 f1ocnvfv2 7267 . . . . . . . . 9 ((𝐾:(1...𝑁)–1-1-onto𝐴𝑗𝐴) → (𝐾‘(𝐾𝑗)) = 𝑗)
2927, 28sylan 579 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝐾‘(𝐾𝑗)) = 𝑗)
30 f1ocnv 6835 . . . . . . . . . . . 12 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:𝐴1-1-onto→(1...𝑁))
31 f1of 6823 . . . . . . . . . . . 12 (𝐾:𝐴1-1-onto→(1...𝑁) → 𝐾:𝐴⟶(1...𝑁))
3227, 30, 313syl 18 . . . . . . . . . . 11 (𝜑𝐾:𝐴⟶(1...𝑁))
3332ffvelcdmda 7076 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝐾𝑗) ∈ (1...𝑁))
34 elfzle2 13502 . . . . . . . . . 10 ((𝐾𝑗) ∈ (1...𝑁) → (𝐾𝑗) ≤ 𝑁)
3533, 34syl 17 . . . . . . . . 9 ((𝜑𝑗𝐴) → (𝐾𝑗) ≤ 𝑁)
3616adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
37 fzssuz 13539 . . . . . . . . . . . . 13 (1...𝑁) ⊆ (ℤ‘1)
38 uzssz 12840 . . . . . . . . . . . . . 14 (ℤ‘1) ⊆ ℤ
39 zssre 12562 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
4038, 39sstri 3983 . . . . . . . . . . . . 13 (ℤ‘1) ⊆ ℝ
4137, 40sstri 3983 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
42 ressxr 11255 . . . . . . . . . . . 12 ℝ ⊆ ℝ*
4341, 42sstri 3983 . . . . . . . . . . 11 (1...𝑁) ⊆ ℝ*
4443a1i 11 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (1...𝑁) ⊆ ℝ*)
45 uzssz 12840 . . . . . . . . . . . . . 14 (ℤ𝑀) ⊆ ℤ
4645, 39sstri 3983 . . . . . . . . . . . . 13 (ℤ𝑀) ⊆ ℝ
4746, 42sstri 3983 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℝ*
483, 47sstrdi 3986 . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℝ*)
4948adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐴 ⊆ ℝ*)
5023adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝑁 ∈ (1...𝑁))
51 leisorel 14418 . . . . . . . . . 10 ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ ((𝐾𝑗) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((𝐾𝑗) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑗)) ≤ (𝐾𝑁)))
5236, 44, 49, 33, 50, 51syl122anc 1376 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝐾𝑗) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑗)) ≤ (𝐾𝑁)))
5335, 52mpbid 231 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝐾‘(𝐾𝑗)) ≤ (𝐾𝑁))
5429, 53eqbrtrrd 5162 . . . . . . 7 ((𝜑𝑗𝐴) → 𝑗 ≤ (𝐾𝑁))
553, 45sstrdi 3986 . . . . . . . . 9 (𝜑𝐴 ⊆ ℤ)
5655sselda 3974 . . . . . . . 8 ((𝜑𝑗𝐴) → 𝑗 ∈ ℤ)
57 eluzelz 12829 . . . . . . . . . 10 ((𝐾𝑁) ∈ (ℤ𝑀) → (𝐾𝑁) ∈ ℤ)
5825, 57syl 17 . . . . . . . . 9 (𝜑 → (𝐾𝑁) ∈ ℤ)
5958adantr 480 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝐾𝑁) ∈ ℤ)
60 eluz 12833 . . . . . . . 8 ((𝑗 ∈ ℤ ∧ (𝐾𝑁) ∈ ℤ) → ((𝐾𝑁) ∈ (ℤ𝑗) ↔ 𝑗 ≤ (𝐾𝑁)))
6156, 59, 60syl2anc 583 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐾𝑁) ∈ (ℤ𝑗) ↔ 𝑗 ≤ (𝐾𝑁)))
6254, 61mpbird 257 . . . . . 6 ((𝜑𝑗𝐴) → (𝐾𝑁) ∈ (ℤ𝑗))
63 elfzuzb 13492 . . . . . 6 (𝑗 ∈ (𝑀...(𝐾𝑁)) ↔ (𝑗 ∈ (ℤ𝑀) ∧ (𝐾𝑁) ∈ (ℤ𝑗)))
6426, 62, 63sylanbrc 582 . . . . 5 ((𝜑𝑗𝐴) → 𝑗 ∈ (𝑀...(𝐾𝑁)))
6564ex 412 . . . 4 (𝜑 → (𝑗𝐴𝑗 ∈ (𝑀...(𝐾𝑁))))
6665ssrdv 3980 . . 3 (𝜑𝐴 ⊆ (𝑀...(𝐾𝑁)))
671, 2, 25, 66fprodcvg 15871 . 2 (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾𝑁)))
68 mullid 11210 . . . . 5 (𝑚 ∈ ℂ → (1 · 𝑚) = 𝑚)
6968adantl 481 . . . 4 ((𝜑𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚)
70 mulrid 11209 . . . . 5 (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚)
7170adantl 481 . . . 4 ((𝜑𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚)
72 mulcl 11190 . . . . 5 ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ)
7372adantl 481 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ)
74 1cnd 11206 . . . 4 (𝜑 → 1 ∈ ℂ)
7523, 13eleqtrrd 2828 . . . 4 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
76 iftrue 4526 . . . . . . . . . . 11 (𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) = 𝐵)
7776adantl 481 . . . . . . . . . 10 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 1) = 𝐵)
7877, 2eqeltrd 2825 . . . . . . . . 9 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
7978ex 412 . . . . . . . 8 (𝜑 → (𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ))
80 iffalse 4529 . . . . . . . . 9 𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) = 1)
81 ax-1cn 11164 . . . . . . . . 9 1 ∈ ℂ
8280, 81eqeltrdi 2833 . . . . . . . 8 𝑘𝐴 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
8379, 82pm2.61d1 180 . . . . . . 7 (𝜑 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
8483adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℤ) → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
8584, 1fmptd 7105 . . . . 5 (𝜑𝐹:ℤ⟶ℂ)
86 elfzelz 13498 . . . . 5 (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
87 ffvelcdm 7073 . . . . 5 ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹𝑚) ∈ ℂ)
8885, 86, 87syl2an 595 . . . 4 ((𝜑𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴)))) → (𝐹𝑚) ∈ ℂ)
89 fveqeq2 6890 . . . . . 6 (𝑘 = 𝑚 → ((𝐹𝑘) = 1 ↔ (𝐹𝑚) = 1))
90 eldifi 4118 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
9190elfzelzd 13499 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
92 eldifn 4119 . . . . . . . . . 10 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘𝐴)
9392, 80syl 17 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 1) = 1)
9493, 81eqeltrdi 2833 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 1) ∈ ℂ)
951fvmpt2 6999 . . . . . . . 8 ((𝑘 ∈ ℤ ∧ if(𝑘𝐴, 𝐵, 1) ∈ ℂ) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
9691, 94, 95syl2anc 583 . . . . . . 7 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 1))
9796, 93eqtrd 2764 . . . . . 6 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = 1)
9889, 97vtoclga 3558 . . . . 5 (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑚) = 1)
9998adantl 481 . . . 4 ((𝜑𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑚) = 1)
100 isof1o 7312 . . . . . . . 8 (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto𝐴)
101 f1of 6823 . . . . . . . 8 (𝐾:(1...(♯‘𝐴))–1-1-onto𝐴𝐾:(1...(♯‘𝐴))⟶𝐴)
1024, 100, 1013syl 18 . . . . . . 7 (𝜑𝐾:(1...(♯‘𝐴))⟶𝐴)
103102ffvelcdmda 7076 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ 𝐴)
104103iftrued 4528 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) = (𝐾𝑥) / 𝑘𝐵)
10555adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ)
106105, 103sseldd 3975 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ ℤ)
107 nfv 1909 . . . . . . . . 9 𝑘𝜑
108 nfv 1909 . . . . . . . . . . 11 𝑘(𝐾𝑥) ∈ 𝐴
109 nfcsb1v 3910 . . . . . . . . . . 11 𝑘(𝐾𝑥) / 𝑘𝐵
110 nfcv 2895 . . . . . . . . . . 11 𝑘1
111108, 109, 110nfif 4550 . . . . . . . . . 10 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1)
112111nfel1 2911 . . . . . . . . 9 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ
113107, 112nfim 1891 . . . . . . . 8 𝑘(𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)
114 fvex 6894 . . . . . . . 8 (𝐾𝑥) ∈ V
115 eleq1 2813 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → (𝑘𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
116 csbeq1a 3899 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → 𝐵 = (𝐾𝑥) / 𝑘𝐵)
117115, 116ifbieq1d 4544 . . . . . . . . . 10 (𝑘 = (𝐾𝑥) → if(𝑘𝐴, 𝐵, 1) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
118117eleq1d 2810 . . . . . . . . 9 (𝑘 = (𝐾𝑥) → (if(𝑘𝐴, 𝐵, 1) ∈ ℂ ↔ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ))
119118imbi2d 340 . . . . . . . 8 (𝑘 = (𝐾𝑥) → ((𝜑 → if(𝑘𝐴, 𝐵, 1) ∈ ℂ) ↔ (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)))
120113, 114, 119, 83vtoclf 3544 . . . . . . 7 (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)
121120adantr 480 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ)
122 eleq1 2813 . . . . . . . 8 (𝑛 = (𝐾𝑥) → (𝑛𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
123 csbeq1 3888 . . . . . . . 8 (𝑛 = (𝐾𝑥) → 𝑛 / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
124122, 123ifbieq1d 4544 . . . . . . 7 (𝑛 = (𝐾𝑥) → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
125 nfcv 2895 . . . . . . . . 9 𝑛if(𝑘𝐴, 𝐵, 1)
126 nfv 1909 . . . . . . . . . 10 𝑘 𝑛𝐴
127 nfcsb1v 3910 . . . . . . . . . 10 𝑘𝑛 / 𝑘𝐵
128126, 127, 110nfif 4550 . . . . . . . . 9 𝑘if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1)
129 eleq1 2813 . . . . . . . . . 10 (𝑘 = 𝑛 → (𝑘𝐴𝑛𝐴))
130 csbeq1a 3899 . . . . . . . . . 10 (𝑘 = 𝑛𝐵 = 𝑛 / 𝑘𝐵)
131129, 130ifbieq1d 4544 . . . . . . . . 9 (𝑘 = 𝑛 → if(𝑘𝐴, 𝐵, 1) = if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1))
132125, 128, 131cbvmpt 5249 . . . . . . . 8 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1))
1331, 132eqtri 2752 . . . . . . 7 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 1))
134124, 133fvmptg 6986 . . . . . 6 (((𝐾𝑥) ∈ ℤ ∧ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
135106, 121, 134syl2anc 583 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 1))
136 elfznn 13527 . . . . . 6 (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
137104, 121eqeltrrd 2826 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) / 𝑘𝐵 ∈ ℂ)
138 fveq2 6881 . . . . . . . 8 (𝑗 = 𝑥 → (𝐾𝑗) = (𝐾𝑥))
139138csbeq1d 3889 . . . . . . 7 (𝑗 = 𝑥(𝐾𝑗) / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
140 prodmolem2.4 . . . . . . 7 𝐻 = (𝑗 ∈ ℕ ↦ (𝐾𝑗) / 𝑘𝐵)
141139, 140fvmptg 6986 . . . . . 6 ((𝑥 ∈ ℕ ∧ (𝐾𝑥) / 𝑘𝐵 ∈ ℂ) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
142136, 137, 141syl2an2 683 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
143104, 135, 1423eqtr4rd 2775 . . . 4 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐹‘(𝐾𝑥)))
14469, 71, 73, 74, 4, 75, 3, 88, 99, 143seqcoll 14422 . . 3 (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾𝑁)) = (seq1( · , 𝐻)‘𝑁))
145 prodmo.3 . . . 4 𝐺 = (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵)
1468, 8jca 511 . . . 4 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
1471, 2, 145, 140, 146, 6, 27prodmolem3 15874 . . 3 (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁))
148144, 147eqtr4d 2767 . 2 (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾𝑁)) = (seq1( · , 𝐺)‘𝑁))
14967, 148breqtrd 5164 1 (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1533  wcel 2098  csb 3885  cdif 3937  wss 3940  ifcif 4520   class class class wbr 5138  cmpt 5221  ccnv 5665  wf 6529  1-1-ontowf1o 6532  cfv 6533   Isom wiso 6534  (class class class)co 7401  Fincfn 8935  cc 11104  cr 11105  1c1 11107   · cmul 11111  *cxr 11244   < clt 11245  cle 11246  cn 12209  0cn0 12469  cz 12555  cuz 12819  ...cfz 13481  seqcseq 13963  chash 14287  cli 15425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-fz 13482  df-fzo 13625  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429
This theorem is referenced by:  prodmolem2  15876  zprod  15878
  Copyright terms: Public domain W3C validator