summo - Metamath Proof Explorer

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

Theorem summo 13688

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 5849	. . . . . . . . . 10
2	1	sseq2d 3470	. . . . . . . . 9
3		seqeq1 12154	. . . . . . . . . 10
4	3	breq1d 4405	. . . . . . . . 9
5	2, 4	anbi12d 709	. . . . . . . 8 $/\$ $/\$
6	5	cbvrexv 3035	. . . . . . 7 $/\$ $/\$
7		reeanv 2975	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simprlr 765	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		summo.1	. . . . . . . . . . . . . 14
10		simpll 752	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		summo.2	. . . . . . . . . . . . . . 15 $/\$
12	10, 11	sylan 469	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simplrl 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simplrr 763	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simprll 764	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simprrl 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	9, 12, 13, 14, 15, 16	sumrb 13684	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	8, 17	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simprrr 767	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		climuni 13524	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22	21	exp31 602	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
23	22	rexlimdvv 2902	. . . . . . . . 9 $/\$ $/\$ $/\$
24	7, 23	syl5bir 218	. . . . . . . 8 $/\$ $/\$ $/\$
25	24	expdimp 435	. . . . . . 7 $/\$ $/\$ $/\$
26	6, 25	syl5bi 217	. . . . . 6 $/\$ $/\$ $/\$
27		summo.3	. . . . . . 7
28	9, 11, 27	summolem2 13687	. . . . . 6 $/\$ $/\$ $/\$
29	26, 28	jaod 378	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
30	9, 11, 27	summolem2 13687	. . . . . . . 8 $/\$ $/\$ $/\$
31		equcom 1818	. . . . . . . 8
32	30, 31	syl6ib 226	. . . . . . 7 $/\$ $/\$ $/\$
33	32	impancom 438	. . . . . 6 $/\$ $/\$ $/\$
34		oveq2 6286	. . . . . . . . . . . 12
35		f1oeq2 5791	. . . . . . . . . . . 12
36	34, 35	syl 17	. . . . . . . . . . 11
37		fveq2 5849	. . . . . . . . . . . 12
38	37	eqeq2d 2416	. . . . . . . . . . 11
39	36, 38	anbi12d 709	. . . . . . . . . 10 $/\$ $/\$
40	39	exbidv 1735	. . . . . . . . 9 $/\$ $/\$
41		f1oeq1 5790	. . . . . . . . . . 11
42		fveq1 5848	. . . . . . . . . . . . . . . . 17
43	42	csbeq1d 3380	. . . . . . . . . . . . . . . 16
44	43	mpteq2dv 4482	. . . . . . . . . . . . . . 15
45	27, 44	syl5eq 2455	. . . . . . . . . . . . . 14
46	45	seqeq3d 12159	. . . . . . . . . . . . 13
47	46	fveq1d 5851	. . . . . . . . . . . 12
48	47	eqeq2d 2416	. . . . . . . . . . 11
49	41, 48	anbi12d 709	. . . . . . . . . 10 $/\$ $/\$
50	49	cbvexv 2051	. . . . . . . . 9 $/\$ $/\$
51	40, 50	syl6bb 261	. . . . . . . 8 $/\$ $/\$
52	51	cbvrexv 3035	. . . . . . 7 $/\$ $/\$
53		reeanv 2975	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		eeanv 2016	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		an4 825	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simpll 752	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	56, 11	sylan 469	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
58		fveq2 5849	. . . . . . . . . . . . . . . . . . 19
59	58	csbeq1d 3380	. . . . . . . . . . . . . . . . . 18
60	59	cbvmptv 4487	. . . . . . . . . . . . . . . . 17
61	27, 60	eqtri 2431	. . . . . . . . . . . . . . . 16
62		fveq2 5849	. . . . . . . . . . . . . . . . . 18
63	62	csbeq1d 3380	. . . . . . . . . . . . . . . . 17
64	63	cbvmptv 4487	. . . . . . . . . . . . . . . 16
65		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
66		simprl 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67		simprr 758	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
68	9, 57, 61, 64, 65, 66, 67	summolem3 13685	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
69		eqeq12 2421	. . . . . . . . . . . . . . 15 $/\$
70	68, 69	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	expimpd 601	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
72	55, 71	syl5bi 217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	exlimdvv 1746	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
74	54, 73	syl5bir 218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2903	. . . . . . . . 9 $/\$ $/\$ $/\$
76	53, 75	syl5bir 218	. . . . . . . 8 $/\$ $/\$ $/\$
77	76	expdimp 435	. . . . . . 7 $/\$ $/\$ $/\$
78	52, 77	syl5bi 217	. . . . . 6 $/\$ $/\$ $/\$
79	33, 78	jaod 378	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
80	29, 79	jaodan 786	. . . 4 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
81	80	expimpd 601	. . 3 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
82	81	alrimivv 1741	. 2 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
83		breq2 4399	. . . . . 6
84	83	anbi2d 702	. . . . 5 $/\$ $/\$
85	84	rexbidv 2918	. . . 4 $/\$ $/\$
86		eqeq1 2406	. . . . . . 7
87	86	anbi2d 702	. . . . . 6 $/\$ $/\$
88	87	exbidv 1735	. . . . 5 $/\$ $/\$
89	88	rexbidv 2918	. . . 4 $/\$ $/\$
90	85, 89	orbi12d 708	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
91	90	mo4 2289	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
92	82, 91	sylibr 212	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wal 1403

wceq 1405

wex 1633

wcel 1842

wmo 2239

wrex 2755

csb 3373

wss 3414

cif 3885 class class class wbr 4395

cmpt 4453

wf1o 5568

cfv 5569 (class class class)co 6278

cc 9520

cc0 9522

c1 9523

caddc 9525

cn 10576

cz 10905

cuz 11127

cfz 11726

cseq 12151

cli 13456

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-inf2 8091 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599 ax-pre-sup 9600

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2759 df-rex 2760 df-reu 2761 df-rmo 2762 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-pss 3430 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4192 df-int 4228 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4490 df-eprel 4734 df-id 4738 df-po 4744 df-so 4745 df-fr 4782 df-se 4783 df-we 4784 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-pred 5367 df-ord 5413 df-on 5414 df-lim 5415 df-suc 5416 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-isom 5578 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6684 df-1st 6784 df-2nd 6785 df-wrecs 7013 df-recs 7075 df-rdg 7113 df-1o 7167 df-oadd 7171 df-er 7348 df-en 7555 df-dom 7556 df-sdom 7557 df-fin 7558 df-sup 7935 df-oi 7969 df-card 8352 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-div 10248 df-nn 10577 df-2 10635 df-3 10636 df-n0 10837 df-z 10906 df-uz 11128 df-rp 11266 df-fz 11727 df-fzo 11855 df-seq 12152 df-exp 12211 df-hash 12453 df-cj 13081 df-re 13082 df-im 13083 df-sqrt 13217 df-abs 13218 df-clim 13460

This theorem is referenced by: fsum 13691

W3C validator