limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 12230

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 10690	. . . 4
2	1	supex 7424	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 12225	. . . 4
7	6	adantl 453	. . 3 $/\$ $/\$ $/\$
8		simpl3 962	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 10461	. . . . . . . . . . 11
11	9, 10	eqsstri 3338	. . . . . . . . . 10
12		zssre 10245	. . . . . . . . . 10
13	11, 12	sstri 3317	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 961	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9085	. . . . . . . . 9
17		fss 5558	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 644	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 10669	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 12228	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1184	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 202	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 11266	. . . . . . . 8
25	15	adantr 452	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11011	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2495	. . . . . . . . . 10
28		ffvelrn 5827	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 464	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2749	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 9913	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 645	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 448	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 707	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 12224	. . . . . . . . . 10
36	35	ffvelrni 5828	. . . . . . . . 9
37	34, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 733	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3306	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 733	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 452	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 5828	. . . . . . . . . 10
43	41, 42	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		ifcl 3735	. . . . . . . . 9 $/\$
45	39, 43, 44	syl2anc 643	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	40	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	sselda 3308	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		xrleid 10699	. . . . . . . . . . . . . . . . 17
51	43, 50	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	18	ad2antrr 707	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	4	limsupgle 12226	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
54	48, 52, 41, 43, 53	syl211anc 1190	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	mpbid 202	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	r19.21bi 2764	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	imp 419	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	47, 42	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	39	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		xrmax1 10719	. . . . . . . . . . . . . . . 16 $/\$
61	58, 59, 60	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	52	ffvelrnda 5829	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	45	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		xrletr 10704	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
65	62, 58, 63, 64	syl3anc 1184	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	61, 65	mpan2d 656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	57, 67	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		simpr 448	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	69, 9	syl6eleq 2494	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	41	flcld 11162	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		elfz5 11007	. . . . . . . . . . . . . . . . 17 $/\$
74	70, 72, 73	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	11, 69	sseldi 3306	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		flge 11169	. . . . . . . . . . . . . . . . 17 $/\$
77	47, 75, 76	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	74, 77	bitr4d 248	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	biimpar 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80		simprr 734	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	80	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82		fveq2 5687	. . . . . . . . . . . . . . . 16
83	82	breq1d 4182	. . . . . . . . . . . . . . 15
84	83	rspcv 3008	. . . . . . . . . . . . . 14
85	79, 81, 84	sylc 58	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		xrmax2 10720	. . . . . . . . . . . . . . . . 17 $/\$
87	43, 39, 86	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	adantr 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		xrletr 10704	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	62, 59, 63, 89	syl3anc 1184	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	88, 90	mpan2d 656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	91	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	85, 92	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	47, 49, 68, 93	lecasei 9135	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	a1d 23	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	ralrimiva 2749	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	4	limsupgle 12226	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	48, 52, 34, 45, 97	syl211anc 1190	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbird 224	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ltpnf 10677	. . . . . . . . . 10
101	38, 100	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simplrr 738	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		breq1 4175	. . . . . . . . . 10
104		breq1 4175	. . . . . . . . . 10
105	103, 104	ifboth 3730	. . . . . . . . 9 $/\$
106	101, 102, 105	syl2anc 643	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	37, 45, 46, 99, 106	xrlelttrd 10706	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108	32, 107	rexlimddv 2794	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	23, 108	rexlimddv 2794	. . . . 5 $/\$ $/\$ $/\$
110	7, 109	eqbrtrrd 4194	. . . 4 $/\$ $/\$ $/\$
111		imassrn 5175	. . . . . . . . 9
112		frn 5556	. . . . . . . . . 10
113	15, 112	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
114	111, 113	syl5ss 3319	. . . . . . . 8 $/\$ $/\$ $/\$
115	114, 16	syl6ss 3320	. . . . . . 7 $/\$ $/\$ $/\$
116		df-ss 3294	. . . . . . 7
117	115, 116	sylib 189	. . . . . 6 $/\$ $/\$ $/\$
118	117, 114	eqsstrd 3342	. . . . 5 $/\$ $/\$ $/\$
119		simpl1 960	. . . . . . . . . . 11 $/\$ $/\$ $/\$
120		flcl 11159	. . . . . . . . . . . . . 14
121	120	adantl 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122	121	peano2zd 10334	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123		ifcl 3735	. . . . . . . . . . . 12 $/\$
124	122, 119, 123	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	119	zred 10331	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	122	zred 10331	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
127		max1 10729	. . . . . . . . . . . 12 $/\$
128	125, 126, 127	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$
129		eluz2 10450	. . . . . . . . . . 11 $/\$ $/\$
130	119, 124, 128, 129	syl3anbrc 1138	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	130, 9	syl6eleqr 2495	. . . . . . . . 9 $/\$ $/\$ $/\$
132		fdm 5554	. . . . . . . . . 10
133	15, 132	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
134	131, 133	eleqtrrd 2481	. . . . . . . 8 $/\$ $/\$ $/\$
135	124	zred 10331	. . . . . . . . 9 $/\$ $/\$ $/\$
136		fllep1 11165	. . . . . . . . . . 11
137	136	adantl 453	. . . . . . . . . 10 $/\$ $/\$ $/\$
138		max2 10731	. . . . . . . . . . 11 $/\$
139	125, 126, 138	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$ $/\$
140	33, 126, 135, 137, 139	letrd 9183	. . . . . . . . 9 $/\$ $/\$ $/\$
141		elicopnf 10956	. . . . . . . . . 10 $/\$
142	141	adantl 453	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
143	135, 140, 142	mpbir2and 889	. . . . . . . 8 $/\$ $/\$ $/\$
144		inelcm 3642	. . . . . . . 8 $/\$
145	134, 143, 144	syl2anc 643	. . . . . . 7 $/\$ $/\$ $/\$
146		imadisj 5182	. . . . . . . 8
147	146	necon3bii 2599	. . . . . . 7
148	145, 147	sylibr 204	. . . . . 6 $/\$ $/\$ $/\$
149	117, 148	eqnetrd 2585	. . . . 5 $/\$ $/\$ $/\$
150		supxrre1 10865	. . . . 5 $/\$
151	118, 149, 150	syl2anc 643	. . . 4 $/\$ $/\$ $/\$
152	110, 151	mpbird 224	. . 3 $/\$ $/\$ $/\$
153	7, 152	eqeltrd 2478	. 2 $/\$ $/\$ $/\$
154	3, 5, 153	fmpt2d 5857	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cvv 2916

cin 3279

wss 3280

c0 3588

cif 3699 class class class wbr 4172

cmpt 4226

cdm 4837

crn 4838

cima 4840

wf 5409

cfv 5413 (class class class)co 6040

cfn 7068

csup 7403

cr 8945

c1 8947

caddc 8949

cpnf 9073

cxr 9075

clt 9076

cle 9077

cz 10238

cuz 10444

cico 10874

cfz 10999

cfl 11156

clsp 12219

This theorem is referenced by: mbflimsup 19511

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-n0 10178 df-z 10239 df-uz 10445 df-ico 10878 df-fz 11000 df-fl 11157 df-limsup 12220

W3C validator