fsumm1 - Metamath Proof Explorer

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

Theorem fsumm1 15926

Description: Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.)

**Hypotheses**
Ref	Expression
fsumm1.1	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
fsumm1.2	⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)
fsumm1.3	⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)

**Assertion**
Ref	Expression
fsumm1	⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + 𝐵))

Distinct variable groups: 𝐵,𝑘 𝑘,𝑀 𝑘,𝑁 𝜑,𝑘 Allowed substitution hint: 𝐴(𝑘)

**Proof of Theorem fsumm1**
Step	Hyp	Ref	Expression
1		fsumm1.1	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
2		eluzelz 12982	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
3	1, 2	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℤ)
4		fzsn 13707	. . . . . 6 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
5	3, 4	syl 18	. . . . 5 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
6	5	ineq2d 4116	. . . 4 ⊢ (𝜑 → ((𝑀...(𝑁 − 1)) ∩ (𝑁...𝑁)) = ((𝑀...(𝑁 − 1)) ∩ {𝑁}))
7	3	zred 12810	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
8	7	ltm1d 12256	. . . . 5 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
9		fzdisj 13692	. . . . 5 ⊢ ((𝑁 − 1) < 𝑁 → ((𝑀...(𝑁 − 1)) ∩ (𝑁...𝑁)) = ∅)
10	8, 9	syl 18	. . . 4 ⊢ (𝜑 → ((𝑀...(𝑁 − 1)) ∩ (𝑁...𝑁)) = ∅)
11	6, 10	eqtr3d 2797	. . 3 ⊢ (𝜑 → ((𝑀...(𝑁 − 1)) ∩ {𝑁}) = ∅)
12		eluzel2 12977	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
13	1, 12	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
14		peano2zm 12746	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
15	13, 14	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
16	13	zcnd 12811	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℂ)
17		ax-1cn 11265	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
18		npcan 11573	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 − 1) + 1) = 𝑀)
19	16, 17, 18	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
20	19	fveq2d 6894	. . . . . . . 8 ⊢ (𝜑 → (ℤ_≥‘((𝑀 − 1) + 1)) = (ℤ_≥‘𝑀))
21	1, 20	eleqtrrd 2863	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘((𝑀 − 1) + 1)))
22		eluzp1m1 12998	. . . . . . 7 ⊢ (((𝑀 − 1) ∈ ℤ ∧ 𝑁 ∈ (ℤ_≥‘((𝑀 − 1) + 1))) → (𝑁 − 1) ∈ (ℤ_≥‘(𝑀 − 1)))
23	15, 21, 22	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘(𝑀 − 1)))
24		fzsuc2 13723	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ (ℤ_≥‘(𝑀 − 1))) → (𝑀...((𝑁 − 1) + 1)) = ((𝑀...(𝑁 − 1)) ∪ {((𝑁 − 1) + 1)}))
25	13, 23, 24	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝑀...((𝑁 − 1) + 1)) = ((𝑀...(𝑁 − 1)) ∪ {((𝑁 − 1) + 1)}))
26	3	zcnd 12811	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
27		npcan 11573	. . . . . . 7 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
28	26, 17, 27	sylancl 598	. . . . . 6 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
29	28	oveq2d 7440	. . . . 5 ⊢ (𝜑 → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁))
30	25, 29	eqtr3d 2797	. . . 4 ⊢ (𝜑 → ((𝑀...(𝑁 − 1)) ∪ {((𝑁 − 1) + 1)}) = (𝑀...𝑁))
31	28	sneqd 4592	. . . . 5 ⊢ (𝜑 → {((𝑁 − 1) + 1)} = {𝑁})
32	31	uneq2d 4166	. . . 4 ⊢ (𝜑 → ((𝑀...(𝑁 − 1)) ∪ {((𝑁 − 1) + 1)}) = ((𝑀...(𝑁 − 1)) ∪ {𝑁}))
33	30, 32	eqtr3d 2797	. . 3 ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀...(𝑁 − 1)) ∪ {𝑁}))
34		fzfid 14123	. . 3 ⊢ (𝜑 → (𝑀...𝑁) ∈ Fin)
35		fsumm1.2	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)
36	11, 33, 34, 35	fsumsplit 15916	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ {𝑁}𝐴))
37		fsumm1.3	. . . . . 6 ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)
38	37	eleq1d 2845	. . . . 5 ⊢ (𝑘 = 𝑁 → (𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ))
39	35	ralrimiva 3154	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ)
40		eluzfz2 13672	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
41	1, 40	syl 18	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
42	38, 39, 41	rspcdva 3577	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
43	37	sumsn 15921	. . . 4 ⊢ ((𝑁 ∈ (ℤ_≥‘𝑀) ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑁}𝐴 = 𝐵)
44	1, 42, 43	syl2anc 596	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑁}𝐴 = 𝐵)
45	44	oveq2d 7440	. 2 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ {𝑁}𝐴) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + 𝐵))
46	36, 45	eqtrd 2795	1 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∩ cin 4088 ∪ cun 4148 ∅c0 4277 {csn 4584 class class class wbr 5102 ‘cfv 6543 (class class class)co 7424 ℂcc 11205 1c1 11208 + caddc 11210 < clt 11350 − cmin 11548 ℤcz 12700 ℤ_≥cuz 12972 ...cfz 13646 Σcsu 15862

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-inf2 9649 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-pre-sup 11285

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7882 df-1st 8005 df-2nd 8006 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-er 8725 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-sup 9441 df-oi 9511 df-card 10027 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-div 11981 df-nn 12343 df-2 12412 df-3 12413 df-n0 12614 df-z 12701 df-uz 12973 df-rp 13128 df-fz 13647 df-fzo 13796 df-seq 14152 df-exp 14212 df-hash 14482 df-cj 15275 df-re 15276 df-im 15277 df-sqrt 15411 df-abs 15412 df-clim 15664 df-sum 15863

This theorem is used by: fzosump1 15927 fsump1 15931 telfsumo 15978 fsumparts 15982 binom1dif 16011 pwdif 16046 bpolysum 16228 bpolydiflem 16229 pwp1fsum 16570 prmreclem4 17106 ovolicc2lem4 25850 dvfsumlem1 26355 abelthlem6 26772 log2ublem2 27284 harmonicbnd4 27347 ftalem1 27409 ftalem5 27413 chpp1 27491 1sgmprm 27535 chtublem 27547 logdivbnd 27892 pntrlog2bndlem1 27913 knoppndvlem15 37516 mettrifi 38828 sticksstones12a 43344 sticksstones12 43345 fzosumm1 43438 fz1sump1 43504 stoweidlem17 47163 nnsum4primeseven 49034 nnsum4primesevenALTV 49035

W3C validator