summo - Metamath Proof Explorer

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

Theorem summo 13296

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 5789	. . . . . . . . . 10
2	1	sseq2d 3482	. . . . . . . . 9
3		seqeq1 11910	. . . . . . . . . 10
4	3	breq1d 4400	. . . . . . . . 9
5	2, 4	anbi12d 710	. . . . . . . 8 $/\$ $/\$
6	5	cbvrexv 3044	. . . . . . 7 $/\$ $/\$
7		reeanv 2984	. . . . . . . . 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 13292	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	8, 17	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simprrr 764	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		climuni 13132	. . . . . . . . . . . 12 $/\$
21	18, 19, 20	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22	21	exp31 604	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
23	22	rexlimdvv 2943	. . . . . . . . 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 13295	. . . . . 6 $/\$ $/\$ $/\$
29	26, 28	jaod 380	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
30	9, 11, 27	summolem2 13295	. . . . . . . 8 $/\$ $/\$ $/\$
31		equcom 1734	. . . . . . . 8
32	30, 31	syl6ib 226	. . . . . . 7 $/\$ $/\$ $/\$
33	32	impancom 440	. . . . . 6 $/\$ $/\$ $/\$
34		oveq2 6198	. . . . . . . . . . . 12
35		f1oeq2 5731	. . . . . . . . . . . 12
36	34, 35	syl 16	. . . . . . . . . . 11
37		fveq2 5789	. . . . . . . . . . . 12
38	37	eqeq2d 2465	. . . . . . . . . . 11
39	36, 38	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
40	39	exbidv 1681	. . . . . . . . 9 $/\$ $/\$
41		f1oeq1 5730	. . . . . . . . . . 11
42		fveq1 5788	. . . . . . . . . . . . . . . . 17
43	42	csbeq1d 3393	. . . . . . . . . . . . . . . 16
44	43	mpteq2dv 4477	. . . . . . . . . . . . . . 15
45	27, 44	syl5eq 2504	. . . . . . . . . . . . . 14
46	45	seqeq3d 11915	. . . . . . . . . . . . 13
47	46	fveq1d 5791	. . . . . . . . . . . 12
48	47	eqeq2d 2465	. . . . . . . . . . 11
49	41, 48	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
50	49	cbvexv 1981	. . . . . . . . 9 $/\$ $/\$
51	40, 50	syl6bb 261	. . . . . . . 8 $/\$ $/\$
52	51	cbvrexv 3044	. . . . . . 7 $/\$ $/\$
53		reeanv 2984	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		eeanv 1941	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		an4 820	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simpll 753	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	56, 11	sylan 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
58		fveq2 5789	. . . . . . . . . . . . . . . . . . 19
59	58	csbeq1d 3393	. . . . . . . . . . . . . . . . . 18
60	59	cbvmptv 4481	. . . . . . . . . . . . . . . . 17
61	27, 60	eqtri 2480	. . . . . . . . . . . . . . . 16
62		fveq2 5789	. . . . . . . . . . . . . . . . . 18
63	62	csbeq1d 3393	. . . . . . . . . . . . . . . . 17
64	63	cbvmptv 4481	. . . . . . . . . . . . . . . 16
65		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
66		simprl 755	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
68	9, 57, 61, 64, 65, 66, 67	summolem3 13293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
69		eqeq12 2470	. . . . . . . . . . . . . . 15 $/\$
70	68, 69	syl5ibrcom 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	expimpd 603	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
72	55, 71	syl5bi 217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	exlimdvv 1692	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
74	54, 73	syl5bir 218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2944	. . . . . . . . 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 1687	. 2 $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
83		breq2 4394	. . . . . 6
84	83	anbi2d 703	. . . . 5 $/\$ $/\$
85	84	rexbidv 2844	. . . 4 $/\$ $/\$
86		eqeq1 2455	. . . . . . 7
87	86	anbi2d 703	. . . . . 6 $/\$ $/\$
88	87	exbidv 1681	. . . . 5 $/\$ $/\$
89	88	rexbidv 2844	. . . 4 $/\$ $/\$
90	85, 89	orbi12d 709	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
91	90	mo4 2324	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
92	82, 91	sylibr 212	1 $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wal 1368

wceq 1370

wex 1587

wcel 1758

wmo 2261

wrex 2796

csb 3386

wss 3426

cif 3889 class class class wbr 4390

cmpt 4448

wf1o 5515

cfv 5516 (class class class)co 6190

cc 9381

cc0 9383

c1 9384

caddc 9386

cn 10423

cz 10747

cuz 10962

cfz 11538

cseq 11907

cli 13064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4501 ax-sep 4511 ax-nul 4519 ax-pow 4568 ax-pr 4629 ax-un 6472 ax-inf2 7948 ax-cnex 9439 ax-resscn 9440 ax-1cn 9441 ax-icn 9442 ax-addcl 9443 ax-addrcl 9444 ax-mulcl 9445 ax-mulrcl 9446 ax-mulcom 9447 ax-addass 9448 ax-mulass 9449 ax-distr 9450 ax-i2m1 9451 ax-1ne0 9452 ax-1rid 9453 ax-rnegex 9454 ax-rrecex 9455 ax-cnre 9456 ax-pre-lttri 9457 ax-pre-lttrn 9458 ax-pre-ltadd 9459 ax-pre-mulgt0 9460 ax-pre-sup 9461

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-pss 3442 df-nul 3736 df-if 3890 df-pw 3960 df-sn 3976 df-pr 3978 df-tp 3980 df-op 3982 df-uni 4190 df-int 4227 df-iun 4271 df-br 4391 df-opab 4449 df-mpt 4450 df-tr 4484 df-eprel 4730 df-id 4734 df-po 4739 df-so 4740 df-fr 4777 df-se 4778 df-we 4779 df-ord 4820 df-on 4821 df-lim 4822 df-suc 4823 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-res 4950 df-ima 4951 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-f1 5521 df-fo 5522 df-f1o 5523 df-fv 5524 df-isom 5525 df-riota 6151 df-ov 6193 df-oprab 6194 df-mpt2 6195 df-om 6577 df-1st 6677 df-2nd 6678 df-recs 6932 df-rdg 6966 df-1o 7020 df-oadd 7024 df-er 7201 df-en 7411 df-dom 7412 df-sdom 7413 df-fin 7414 df-sup 7792 df-oi 7825 df-card 8210 df-pnf 9521 df-mnf 9522 df-xr 9523 df-ltxr 9524 df-le 9525 df-sub 9698 df-neg 9699 df-div 10095 df-nn 10424 df-2 10481 df-3 10482 df-n0 10681 df-z 10748 df-uz 10963 df-rp 11093 df-fz 11539 df-fzo 11650 df-seq 11908 df-exp 11967 df-hash 12205 df-cj 12690 df-re 12691 df-im 12692 df-sqr 12826 df-abs 12827 df-clim 13068

This theorem is referenced by: fsum 13299

W3C validator