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

Theorem summolem2a 15605
Description: Lemma for summo 15607. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 20-Apr-2014.)
Hypotheses
Ref Expression
summo.1 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0))
summo.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
summo.3 𝐺 = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
summolem2.4 𝐻 = (𝑛 ∈ ℕ ↦ (𝐾𝑛) / 𝑘𝐵)
summolem2.5 (𝜑𝑁 ∈ ℕ)
summolem2.6 (𝜑𝑀 ∈ ℤ)
summolem2.7 (𝜑𝐴 ⊆ (ℤ𝑀))
summolem2.8 (𝜑𝑓:(1...𝑁)–1-1-onto𝐴)
summolem2.9 (𝜑𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))
Assertion
Ref Expression
summolem2a (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))
Distinct variable groups:   𝑓,𝑘,𝑛,𝐴   𝑓,𝐹,𝑘,𝑛   𝑘,𝐺,𝑛   𝑘,𝐾,𝑛   𝑘,𝑁,𝑛   𝜑,𝑘,𝑛   𝐵,𝑓,𝑛   𝑘,𝑀,𝑛
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑘)   𝐺(𝑓)   𝐻(𝑓,𝑘,𝑛)   𝐾(𝑓)   𝑀(𝑓)   𝑁(𝑓)

Proof of Theorem summolem2a
Dummy variables 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 summo.1 . . 3 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0))
2 summo.2 . . 3 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
3 summolem2.7 . . . 4 (𝜑𝐴 ⊆ (ℤ𝑀))
4 summolem2.9 . . . . . . . 8 (𝜑𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))
5 fzfid 13884 . . . . . . . . . . . 12 (𝜑 → (1...𝑁) ∈ Fin)
6 summolem2.8 . . . . . . . . . . . 12 (𝜑𝑓:(1...𝑁)–1-1-onto𝐴)
75, 6hasheqf1od 14259 . . . . . . . . . . 11 (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
8 summolem2.5 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
9 nnnn0 12425 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
10 hashfz1 14252 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
118, 9, 103syl 18 . . . . . . . . . . 11 (𝜑 → (♯‘(1...𝑁)) = 𝑁)
127, 11eqtr3d 2775 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = 𝑁)
1312oveq2d 7374 . . . . . . . . 9 (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
14 isoeq4 7266 . . . . . . . . 9 ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
1513, 14syl 17 . . . . . . . 8 (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
164, 15mpbid 231 . . . . . . 7 (𝜑𝐾 Isom < , < ((1...𝑁), 𝐴))
17 isof1o 7269 . . . . . . 7 (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto𝐴)
1816, 17syl 17 . . . . . 6 (𝜑𝐾:(1...𝑁)–1-1-onto𝐴)
19 f1of 6785 . . . . . 6 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:(1...𝑁)⟶𝐴)
2018, 19syl 17 . . . . 5 (𝜑𝐾:(1...𝑁)⟶𝐴)
21 nnuz 12811 . . . . . . 7 ℕ = (ℤ‘1)
228, 21eleqtrdi 2844 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘1))
23 eluzfz2 13455 . . . . . 6 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2422, 23syl 17 . . . . 5 (𝜑𝑁 ∈ (1...𝑁))
2520, 24ffvelcdmd 7037 . . . 4 (𝜑 → (𝐾𝑁) ∈ 𝐴)
263, 25sseldd 3946 . . 3 (𝜑 → (𝐾𝑁) ∈ (ℤ𝑀))
273sselda 3945 . . . . . 6 ((𝜑𝑛𝐴) → 𝑛 ∈ (ℤ𝑀))
28 f1ocnvfv2 7224 . . . . . . . . 9 ((𝐾:(1...𝑁)–1-1-onto𝐴𝑛𝐴) → (𝐾‘(𝐾𝑛)) = 𝑛)
2918, 28sylan 581 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝐾‘(𝐾𝑛)) = 𝑛)
30 f1ocnv 6797 . . . . . . . . . . . 12 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:𝐴1-1-onto→(1...𝑁))
31 f1of 6785 . . . . . . . . . . . 12 (𝐾:𝐴1-1-onto→(1...𝑁) → 𝐾:𝐴⟶(1...𝑁))
3218, 30, 313syl 18 . . . . . . . . . . 11 (𝜑𝐾:𝐴⟶(1...𝑁))
3332ffvelcdmda 7036 . . . . . . . . . 10 ((𝜑𝑛𝐴) → (𝐾𝑛) ∈ (1...𝑁))
34 elfzle2 13451 . . . . . . . . . 10 ((𝐾𝑛) ∈ (1...𝑁) → (𝐾𝑛) ≤ 𝑁)
3533, 34syl 17 . . . . . . . . 9 ((𝜑𝑛𝐴) → (𝐾𝑛) ≤ 𝑁)
3616adantr 482 . . . . . . . . . 10 ((𝜑𝑛𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
37 fzssuz 13488 . . . . . . . . . . . . 13 (1...𝑁) ⊆ (ℤ‘1)
38 uzssz 12789 . . . . . . . . . . . . . 14 (ℤ‘1) ⊆ ℤ
39 zssre 12511 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
4038, 39sstri 3954 . . . . . . . . . . . . 13 (ℤ‘1) ⊆ ℝ
4137, 40sstri 3954 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
42 ressxr 11204 . . . . . . . . . . . 12 ℝ ⊆ ℝ*
4341, 42sstri 3954 . . . . . . . . . . 11 (1...𝑁) ⊆ ℝ*
4443a1i 11 . . . . . . . . . 10 ((𝜑𝑛𝐴) → (1...𝑁) ⊆ ℝ*)
453adantr 482 . . . . . . . . . . . 12 ((𝜑𝑛𝐴) → 𝐴 ⊆ (ℤ𝑀))
46 uzssz 12789 . . . . . . . . . . . . 13 (ℤ𝑀) ⊆ ℤ
4746, 39sstri 3954 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℝ
4845, 47sstrdi 3957 . . . . . . . . . . 11 ((𝜑𝑛𝐴) → 𝐴 ⊆ ℝ)
4948, 42sstrdi 3957 . . . . . . . . . 10 ((𝜑𝑛𝐴) → 𝐴 ⊆ ℝ*)
5024adantr 482 . . . . . . . . . 10 ((𝜑𝑛𝐴) → 𝑁 ∈ (1...𝑁))
51 leisorel 14365 . . . . . . . . . 10 ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ ((𝐾𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((𝐾𝑛) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑛)) ≤ (𝐾𝑁)))
5236, 44, 49, 33, 50, 51syl122anc 1380 . . . . . . . . 9 ((𝜑𝑛𝐴) → ((𝐾𝑛) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑛)) ≤ (𝐾𝑁)))
5335, 52mpbid 231 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝐾‘(𝐾𝑛)) ≤ (𝐾𝑁))
5429, 53eqbrtrrd 5130 . . . . . . 7 ((𝜑𝑛𝐴) → 𝑛 ≤ (𝐾𝑁))
55 eluzelz 12778 . . . . . . . . 9 (𝑛 ∈ (ℤ𝑀) → 𝑛 ∈ ℤ)
5627, 55syl 17 . . . . . . . 8 ((𝜑𝑛𝐴) → 𝑛 ∈ ℤ)
57 eluzelz 12778 . . . . . . . . . 10 ((𝐾𝑁) ∈ (ℤ𝑀) → (𝐾𝑁) ∈ ℤ)
5826, 57syl 17 . . . . . . . . 9 (𝜑 → (𝐾𝑁) ∈ ℤ)
5958adantr 482 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝐾𝑁) ∈ ℤ)
60 eluz 12782 . . . . . . . 8 ((𝑛 ∈ ℤ ∧ (𝐾𝑁) ∈ ℤ) → ((𝐾𝑁) ∈ (ℤ𝑛) ↔ 𝑛 ≤ (𝐾𝑁)))
6156, 59, 60syl2anc 585 . . . . . . 7 ((𝜑𝑛𝐴) → ((𝐾𝑁) ∈ (ℤ𝑛) ↔ 𝑛 ≤ (𝐾𝑁)))
6254, 61mpbird 257 . . . . . 6 ((𝜑𝑛𝐴) → (𝐾𝑁) ∈ (ℤ𝑛))
63 elfzuzb 13441 . . . . . 6 (𝑛 ∈ (𝑀...(𝐾𝑁)) ↔ (𝑛 ∈ (ℤ𝑀) ∧ (𝐾𝑁) ∈ (ℤ𝑛)))
6427, 62, 63sylanbrc 584 . . . . 5 ((𝜑𝑛𝐴) → 𝑛 ∈ (𝑀...(𝐾𝑁)))
6564ex 414 . . . 4 (𝜑 → (𝑛𝐴𝑛 ∈ (𝑀...(𝐾𝑁))))
6665ssrdv 3951 . . 3 (𝜑𝐴 ⊆ (𝑀...(𝐾𝑁)))
671, 2, 26, 66fsumcvg 15602 . 2 (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾𝑁)))
68 addid2 11343 . . . . 5 (𝑚 ∈ ℂ → (0 + 𝑚) = 𝑚)
6968adantl 483 . . . 4 ((𝜑𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚)
70 addid1 11340 . . . . 5 (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚)
7170adantl 483 . . . 4 ((𝜑𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚)
72 addcl 11138 . . . . 5 ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ)
7372adantl 483 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ)
74 0cnd 11153 . . . 4 (𝜑 → 0 ∈ ℂ)
7524, 13eleqtrrd 2837 . . . 4 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
76 iftrue 4493 . . . . . . . . . . 11 (𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) = 𝐵)
7776adantl 483 . . . . . . . . . 10 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 0) = 𝐵)
7877, 2eqeltrd 2834 . . . . . . . . 9 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
7978ex 414 . . . . . . . 8 (𝜑 → (𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ))
80 iffalse 4496 . . . . . . . . 9 𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) = 0)
81 0cn 11152 . . . . . . . . 9 0 ∈ ℂ
8280, 81eqeltrdi 2842 . . . . . . . 8 𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
8379, 82pm2.61d1 180 . . . . . . 7 (𝜑 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
8483adantr 482 . . . . . 6 ((𝜑𝑘 ∈ ℤ) → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
8584, 1fmptd 7063 . . . . 5 (𝜑𝐹:ℤ⟶ℂ)
86 elfzelz 13447 . . . . 5 (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
87 ffvelcdm 7033 . . . . 5 ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹𝑚) ∈ ℂ)
8885, 86, 87syl2an 597 . . . 4 ((𝜑𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴)))) → (𝐹𝑚) ∈ ℂ)
89 fveqeq2 6852 . . . . . 6 (𝑘 = 𝑚 → ((𝐹𝑘) = 0 ↔ (𝐹𝑚) = 0))
90 eldifi 4087 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
9190elfzelzd 13448 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
92 eldifn 4088 . . . . . . . . . 10 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘𝐴)
9392, 80syl 17 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 0) = 0)
9493, 81eqeltrdi 2842 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
951fvmpt2 6960 . . . . . . . 8 ((𝑘 ∈ ℤ ∧ if(𝑘𝐴, 𝐵, 0) ∈ ℂ) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 0))
9691, 94, 95syl2anc 585 . . . . . . 7 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 0))
9796, 93eqtrd 2773 . . . . . 6 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = 0)
9889, 97vtoclga 3533 . . . . 5 (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑚) = 0)
9998adantl 483 . . . 4 ((𝜑𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑚) = 0)
100 isof1o 7269 . . . . . . . 8 (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto𝐴)
101 f1of 6785 . . . . . . . 8 (𝐾:(1...(♯‘𝐴))–1-1-onto𝐴𝐾:(1...(♯‘𝐴))⟶𝐴)
1024, 100, 1013syl 18 . . . . . . 7 (𝜑𝐾:(1...(♯‘𝐴))⟶𝐴)
103102ffvelcdmda 7036 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ 𝐴)
104103iftrued 4495 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) = (𝐾𝑥) / 𝑘𝐵)
1053adantr 482 . . . . . . . 8 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ𝑀))
106105, 103sseldd 3946 . . . . . . 7 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ (ℤ𝑀))
107 eluzelz 12778 . . . . . . 7 ((𝐾𝑥) ∈ (ℤ𝑀) → (𝐾𝑥) ∈ ℤ)
108106, 107syl 17 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ ℤ)
109 nfv 1918 . . . . . . . . 9 𝑘𝜑
110 nfv 1918 . . . . . . . . . . 11 𝑘(𝐾𝑥) ∈ 𝐴
111 nfcsb1v 3881 . . . . . . . . . . 11 𝑘(𝐾𝑥) / 𝑘𝐵
112 nfcv 2904 . . . . . . . . . . 11 𝑘0
113110, 111, 112nfif 4517 . . . . . . . . . 10 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0)
114113nfel1 2920 . . . . . . . . 9 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ
115109, 114nfim 1900 . . . . . . . 8 𝑘(𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)
116 fvex 6856 . . . . . . . 8 (𝐾𝑥) ∈ V
117 eleq1 2822 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → (𝑘𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
118 csbeq1a 3870 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → 𝐵 = (𝐾𝑥) / 𝑘𝐵)
119117, 118ifbieq1d 4511 . . . . . . . . . 10 (𝑘 = (𝐾𝑥) → if(𝑘𝐴, 𝐵, 0) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
120119eleq1d 2819 . . . . . . . . 9 (𝑘 = (𝐾𝑥) → (if(𝑘𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ))
121120imbi2d 341 . . . . . . . 8 (𝑘 = (𝐾𝑥) → ((𝜑 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ) ↔ (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)))
122115, 116, 121, 83vtoclf 3515 . . . . . . 7 (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)
123122adantr 482 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)
124 eleq1 2822 . . . . . . . 8 (𝑛 = (𝐾𝑥) → (𝑛𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
125 csbeq1 3859 . . . . . . . 8 (𝑛 = (𝐾𝑥) → 𝑛 / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
126124, 125ifbieq1d 4511 . . . . . . 7 (𝑛 = (𝐾𝑥) → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
127 nfcv 2904 . . . . . . . . 9 𝑛if(𝑘𝐴, 𝐵, 0)
128 nfv 1918 . . . . . . . . . 10 𝑘 𝑛𝐴
129 nfcsb1v 3881 . . . . . . . . . 10 𝑘𝑛 / 𝑘𝐵
130128, 129, 112nfif 4517 . . . . . . . . 9 𝑘if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
131 eleq1 2822 . . . . . . . . . 10 (𝑘 = 𝑛 → (𝑘𝐴𝑛𝐴))
132 csbeq1a 3870 . . . . . . . . . 10 (𝑘 = 𝑛𝐵 = 𝑛 / 𝑘𝐵)
133131, 132ifbieq1d 4511 . . . . . . . . 9 (𝑘 = 𝑛 → if(𝑘𝐴, 𝐵, 0) = if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
134127, 130, 133cbvmpt 5217 . . . . . . . 8 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
1351, 134eqtri 2761 . . . . . . 7 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
136126, 135fvmptg 6947 . . . . . 6 (((𝐾𝑥) ∈ ℤ ∧ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
137108, 123, 136syl2anc 585 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
138 elfznn 13476 . . . . . 6 (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
139104, 123eqeltrrd 2835 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) / 𝑘𝐵 ∈ ℂ)
140 fveq2 6843 . . . . . . . 8 (𝑛 = 𝑥 → (𝐾𝑛) = (𝐾𝑥))
141140csbeq1d 3860 . . . . . . 7 (𝑛 = 𝑥(𝐾𝑛) / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
142 summolem2.4 . . . . . . 7 𝐻 = (𝑛 ∈ ℕ ↦ (𝐾𝑛) / 𝑘𝐵)
143141, 142fvmptg 6947 . . . . . 6 ((𝑥 ∈ ℕ ∧ (𝐾𝑥) / 𝑘𝐵 ∈ ℂ) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
144138, 139, 143syl2an2 685 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
145104, 137, 1443eqtr4rd 2784 . . . 4 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐹‘(𝐾𝑥)))
14669, 71, 73, 74, 4, 75, 3, 88, 99, 145seqcoll 14369 . . 3 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾𝑁)) = (seq1( + , 𝐻)‘𝑁))
147 summo.3 . . . 4 𝐺 = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
1488, 8jca 513 . . . 4 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
1491, 2, 147, 142, 148, 6, 18summolem3 15604 . . 3 (𝜑 → (seq1( + , 𝐺)‘𝑁) = (seq1( + , 𝐻)‘𝑁))
150146, 149eqtr4d 2776 . 2 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾𝑁)) = (seq1( + , 𝐺)‘𝑁))
15167, 150breqtrd 5132 1 (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  csb 3856  cdif 3908  wss 3911  ifcif 4487   class class class wbr 5106  cmpt 5189  ccnv 5633  wf 6493  1-1-ontowf1o 6496  cfv 6497   Isom wiso 6498  (class class class)co 7358  Fincfn 8886  cc 11054  cr 11055  0cc0 11056  1c1 11057   + caddc 11059  *cxr 11193   < clt 11194  cle 11195  cn 12158  0cn0 12418  cz 12504  cuz 12768  ...cfz 13430  seqcseq 13912  chash 14236  cli 15372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-n0 12419  df-z 12505  df-uz 12769  df-rp 12921  df-fz 13431  df-fzo 13574  df-seq 13913  df-exp 13974  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-clim 15376
This theorem is referenced by:  summolem2  15606  zsum  15608
  Copyright terms: Public domain W3C validator