summo - Metamath Proof Explorer

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

Theorem summo 13771

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 5878	. . . . . . . . . 10
2	1	sseq2d 3492	. . . . . . . . 9
3		seqeq1 12216	. . . . . . . . . 10
4	3	breq1d 4430	. . . . . . . . 9
5	2, 4	anbi12d 715	. . . . . . . 8 $/\$ $/\$
6	5	cbvrexv 3056	. . . . . . 7 $/\$ $/\$
7		reeanv 2996	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simprlr 771	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		summo.1	. . . . . . . . . . . . . 14
10		simpll 758	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		summo.2	. . . . . . . . . . . . . . 15 $/\$
12	10, 11	sylan 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simplrl 768	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simplrr 769	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simprll 770	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simprrl 772	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	9, 12, 13, 14, 15, 16	sumrb 13767	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	8, 17	mpbid 213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simprrr 773	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		climuni 13604	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22	21	exp31 607	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
23	22	rexlimdvv 2923	. . . . . . . . 9 $/\$ $/\$ $/\$
24	7, 23	syl5bir 221	. . . . . . . 8 $/\$ $/\$ $/\$
25	24	expdimp 438	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 25	syl5bi 220	. . . . . 6 $/\$ $/\$ $/\$
27		summo.3	. . . . . . 7
28	9, 11, 27	summolem2 13770	. . . . . 6 $/\$ $/\$ $/\$
29	26, 28	jaod 381	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
30	9, 11, 27	summolem2 13770	. . . . . . . 8 $/\$ $/\$ $/\$
31		equcom 1844	. . . . . . . 8
32	30, 31	syl6ib 229	. . . . . . 7 $/\$ $/\$ $/\$
33	32	impancom 441	. . . . . 6 $/\$ $/\$ $/\$
34		oveq2 6310	. . . . . . . . . . . 12
35		f1oeq2 5820	. . . . . . . . . . . 12
36	34, 35	syl 17	. . . . . . . . . . 11
37		fveq2 5878	. . . . . . . . . . . 12
38	37	eqeq2d 2436	. . . . . . . . . . 11
39	36, 38	anbi12d 715	. . . . . . . . . 10 $/\$ $/\$
40	39	exbidv 1758	. . . . . . . . 9 $/\$ $/\$
41		f1oeq1 5819	. . . . . . . . . . 11
42		fveq1 5877	. . . . . . . . . . . . . . . . 17
43	42	csbeq1d 3402	. . . . . . . . . . . . . . . 16
44	43	mpteq2dv 4508	. . . . . . . . . . . . . . 15
45	27, 44	syl5eq 2475	. . . . . . . . . . . . . 14
46	45	seqeq3d 12221	. . . . . . . . . . . . 13
47	46	fveq1d 5880	. . . . . . . . . . . 12
48	47	eqeq2d 2436	. . . . . . . . . . 11
49	41, 48	anbi12d 715	. . . . . . . . . 10 $/\$ $/\$
50	49	cbvexv 2078	. . . . . . . . 9 $/\$ $/\$
51	40, 50	syl6bb 264	. . . . . . . 8 $/\$ $/\$
52	51	cbvrexv 3056	. . . . . . 7 $/\$ $/\$
53		reeanv 2996	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		eeanv 2043	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		an4 831	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simpll 758	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	56, 11	sylan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
58		fveq2 5878	. . . . . . . . . . . . . . . . . . 19
59	58	csbeq1d 3402	. . . . . . . . . . . . . . . . . 18
60	59	cbvmptv 4513	. . . . . . . . . . . . . . . . 17
61	27, 60	eqtri 2451	. . . . . . . . . . . . . . . 16
62		fveq2 5878	. . . . . . . . . . . . . . . . . 18
63	62	csbeq1d 3402	. . . . . . . . . . . . . . . . 17
64	63	cbvmptv 4513	. . . . . . . . . . . . . . . 16
65		simplr 760	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
66		simprl 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67		simprr 764	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
68	9, 57, 61, 64, 65, 66, 67	summolem3 13768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
69		eqeq12 2441	. . . . . . . . . . . . . . 15 $/\$
70	68, 69	syl5ibrcom 225	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	expimpd 606	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
72	55, 71	syl5bi 220	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	exlimdvv 1769	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
74	54, 73	syl5bir 221	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2924	. . . . . . . . 9 $/\$ $/\$ $/\$
76	53, 75	syl5bir 221	. . . . . . . 8 $/\$ $/\$ $/\$
77	76	expdimp 438	. . . . . . 7 $/\$ $/\$ $/\$
78	52, 77	syl5bi 220	. . . . . 6 $/\$ $/\$ $/\$
79	33, 78	jaod 381	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
80	29, 79	jaodan 792	. . . 4 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
81	80	expimpd 606	. . 3 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
82	81	alrimivv 1764	. 2 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
83		breq2 4424	. . . . . 6
84	83	anbi2d 708	. . . . 5 $/\$ $/\$
85	84	rexbidv 2939	. . . 4 $/\$ $/\$
86		eqeq1 2426	. . . . . . 7
87	86	anbi2d 708	. . . . . 6 $/\$ $/\$
88	87	exbidv 1758	. . . . 5 $/\$ $/\$
89	88	rexbidv 2939	. . . 4 $/\$ $/\$
90	85, 89	orbi12d 714	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
91	90	mo4 2313	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
92	82, 91	sylibr 215	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370

wal 1435

wceq 1437

wex 1659

wcel 1868

wmo 2266

wrex 2776

csb 3395

wss 3436

cif 3909 class class class wbr 4420

cmpt 4479

wf1o 5597

cfv 5598 (class class class)co 6302

cc 9538

cc0 9540

c1 9541

caddc 9543

cn 10610

cz 10938

cuz 11160

cfz 11785

cseq 12213

cli 13536

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-inf2 8149 ax-cnex 9596 ax-resscn 9597 ax-1cn 9598 ax-icn 9599 ax-addcl 9600 ax-addrcl 9601 ax-mulcl 9602 ax-mulrcl 9603 ax-mulcom 9604 ax-addass 9605 ax-mulass 9606 ax-distr 9607 ax-i2m1 9608 ax-1ne0 9609 ax-1rid 9610 ax-rnegex 9611 ax-rrecex 9612 ax-cnre 9613 ax-pre-lttri 9614 ax-pre-lttrn 9615 ax-pre-ltadd 9616 ax-pre-mulgt0 9617 ax-pre-sup 9618

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-se 4810 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-isom 5607 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-om 6704 df-1st 6804 df-2nd 6805 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-oadd 7191 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-sup 7959 df-oi 8028 df-card 8375 df-pnf 9678 df-mnf 9679 df-xr 9680 df-ltxr 9681 df-le 9682 df-sub 9863 df-neg 9864 df-div 10271 df-nn 10611 df-2 10669 df-3 10670 df-n0 10871 df-z 10939 df-uz 11161 df-rp 11304 df-fz 11786 df-fzo 11917 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13151 df-re 13152 df-im 13153 df-sqrt 13287 df-abs 13288 df-clim 13540

This theorem is referenced by: fsum 13774

W3C validator