limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 12951

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 11110	. . . 4
2	1	supex 7705	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 12946	. . . 4
7	6	adantl 466	. . 3 $/\$ $/\$ $/\$
8		simpl3 993	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 10872	. . . . . . . . . . 11
11	9, 10	eqsstri 3381	. . . . . . . . . 10
12		zssre 10645	. . . . . . . . . 10
13	11, 12	sstri 3360	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 992	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9419	. . . . . . . . 9
17		fss 5562	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11084	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 12949	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1218	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 11786	. . . . . . . 8
25	15	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11441	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2529	. . . . . . . . . 10
28		ffvelrn 5836	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2794	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10271	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 12945	. . . . . . . . . 10
36	35	ffvelrni 5837	. . . . . . . . 9
37	34, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 755	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3349	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 755	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 5837	. . . . . . . . . 10
43	41, 42	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		ifcl 3826	. . . . . . . . 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 3351	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		xrleid 11119	. . . . . . . . . . . . . . . . 17
51	43, 50	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	18	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	4	limsupgle 12947	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
54	48, 52, 41, 43, 53	syl211anc 1224	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	r19.21bi 2809	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	47, 42	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		xrmax1 11139	. . . . . . . . . . . . . . . 16 $/\$
61	58, 59, 60	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	52	ffvelrnda 5838	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	45	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		xrletr 11124	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
65	62, 58, 63, 64	syl3anc 1218	. . . . . . . . . . . . . . 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 2528	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	41	flcld 11640	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		elfz5 11437	. . . . . . . . . . . . . . . . 17 $/\$
74	70, 72, 73	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	11, 69	sseldi 3349	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		flge 11647	. . . . . . . . . . . . . . . . 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 5686	. . . . . . . . . . . . . . . 16
83	82	breq1d 4297	. . . . . . . . . . . . . . 15
84	83	rspcv 3064	. . . . . . . . . . . . . 14
85	79, 81, 84	sylc 60	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		xrmax2 11140	. . . . . . . . . . . . . . . . 17 $/\$
87	43, 39, 86	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		xrletr 11124	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	62, 59, 63, 89	syl3anc 1218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	88, 90	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	91	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	85, 92	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	47, 49, 68, 93	lecasei 9472	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	a1d 25	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	ralrimiva 2794	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	4	limsupgle 12947	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	48, 52, 34, 45, 97	syl211anc 1224	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ltpnf 11094	. . . . . . . . . 10
101	38, 100	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simplrr 760	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		breq1 4290	. . . . . . . . . 10
104		breq1 4290	. . . . . . . . . 10
105	103, 104	ifboth 3820	. . . . . . . . 9 $/\$
106	101, 102, 105	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	37, 45, 46, 99, 106	xrlelttrd 11126	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108	32, 107	rexlimddv 2840	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	23, 108	rexlimddv 2840	. . . . 5 $/\$ $/\$ $/\$
110	7, 109	eqbrtrrd 4309	. . . 4 $/\$ $/\$ $/\$
111		imassrn 5175	. . . . . . . . 9
112		frn 5560	. . . . . . . . . 10
113	15, 112	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
114	111, 113	syl5ss 3362	. . . . . . . 8 $/\$ $/\$ $/\$
115	114, 16	syl6ss 3363	. . . . . . 7 $/\$ $/\$ $/\$
116		df-ss 3337	. . . . . . 7
117	115, 116	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
118	117, 114	eqsstrd 3385	. . . . 5 $/\$ $/\$ $/\$
119		simpl1 991	. . . . . . . . . . 11 $/\$ $/\$ $/\$
120		flcl 11637	. . . . . . . . . . . . . 14
121	120	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122	121	peano2zd 10742	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123		ifcl 3826	. . . . . . . . . . . 12 $/\$
124	122, 119, 123	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	119	zred 10739	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	122	zred 10739	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
127		max1 11149	. . . . . . . . . . . 12 $/\$
128	125, 126, 127	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
129		eluz2 10859	. . . . . . . . . . 11 $/\$ $/\$
130	119, 124, 128, 129	syl3anbrc 1172	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	130, 9	syl6eleqr 2529	. . . . . . . . 9 $/\$ $/\$ $/\$
132		fdm 5558	. . . . . . . . . 10
133	15, 132	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
134	131, 133	eleqtrrd 2515	. . . . . . . 8 $/\$ $/\$ $/\$
135	124	zred 10739	. . . . . . . . 9 $/\$ $/\$ $/\$
136		fllep1 11643	. . . . . . . . . . 11
137	136	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
138		max2 11151	. . . . . . . . . . 11 $/\$
139	125, 126, 138	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
140	33, 126, 135, 137, 139	letrd 9520	. . . . . . . . 9 $/\$ $/\$ $/\$
141		elicopnf 11377	. . . . . . . . . 10 $/\$
142	141	adantl 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
143	135, 140, 142	mpbir2and 913	. . . . . . . 8 $/\$ $/\$ $/\$
144		inelcm 3728	. . . . . . . 8 $/\$
145	134, 143, 144	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
146		imadisj 5183	. . . . . . . 8
147	146	necon3bii 2635	. . . . . . 7
148	145, 147	sylibr 212	. . . . . 6 $/\$ $/\$ $/\$
149	117, 148	eqnetrd 2621	. . . . 5 $/\$ $/\$ $/\$
150		supxrre1 11285	. . . . 5 $/\$
151	118, 149, 150	syl2anc 661	. . . 4 $/\$ $/\$ $/\$
152	110, 151	mpbird 232	. . 3 $/\$ $/\$ $/\$
153	7, 152	eqeltrd 2512	. 2 $/\$ $/\$ $/\$
154	3, 5, 153	fmpt2d 5868	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wne 2601

wral 2710

wrex 2711

cvv 2967

cin 3322

wss 3323

c0 3632

cif 3786 class class class wbr 4287

cmpt 4345

cdm 4835

crn 4836

cima 4838

wf 5409

cfv 5413 (class class class)co 6086

cfn 7302

csup 7682

cr 9273

c1 9275

caddc 9277

cpnf 9407

cxr 9409

clt 9410

cle 9411

cz 10638

cuz 10853

cico 11294

cfz 11429

cfl 11632

clsp 12940

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-sup 7683 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-nn 10315 df-n0 10572 df-z 10639 df-uz 10854 df-ico 11298 df-fz 11430 df-fl 11634 df-limsup 12941

This theorem is referenced by: mbflimsup 21119

W3C validator