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

Theorem summolem2a 15064
 Description: Lemma for summo 15066. (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 13336 . . . . . . . . . . . 12 (𝜑 → (1...𝑁) ∈ Fin)
6 summolem2.8 . . . . . . . . . . . 12 (𝜑𝑓:(1...𝑁)–1-1-onto𝐴)
75, 6hasheqf1od 13710 . . . . . . . . . . 11 (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
8 summolem2.5 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
9 nnnn0 11892 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
10 hashfz1 13702 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
118, 9, 103syl 18 . . . . . . . . . . 11 (𝜑 → (♯‘(1...𝑁)) = 𝑁)
127, 11eqtr3d 2835 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = 𝑁)
1312oveq2d 7151 . . . . . . . . 9 (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
14 isoeq4 7052 . . . . . . . . 9 ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
1513, 14syl 17 . . . . . . . 8 (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
164, 15mpbid 235 . . . . . . 7 (𝜑𝐾 Isom < , < ((1...𝑁), 𝐴))
17 isof1o 7055 . . . . . . 7 (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto𝐴)
1816, 17syl 17 . . . . . 6 (𝜑𝐾:(1...𝑁)–1-1-onto𝐴)
19 f1of 6590 . . . . . 6 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:(1...𝑁)⟶𝐴)
2018, 19syl 17 . . . . 5 (𝜑𝐾:(1...𝑁)⟶𝐴)
21 nnuz 12269 . . . . . . 7 ℕ = (ℤ‘1)
228, 21eleqtrdi 2900 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘1))
23 eluzfz2 12910 . . . . . 6 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2422, 23syl 17 . . . . 5 (𝜑𝑁 ∈ (1...𝑁))
2520, 24ffvelrnd 6829 . . . 4 (𝜑 → (𝐾𝑁) ∈ 𝐴)
263, 25sseldd 3916 . . 3 (𝜑 → (𝐾𝑁) ∈ (ℤ𝑀))
273sselda 3915 . . . . . 6 ((𝜑𝑛𝐴) → 𝑛 ∈ (ℤ𝑀))
28 f1ocnvfv2 7012 . . . . . . . . 9 ((𝐾:(1...𝑁)–1-1-onto𝐴𝑛𝐴) → (𝐾‘(𝐾𝑛)) = 𝑛)
2918, 28sylan 583 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝐾‘(𝐾𝑛)) = 𝑛)
30 f1ocnv 6602 . . . . . . . . . . . 12 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:𝐴1-1-onto→(1...𝑁))
31 f1of 6590 . . . . . . . . . . . 12 (𝐾:𝐴1-1-onto→(1...𝑁) → 𝐾:𝐴⟶(1...𝑁))
3218, 30, 313syl 18 . . . . . . . . . . 11 (𝜑𝐾:𝐴⟶(1...𝑁))
3332ffvelrnda 6828 . . . . . . . . . 10 ((𝜑𝑛𝐴) → (𝐾𝑛) ∈ (1...𝑁))
34 elfzle2 12906 . . . . . . . . . 10 ((𝐾𝑛) ∈ (1...𝑁) → (𝐾𝑛) ≤ 𝑁)
3533, 34syl 17 . . . . . . . . 9 ((𝜑𝑛𝐴) → (𝐾𝑛) ≤ 𝑁)
3616adantr 484 . . . . . . . . . 10 ((𝜑𝑛𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
37 fzssuz 12943 . . . . . . . . . . . . 13 (1...𝑁) ⊆ (ℤ‘1)
38 uzssz 12252 . . . . . . . . . . . . . 14 (ℤ‘1) ⊆ ℤ
39 zssre 11976 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
4038, 39sstri 3924 . . . . . . . . . . . . 13 (ℤ‘1) ⊆ ℝ
4137, 40sstri 3924 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
42 ressxr 10674 . . . . . . . . . . . 12 ℝ ⊆ ℝ*
4341, 42sstri 3924 . . . . . . . . . . 11 (1...𝑁) ⊆ ℝ*
4443a1i 11 . . . . . . . . . 10 ((𝜑𝑛𝐴) → (1...𝑁) ⊆ ℝ*)
453adantr 484 . . . . . . . . . . . 12 ((𝜑𝑛𝐴) → 𝐴 ⊆ (ℤ𝑀))
46 uzssz 12252 . . . . . . . . . . . . 13 (ℤ𝑀) ⊆ ℤ
4746, 39sstri 3924 . . . . . . . . . . . 12 (ℤ𝑀) ⊆ ℝ
4845, 47sstrdi 3927 . . . . . . . . . . 11 ((𝜑𝑛𝐴) → 𝐴 ⊆ ℝ)
4948, 42sstrdi 3927 . . . . . . . . . 10 ((𝜑𝑛𝐴) → 𝐴 ⊆ ℝ*)
5024adantr 484 . . . . . . . . . 10 ((𝜑𝑛𝐴) → 𝑁 ∈ (1...𝑁))
51 leisorel 13814 . . . . . . . . . 10 ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ ((𝐾𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((𝐾𝑛) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑛)) ≤ (𝐾𝑁)))
5236, 44, 49, 33, 50, 51syl122anc 1376 . . . . . . . . 9 ((𝜑𝑛𝐴) → ((𝐾𝑛) ≤ 𝑁 ↔ (𝐾‘(𝐾𝑛)) ≤ (𝐾𝑁)))
5335, 52mpbid 235 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝐾‘(𝐾𝑛)) ≤ (𝐾𝑁))
5429, 53eqbrtrrd 5054 . . . . . . 7 ((𝜑𝑛𝐴) → 𝑛 ≤ (𝐾𝑁))
55 eluzelz 12241 . . . . . . . . 9 (𝑛 ∈ (ℤ𝑀) → 𝑛 ∈ ℤ)
5627, 55syl 17 . . . . . . . 8 ((𝜑𝑛𝐴) → 𝑛 ∈ ℤ)
57 eluzelz 12241 . . . . . . . . . 10 ((𝐾𝑁) ∈ (ℤ𝑀) → (𝐾𝑁) ∈ ℤ)
5826, 57syl 17 . . . . . . . . 9 (𝜑 → (𝐾𝑁) ∈ ℤ)
5958adantr 484 . . . . . . . 8 ((𝜑𝑛𝐴) → (𝐾𝑁) ∈ ℤ)
60 eluz 12245 . . . . . . . 8 ((𝑛 ∈ ℤ ∧ (𝐾𝑁) ∈ ℤ) → ((𝐾𝑁) ∈ (ℤ𝑛) ↔ 𝑛 ≤ (𝐾𝑁)))
6156, 59, 60syl2anc 587 . . . . . . 7 ((𝜑𝑛𝐴) → ((𝐾𝑁) ∈ (ℤ𝑛) ↔ 𝑛 ≤ (𝐾𝑁)))
6254, 61mpbird 260 . . . . . 6 ((𝜑𝑛𝐴) → (𝐾𝑁) ∈ (ℤ𝑛))
63 elfzuzb 12896 . . . . . 6 (𝑛 ∈ (𝑀...(𝐾𝑁)) ↔ (𝑛 ∈ (ℤ𝑀) ∧ (𝐾𝑁) ∈ (ℤ𝑛)))
6427, 62, 63sylanbrc 586 . . . . 5 ((𝜑𝑛𝐴) → 𝑛 ∈ (𝑀...(𝐾𝑁)))
6564ex 416 . . . 4 (𝜑 → (𝑛𝐴𝑛 ∈ (𝑀...(𝐾𝑁))))
6665ssrdv 3921 . . 3 (𝜑𝐴 ⊆ (𝑀...(𝐾𝑁)))
671, 2, 26, 66fsumcvg 15061 . 2 (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾𝑁)))
68 addid2 10812 . . . . 5 (𝑚 ∈ ℂ → (0 + 𝑚) = 𝑚)
6968adantl 485 . . . 4 ((𝜑𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚)
70 addid1 10809 . . . . 5 (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚)
7170adantl 485 . . . 4 ((𝜑𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚)
72 addcl 10608 . . . . 5 ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ)
7372adantl 485 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ)
74 0cnd 10623 . . . 4 (𝜑 → 0 ∈ ℂ)
7524, 13eleqtrrd 2893 . . . 4 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
76 iftrue 4431 . . . . . . . . . . 11 (𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) = 𝐵)
7776adantl 485 . . . . . . . . . 10 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 0) = 𝐵)
7877, 2eqeltrd 2890 . . . . . . . . 9 ((𝜑𝑘𝐴) → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
7978ex 416 . . . . . . . 8 (𝜑 → (𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ))
80 iffalse 4434 . . . . . . . . 9 𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) = 0)
81 0cn 10622 . . . . . . . . 9 0 ∈ ℂ
8280, 81eqeltrdi 2898 . . . . . . . 8 𝑘𝐴 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
8379, 82pm2.61d1 183 . . . . . . 7 (𝜑 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
8483adantr 484 . . . . . 6 ((𝜑𝑘 ∈ ℤ) → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
8584, 1fmptd 6855 . . . . 5 (𝜑𝐹:ℤ⟶ℂ)
86 elfzelz 12902 . . . . 5 (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
87 ffvelrn 6826 . . . . 5 ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹𝑚) ∈ ℂ)
8885, 86, 87syl2an 598 . . . 4 ((𝜑𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴)))) → (𝐹𝑚) ∈ ℂ)
89 fveqeq2 6654 . . . . . 6 (𝑘 = 𝑚 → ((𝐹𝑘) = 0 ↔ (𝐹𝑚) = 0))
90 eldifi 4054 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
91 elfzelz 12902 . . . . . . . . 9 (𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑘 ∈ ℤ)
9290, 91syl 17 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
93 eldifn 4055 . . . . . . . . . 10 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘𝐴)
9493, 80syl 17 . . . . . . . . 9 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 0) = 0)
9594, 81eqeltrdi 2898 . . . . . . . 8 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘𝐴, 𝐵, 0) ∈ ℂ)
961fvmpt2 6756 . . . . . . . 8 ((𝑘 ∈ ℤ ∧ if(𝑘𝐴, 𝐵, 0) ∈ ℂ) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 0))
9792, 95, 96syl2anc 587 . . . . . . 7 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = if(𝑘𝐴, 𝐵, 0))
9897, 94eqtrd 2833 . . . . . 6 (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑘) = 0)
9989, 98vtoclga 3522 . . . . 5 (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹𝑚) = 0)
10099adantl 485 . . . 4 ((𝜑𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑚) = 0)
101 isof1o 7055 . . . . . . . 8 (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto𝐴)
102 f1of 6590 . . . . . . . 8 (𝐾:(1...(♯‘𝐴))–1-1-onto𝐴𝐾:(1...(♯‘𝐴))⟶𝐴)
1034, 101, 1023syl 18 . . . . . . 7 (𝜑𝐾:(1...(♯‘𝐴))⟶𝐴)
104103ffvelrnda 6828 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ 𝐴)
105104iftrued 4433 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) = (𝐾𝑥) / 𝑘𝐵)
1063adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ𝑀))
107106, 104sseldd 3916 . . . . . . 7 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ (ℤ𝑀))
108 eluzelz 12241 . . . . . . 7 ((𝐾𝑥) ∈ (ℤ𝑀) → (𝐾𝑥) ∈ ℤ)
109107, 108syl 17 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) ∈ ℤ)
110 nfv 1915 . . . . . . . . 9 𝑘𝜑
111 nfv 1915 . . . . . . . . . . 11 𝑘(𝐾𝑥) ∈ 𝐴
112 nfcsb1v 3852 . . . . . . . . . . 11 𝑘(𝐾𝑥) / 𝑘𝐵
113 nfcv 2955 . . . . . . . . . . 11 𝑘0
114111, 112, 113nfif 4454 . . . . . . . . . 10 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0)
115114nfel1 2971 . . . . . . . . 9 𝑘if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ
116110, 115nfim 1897 . . . . . . . 8 𝑘(𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)
117 fvex 6658 . . . . . . . 8 (𝐾𝑥) ∈ V
118 eleq1 2877 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → (𝑘𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
119 csbeq1a 3842 . . . . . . . . . . 11 (𝑘 = (𝐾𝑥) → 𝐵 = (𝐾𝑥) / 𝑘𝐵)
120118, 119ifbieq1d 4448 . . . . . . . . . 10 (𝑘 = (𝐾𝑥) → if(𝑘𝐴, 𝐵, 0) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
121120eleq1d 2874 . . . . . . . . 9 (𝑘 = (𝐾𝑥) → (if(𝑘𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ))
122121imbi2d 344 . . . . . . . 8 (𝑘 = (𝐾𝑥) → ((𝜑 → if(𝑘𝐴, 𝐵, 0) ∈ ℂ) ↔ (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)))
123116, 117, 122, 83vtoclf 3506 . . . . . . 7 (𝜑 → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)
124123adantr 484 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ)
125 eleq1 2877 . . . . . . . 8 (𝑛 = (𝐾𝑥) → (𝑛𝐴 ↔ (𝐾𝑥) ∈ 𝐴))
126 csbeq1 3831 . . . . . . . 8 (𝑛 = (𝐾𝑥) → 𝑛 / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
127125, 126ifbieq1d 4448 . . . . . . 7 (𝑛 = (𝐾𝑥) → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
128 nfcv 2955 . . . . . . . . 9 𝑛if(𝑘𝐴, 𝐵, 0)
129 nfv 1915 . . . . . . . . . 10 𝑘 𝑛𝐴
130 nfcsb1v 3852 . . . . . . . . . 10 𝑘𝑛 / 𝑘𝐵
131129, 130, 113nfif 4454 . . . . . . . . 9 𝑘if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)
132 eleq1 2877 . . . . . . . . . 10 (𝑘 = 𝑛 → (𝑘𝐴𝑛𝐴))
133 csbeq1a 3842 . . . . . . . . . 10 (𝑘 = 𝑛𝐵 = 𝑛 / 𝑘𝐵)
134132, 133ifbieq1d 4448 . . . . . . . . 9 (𝑘 = 𝑛 → if(𝑘𝐴, 𝐵, 0) = if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
135128, 131, 134cbvmpt 5131 . . . . . . . 8 (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
1361, 135eqtri 2821 . . . . . . 7 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))
137127, 136fvmptg 6743 . . . . . 6 (((𝐾𝑥) ∈ ℤ ∧ if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
138109, 124, 137syl2anc 587 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾𝑥)) = if((𝐾𝑥) ∈ 𝐴, (𝐾𝑥) / 𝑘𝐵, 0))
139 elfznn 12931 . . . . . 6 (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
140105, 124eqeltrrd 2891 . . . . . 6 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐾𝑥) / 𝑘𝐵 ∈ ℂ)
141 fveq2 6645 . . . . . . . 8 (𝑛 = 𝑥 → (𝐾𝑛) = (𝐾𝑥))
142141csbeq1d 3832 . . . . . . 7 (𝑛 = 𝑥(𝐾𝑛) / 𝑘𝐵 = (𝐾𝑥) / 𝑘𝐵)
143 summolem2.4 . . . . . . 7 𝐻 = (𝑛 ∈ ℕ ↦ (𝐾𝑛) / 𝑘𝐵)
144142, 143fvmptg 6743 . . . . . 6 ((𝑥 ∈ ℕ ∧ (𝐾𝑥) / 𝑘𝐵 ∈ ℂ) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
145139, 140, 144syl2an2 685 . . . . 5 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐾𝑥) / 𝑘𝐵)
146105, 138, 1453eqtr4rd 2844 . . . 4 ((𝜑𝑥 ∈ (1...(♯‘𝐴))) → (𝐻𝑥) = (𝐹‘(𝐾𝑥)))
14769, 71, 73, 74, 4, 75, 3, 88, 100, 146seqcoll 13818 . . 3 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾𝑁)) = (seq1( + , 𝐻)‘𝑁))
148 summo.3 . . . 4 𝐺 = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
1498, 8jca 515 . . . 4 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
1501, 2, 148, 143, 149, 6, 18summolem3 15063 . . 3 (𝜑 → (seq1( + , 𝐺)‘𝑁) = (seq1( + , 𝐻)‘𝑁))
151147, 150eqtr4d 2836 . 2 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾𝑁)) = (seq1( + , 𝐺)‘𝑁))
15267, 151breqtrd 5056 1 (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ⦋csb 3828   ∖ cdif 3878   ⊆ wss 3881  ifcif 4425   class class class wbr 5030   ↦ cmpt 5110  ◡ccnv 5518  ⟶wf 6320  –1-1-onto→wf1o 6323  ‘cfv 6324   Isom wiso 6325  (class class class)co 7135  Fincfn 8492  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529  ℝ*cxr 10663   < clt 10664   ≤ cle 10665  ℕcn 11625  ℕ0cn0 11885  ℤcz 11969  ℤ≥cuz 12231  ...cfz 12885  seqcseq 13364  ♯chash 13686   ⇝ cli 14833 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12886  df-fzo 13029  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837 This theorem is referenced by:  summolem2  15065  zsum  15067
 Copyright terms: Public domain W3C validator