summo - Metamath Proof Explorer

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

Theorem summo 13488

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 5857	. . . . . . . . . 10
2	1	sseq2d 3525	. . . . . . . . 9
3		seqeq1 12066	. . . . . . . . . 10
4	3	breq1d 4450	. . . . . . . . 9
5	2, 4	anbi12d 710	. . . . . . . 8 $/\$ $/\$
6	5	cbvrexv 3082	. . . . . . 7 $/\$ $/\$
7		reeanv 3022	. . . . . . . . 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 13484	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	8, 17	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simprrr 764	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		climuni 13324	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22	21	exp31 604	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
23	22	rexlimdvv 2954	. . . . . . . . 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 13487	. . . . . 6 $/\$ $/\$ $/\$
29	26, 28	jaod 380	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
30	9, 11, 27	summolem2 13487	. . . . . . . 8 $/\$ $/\$ $/\$
31		equcom 1738	. . . . . . . 8
32	30, 31	syl6ib 226	. . . . . . 7 $/\$ $/\$ $/\$
33	32	impancom 440	. . . . . 6 $/\$ $/\$ $/\$
34		oveq2 6283	. . . . . . . . . . . 12
35		f1oeq2 5799	. . . . . . . . . . . 12
36	34, 35	syl 16	. . . . . . . . . . 11
37		fveq2 5857	. . . . . . . . . . . 12
38	37	eqeq2d 2474	. . . . . . . . . . 11
39	36, 38	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
40	39	exbidv 1685	. . . . . . . . 9 $/\$ $/\$
41		f1oeq1 5798	. . . . . . . . . . 11
42		fveq1 5856	. . . . . . . . . . . . . . . . 17
43	42	csbeq1d 3435	. . . . . . . . . . . . . . . 16
44	43	mpteq2dv 4527	. . . . . . . . . . . . . . 15
45	27, 44	syl5eq 2513	. . . . . . . . . . . . . 14
46	45	seqeq3d 12071	. . . . . . . . . . . . 13
47	46	fveq1d 5859	. . . . . . . . . . . 12
48	47	eqeq2d 2474	. . . . . . . . . . 11
49	41, 48	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
50	49	cbvexv 1990	. . . . . . . . 9 $/\$ $/\$
51	40, 50	syl6bb 261	. . . . . . . 8 $/\$ $/\$
52	51	cbvrexv 3082	. . . . . . 7 $/\$ $/\$
53		reeanv 3022	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		eeanv 1950	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		an4 821	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simpll 753	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	56, 11	sylan 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
58		fveq2 5857	. . . . . . . . . . . . . . . . . . 19
59	58	csbeq1d 3435	. . . . . . . . . . . . . . . . . 18
60	59	cbvmptv 4531	. . . . . . . . . . . . . . . . 17
61	27, 60	eqtri 2489	. . . . . . . . . . . . . . . 16
62		fveq2 5857	. . . . . . . . . . . . . . . . . 18
63	62	csbeq1d 3435	. . . . . . . . . . . . . . . . 17
64	63	cbvmptv 4531	. . . . . . . . . . . . . . . 16
65		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
66		simprl 755	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
68	9, 57, 61, 64, 65, 66, 67	summolem3 13485	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
69		eqeq12 2479	. . . . . . . . . . . . . . 15 $/\$
70	68, 69	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	expimpd 603	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
72	55, 71	syl5bi 217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	exlimdvv 1696	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
74	54, 73	syl5bir 218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2955	. . . . . . . . 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 1691	. 2 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
83		breq2 4444	. . . . . 6
84	83	anbi2d 703	. . . . 5 $/\$ $/\$
85	84	rexbidv 2966	. . . 4 $/\$ $/\$
86		eqeq1 2464	. . . . . . 7
87	86	anbi2d 703	. . . . . 6 $/\$ $/\$
88	87	exbidv 1685	. . . . 5 $/\$ $/\$
89	88	rexbidv 2966	. . . 4 $/\$ $/\$
90	85, 89	orbi12d 709	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
91	90	mo4 2332	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
92	82, 91	sylibr 212	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wal 1372

wceq 1374

wex 1591

wcel 1762

wmo 2269

wrex 2808

csb 3428

wss 3469

cif 3932 class class class wbr 4440

cmpt 4498

wf1o 5578

cfv 5579 (class class class)co 6275

cc 9479

cc0 9481

c1 9482

caddc 9484

cn 10525

cz 10853

cuz 11071

cfz 11661

cseq 12063

cli 13256

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-inf2 8047 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-se 4832 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-om 6672 df-1st 6774 df-2nd 6775 df-recs 7032 df-rdg 7066 df-1o 7120 df-oadd 7124 df-er 7301 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-sup 7890 df-oi 7924 df-card 8309 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-div 10196 df-nn 10526 df-2 10583 df-3 10584 df-n0 10785 df-z 10854 df-uz 11072 df-rp 11210 df-fz 11662 df-fzo 11782 df-seq 12064 df-exp 12123 df-hash 12361 df-cj 12882 df-re 12883 df-im 12884 df-sqr 13018 df-abs 13019 df-clim 13260

This theorem is referenced by: fsum 13491

W3C validator