limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 13267

Description: If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014.)

**Hypotheses**
Ref	Expression
limsupval.1
limsupgre.z

**Assertion**
Ref	Expression
limsupgre	$/\$ $/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem limsupgre Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrltso 11347	. . . 4
2	1	supex 7923	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 13262	. . . 4
7	6	adantl 466	. . 3 $/\$ $/\$ $/\$
8		simpl3 1001	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 11101	. . . . . . . . . . 11
11	9, 10	eqsstri 3534	. . . . . . . . . 10
12		zssre 10871	. . . . . . . . . 10
13	11, 12	sstri 3513	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 1000	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9637	. . . . . . . . 9
17		fss 5739	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11321	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 13265	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 12050	. . . . . . . 8
25	15	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11684	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2566	. . . . . . . . . 10
28		ffvelrn 6019	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2878	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10492	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 13261	. . . . . . . . . 10
36	35	ffvelrni 6020	. . . . . . . . 9
37	34, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 755	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3502	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 755	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 6020	. . . . . . . . . 10
43	41, 42	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		ifcl 3981	. . . . . . . . 9 $/\$
45	39, 43, 44	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	40	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	sselda 3504	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		xrleid 11356	. . . . . . . . . . . . . . . . 17
51	43, 50	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	18	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	4	limsupgle 13263	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
54	48, 52, 41, 43, 53	syl211anc 1234	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	r19.21bi 2833	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	47, 42	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		xrmax1 11376	. . . . . . . . . . . . . . . 16 $/\$
61	58, 59, 60	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	52	ffvelrnda 6021	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	45	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		xrletr 11361	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
65	62, 58, 63, 64	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	61, 65	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	57, 67	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	69, 9	syl6eleq 2565	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	41	flcld 11903	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		elfz5 11680	. . . . . . . . . . . . . . . . 17 $/\$
74	70, 72, 73	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	11, 69	sseldi 3502	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		flge 11910	. . . . . . . . . . . . . . . . 17 $/\$
77	47, 75, 76	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	74, 77	bitr4d 256	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	biimpar 485	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80		simprr 756	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	80	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82		fveq2 5866	. . . . . . . . . . . . . . . 16
83	82	breq1d 4457	. . . . . . . . . . . . . . 15
84	83	rspcv 3210	. . . . . . . . . . . . . 14
85	79, 81, 84	sylc 60	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		xrmax2 11377	. . . . . . . . . . . . . . . . 17 $/\$
87	43, 39, 86	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		xrletr 11361	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	62, 59, 63, 89	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	88, 90	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	91	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	85, 92	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	47, 49, 68, 93	lecasei 9690	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	a1d 25	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	ralrimiva 2878	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	4	limsupgle 13263	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	48, 52, 34, 45, 97	syl211anc 1234	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ltpnf 11331	. . . . . . . . . 10
101	38, 100	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simplrr 760	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		breq1 4450	. . . . . . . . . 10
104		breq1 4450	. . . . . . . . . 10
105	103, 104	ifboth 3975	. . . . . . . . 9 $/\$
106	101, 102, 105	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	37, 45, 46, 99, 106	xrlelttrd 11363	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108	32, 107	rexlimddv 2959	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	23, 108	rexlimddv 2959	. . . . 5 $/\$ $/\$ $/\$
110	7, 109	eqbrtrrd 4469	. . . 4 $/\$ $/\$ $/\$
111		imassrn 5348	. . . . . . . . 9
112		frn 5737	. . . . . . . . . 10
113	15, 112	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
114	111, 113	syl5ss 3515	. . . . . . . 8 $/\$ $/\$ $/\$
115	114, 16	syl6ss 3516	. . . . . . 7 $/\$ $/\$ $/\$
116		df-ss 3490	. . . . . . 7
117	115, 116	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
118	117, 114	eqsstrd 3538	. . . . 5 $/\$ $/\$ $/\$
119		simpl1 999	. . . . . . . . . . 11 $/\$ $/\$ $/\$
120		flcl 11900	. . . . . . . . . . . . . 14
121	120	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122	121	peano2zd 10969	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123		ifcl 3981	. . . . . . . . . . . 12 $/\$
124	122, 119, 123	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	119	zred 10966	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	122	zred 10966	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
127		max1 11386	. . . . . . . . . . . 12 $/\$
128	125, 126, 127	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
129		eluz2 11088	. . . . . . . . . . 11 $/\$ $/\$
130	119, 124, 128, 129	syl3anbrc 1180	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	130, 9	syl6eleqr 2566	. . . . . . . . 9 $/\$ $/\$ $/\$
132		fdm 5735	. . . . . . . . . 10
133	15, 132	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
134	131, 133	eleqtrrd 2558	. . . . . . . 8 $/\$ $/\$ $/\$
135	124	zred 10966	. . . . . . . . 9 $/\$ $/\$ $/\$
136		fllep1 11906	. . . . . . . . . . 11
137	136	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
138		max2 11388	. . . . . . . . . . 11 $/\$
139	125, 126, 138	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
140	33, 126, 135, 137, 139	letrd 9738	. . . . . . . . 9 $/\$ $/\$ $/\$
141		elicopnf 11620	. . . . . . . . . 10 $/\$
142	141	adantl 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
143	135, 140, 142	mpbir2and 920	. . . . . . . 8 $/\$ $/\$ $/\$
144		inelcm 3881	. . . . . . . 8 $/\$
145	134, 143, 144	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
146		imadisj 5356	. . . . . . . 8
147	146	necon3bii 2735	. . . . . . 7
148	145, 147	sylibr 212	. . . . . 6 $/\$ $/\$ $/\$
149	117, 148	eqnetrd 2760	. . . . 5 $/\$ $/\$ $/\$
150		supxrre1 11522	. . . . 5 $/\$
151	118, 149, 150	syl2anc 661	. . . 4 $/\$ $/\$ $/\$
152	110, 151	mpbird 232	. . 3 $/\$ $/\$ $/\$
153	7, 152	eqeltrd 2555	. 2 $/\$ $/\$ $/\$
154	3, 5, 153	fmpt2d 6051	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767

wne 2662

wral 2814

wrex 2815

cvv 3113

cin 3475

wss 3476

c0 3785

cif 3939 class class class wbr 4447

cmpt 4505

cdm 4999

crn 5000

cima 5002

wf 5584

cfv 5588 (class class class)co 6284

cfn 7516

csup 7900

cr 9491

c1 9493

caddc 9495

cpnf 9625

cxr 9627

clt 9628

cle 9629

cz 10864

cuz 11082

cico 11531

cfz 11672

cfl 11895

clsp 13256

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-sup 7901 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-nn 10537 df-n0 10796 df-z 10865 df-uz 11083 df-ico 11535 df-fz 11673 df-fl 11897 df-limsup 13257

This theorem is referenced by: mbflimsup 21836

W3C validator