summo - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > summo		Structured version Unicode version

Theorem summo 13186

Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

**Hypotheses**
Ref	Expression
summo.1
summo.2	$/\$
summo.3

**Assertion**
Ref	Expression
summo	$/\$ $\/$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem summo Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5686	. . . . . . . . . 10
2	1	sseq2d 3379	. . . . . . . . 9
3		seqeq1 11801	. . . . . . . . . 10
4	3	breq1d 4297	. . . . . . . . 9
5	2, 4	anbi12d 710	. . . . . . . 8 $/\$ $/\$
6	5	cbvrexv 2943	. . . . . . 7 $/\$ $/\$
7		reeanv 2883	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simprlr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		summo.1	. . . . . . . . . . . . . 14
10		simpll 753	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		summo.2	. . . . . . . . . . . . . . 15 $/\$
12	10, 11	sylan 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simplrl 759	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simplrr 760	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simprll 761	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simprrl 763	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	9, 12, 13, 14, 15, 16	sumrb 13182	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	8, 17	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simprrr 764	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		climuni 13022	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22	21	exp31 604	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
23	22	rexlimdvv 2842	. . . . . . . . 9 $/\$ $/\$ $/\$
24	7, 23	syl5bir 218	. . . . . . . 8 $/\$ $/\$ $/\$
25	24	expdimp 437	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 25	syl5bi 217	. . . . . 6 $/\$ $/\$ $/\$
27		summo.3	. . . . . . 7
28	9, 11, 27	summolem2 13185	. . . . . 6 $/\$ $/\$ $/\$
29	26, 28	jaod 380	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
30	9, 11, 27	summolem2 13185	. . . . . . . 8 $/\$ $/\$ $/\$
31		equcom 1732	. . . . . . . 8
32	30, 31	syl6ib 226	. . . . . . 7 $/\$ $/\$ $/\$
33	32	impancom 440	. . . . . 6 $/\$ $/\$ $/\$
34		oveq2 6094	. . . . . . . . . . . 12
35		f1oeq2 5628	. . . . . . . . . . . 12
36	34, 35	syl 16	. . . . . . . . . . 11
37		fveq2 5686	. . . . . . . . . . . 12
38	37	eqeq2d 2449	. . . . . . . . . . 11
39	36, 38	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
40	39	exbidv 1680	. . . . . . . . 9 $/\$ $/\$
41		f1oeq1 5627	. . . . . . . . . . 11
42		fveq1 5685	. . . . . . . . . . . . . . . . 17
43	42	csbeq1d 3290	. . . . . . . . . . . . . . . 16
44	43	mpteq2dv 4374	. . . . . . . . . . . . . . 15
45	27, 44	syl5eq 2482	. . . . . . . . . . . . . 14
46	45	seqeq3d 11806	. . . . . . . . . . . . 13
47	46	fveq1d 5688	. . . . . . . . . . . 12
48	47	eqeq2d 2449	. . . . . . . . . . 11
49	41, 48	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
50	49	cbvexv 1972	. . . . . . . . 9 $/\$ $/\$
51	40, 50	syl6bb 261	. . . . . . . 8 $/\$ $/\$
52	51	cbvrexv 2943	. . . . . . 7 $/\$ $/\$
53		reeanv 2883	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		eeanv 1932	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		an4 820	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simpll 753	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	56, 11	sylan 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
58		fveq2 5686	. . . . . . . . . . . . . . . . . . 19
59	58	csbeq1d 3290	. . . . . . . . . . . . . . . . . 18
60	59	cbvmptv 4378	. . . . . . . . . . . . . . . . 17
61	27, 60	eqtri 2458	. . . . . . . . . . . . . . . 16
62		fveq2 5686	. . . . . . . . . . . . . . . . . 18
63	62	csbeq1d 3290	. . . . . . . . . . . . . . . . 17
64	63	cbvmptv 4378	. . . . . . . . . . . . . . . 16
65		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
66		simprl 755	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
68	9, 57, 61, 64, 65, 66, 67	summolem3 13183	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
69		eqeq12 2450	. . . . . . . . . . . . . . 15 $/\$
70	68, 69	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	expimpd 603	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
72	55, 71	syl5bi 217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	exlimdvv 1691	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
74	54, 73	syl5bir 218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2843	. . . . . . . . 9 $/\$ $/\$ $/\$
76	53, 75	syl5bir 218	. . . . . . . 8 $/\$ $/\$ $/\$
77	76	expdimp 437	. . . . . . 7 $/\$ $/\$ $/\$
78	52, 77	syl5bi 217	. . . . . 6 $/\$ $/\$ $/\$
79	33, 78	jaod 380	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
80	29, 79	jaodan 783	. . . 4 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
81	80	expimpd 603	. . 3 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
82	81	alrimivv 1686	. 2 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
83		breq2 4291	. . . . . 6
84	83	anbi2d 703	. . . . 5 $/\$ $/\$
85	84	rexbidv 2731	. . . 4 $/\$ $/\$
86		eqeq1 2444	. . . . . . 7
87	86	anbi2d 703	. . . . . 6 $/\$ $/\$
88	87	exbidv 1680	. . . . 5 $/\$ $/\$
89	88	rexbidv 2731	. . . 4 $/\$ $/\$
90	85, 89	orbi12d 709	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
91	90	mo4 2315	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
92	82, 91	sylibr 212	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wal 1367

wceq 1369

wex 1586

wcel 1756

wmo 2253

wrex 2711

csb 3283

wss 3323

cif 3786 class class class wbr 4287

cmpt 4345

wf1o 5412

cfv 5413 (class class class)co 6086

cc 9272

cc0 9274

c1 9275

caddc 9277

cn 10314

cz 10638

cuz 10853

cfz 11429

cseq 11798

cli 12954

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-sup 7683 df-oi 7716 df-card 8101 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-n0 10572 df-z 10639 df-uz 10854 df-rp 10984 df-fz 11430 df-fzo 11541 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-clim 12958

This theorem is referenced by: fsum 13189

W3C validator