fsumconst - Metamath Proof Explorer

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

Theorem fsumconst 15715

Description: The sum of constant terms (𝑘 is not free in 𝐵). (Contributed by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)

**Assertion**
Ref	Expression
fsumconst	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘

Proof of Theorem fsumconst Dummy variables 𝑓 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mul02 11312	. . . . 5 ⊢ (𝐵 ∈ ℂ → (0 · 𝐵) = 0)
2	1	adantl 481	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → (0 · 𝐵) = 0)
3	2	eqcomd 2735	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → 0 = (0 · 𝐵))
4		sumeq1 15614	. . . . 5 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
5		sum0 15646	. . . . 5 ⊢ Σ𝑘 ∈ ∅ 𝐵 = 0
6	4, 5	eqtrdi 2780	. . . 4 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = 0)
7		fveq2 6826	. . . . . 6 ⊢ (𝐴 = ∅ → (♯‘𝐴) = (♯‘∅))
8		hash0 14292	. . . . . 6 ⊢ (♯‘∅) = 0
9	7, 8	eqtrdi 2780	. . . . 5 ⊢ (𝐴 = ∅ → (♯‘𝐴) = 0)
10	9	oveq1d 7368	. . . 4 ⊢ (𝐴 = ∅ → ((♯‘𝐴) · 𝐵) = (0 · 𝐵))
11	6, 10	eqeq12d 2745	. . 3 ⊢ (𝐴 = ∅ → (Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵) ↔ 0 = (0 · 𝐵)))
12	3, 11	syl5ibrcom 247	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵)))
13		eqidd 2730	. . . . . . 7 ⊢ (𝑘 = (𝑓‘𝑛) → 𝐵 = 𝐵)
14		simprl 770	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈ ℕ)
15		simprr 772	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
16		simpllr 775	. . . . . . 7 ⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
17		simplr 768	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝐵 ∈ ℂ)
18		elfznn 13474	. . . . . . . 8 ⊢ (𝑛 ∈ (1...(♯‘𝐴)) → 𝑛 ∈ ℕ)
19		fvconst2g 7142	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 𝑛 ∈ ℕ) → ((ℕ × {𝐵})‘𝑛) = 𝐵)
20	17, 18, 19	syl2an 596	. . . . . . 7 ⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((ℕ × {𝐵})‘𝑛) = 𝐵)
21	13, 14, 15, 16, 20	fsum 15645	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (ℕ × {𝐵}))‘(♯‘𝐴)))
22		ser1const 13983	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ (♯‘𝐴) ∈ ℕ) → (seq1( + , (ℕ × {𝐵}))‘(♯‘𝐴)) = ((♯‘𝐴) · 𝐵))
23	22	ad2ant2lr 748	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (seq1( + , (ℕ × {𝐵}))‘(♯‘𝐴)) = ((♯‘𝐴) · 𝐵))
24	21, 23	eqtrd 2764	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵))
25	24	expr 456	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵)))
26	25	exlimdv 1933	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) ∧ (♯‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵)))
27	26	expimpd 453	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → (((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵)))
28		fz1f1o 15635	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
29	28	adantr 480	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
30	12, 27, 29	mpjaod 860	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∅c0 4286 {csn 4579 × cxp 5621 –1-1-onto→wf1o 6485 ‘cfv 6486 (class class class)co 7353 Fincfn 8879 ℂcc 11026 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 ℕcn 12146 ...cfz 13428 seqcseq 13926 ♯chash 14255 Σcsu 15611

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9351 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-n0 12403 df-z 12490 df-uz 12754 df-rp 12912 df-fz 13429 df-fzo 13576 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-clim 15413 df-sum 15612

This theorem is referenced by: fsumdifsnconst 15716 o1fsum 15738 hashiun 15747 hash2iun1dif1 15749 climcndslem1 15774 climcndslem2 15775 harmonic 15784 mertenslem1 15809 sumhash 16826 cshwshashnsame 17033 lagsubg2 19091 sylow2a 19516 lebnumlem3 24878 uniioombllem4 25503 birthdaylem2 26878 basellem8 27014 0sgm 27070 musum 27117 chtleppi 27137 vmasum 27143 logfac2 27144 chpval2 27145 chpchtsum 27146 chpub 27147 logfaclbnd 27149 dchrsum2 27195 sumdchr2 27197 lgsquadlem1 27307 chebbnd1lem1 27396 chtppilimlem1 27400 dchrmusum2 27421 dchrisum0flblem1 27435 rpvmasum2 27439 dchrisum0lem2a 27444 mudivsum 27457 mulogsumlem 27458 selberglem2 27473 pntlemj 27530 rusgrnumwwlks 29937 fusgrhashclwwlkn 30041 fusgreghash2wsp 30300 numclwwlk6 30352 reprlt 34586 hashreprin 34587 reprgt 34588 hgt750lema 34624 rrndstprj2 37810 lcmineqlem17 42018 sticksstones10 42128 sticksstones12a 42130 fz1sumconst 42282 fltnltalem 42635 stoweidlem11 45993 stoweidlem26 46008 stoweidlem38 46020 dirkertrigeq 46083 fourierdlem73 46161 etransclem32 46248 rrndistlt 46272 sge0rpcpnf 46403 hoiqssbllem2 46605 nn0mulfsum 48597 amgmlemALT 49776

W3C validator