limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 13520

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.) (Revised by AV, 12-Sep-2020.)

**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 11440	. . . 4
2	1	supex 7983	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 13512	. . . 4
7	6	adantl 467	. . 3 $/\$ $/\$ $/\$
8		simpl3 1010	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 11178	. . . . . . . . . . 11
11	9, 10	eqsstri 3500	. . . . . . . . . 10
12		zssre 10944	. . . . . . . . . 10
13	11, 12	sstri 3479	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 1009	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9683	. . . . . . . . 9
17		fss 5754	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 666	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11412	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 13516	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1264	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 213	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 12182	. . . . . . . 8
25	15	adantr 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11794	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2528	. . . . . . . . . 10
28		ffvelrn 6035	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 479	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2846	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10553	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 462	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 730	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 13511	. . . . . . . . . 10
36	35	ffvelrni 6036	. . . . . . . . 9
37	34, 36	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 762	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 6036	. . . . . . . . . 10
43	41, 42	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	39, 43	ifcld 3958	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	40	ad2antrr 730	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	47	sselda 3470	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		xrleid 11449	. . . . . . . . . . . . . . . . 17
50	43, 49	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	18	ad2antrr 730	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	4	limsupgle 13513	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
53	47, 51, 41, 43, 52	syl211anc 1270	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	50, 53	mpbid 213	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	r19.21bi 2801	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	imp 430	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	46, 42	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	39	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		xrmax1 11470	. . . . . . . . . . . . . . . 16 $/\$
60	57, 58, 59	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	51	ffvelrnda 6037	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	44	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		xrletr 11455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
64	61, 57, 62, 63	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	60, 64	mpan2d 678	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	65	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	56, 66	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simpr 462	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68, 9	syl6eleq 2527	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	41	flcld 12031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		elfz5 11790	. . . . . . . . . . . . . . . . 17 $/\$
73	69, 71, 72	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 68	sseldi 3468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		flge 12038	. . . . . . . . . . . . . . . . 17 $/\$
76	46, 74, 75	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	73, 76	bitr4d 259	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	biimpar 487	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprr 764	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ad2antrr 730	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		fveq2 5881	. . . . . . . . . . . . . . . 16
82	81	breq1d 4436	. . . . . . . . . . . . . . 15
83	82	rspcv 3184	. . . . . . . . . . . . . 14
84	78, 80, 83	sylc 62	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		xrmax2 11471	. . . . . . . . . . . . . . . . 17 $/\$
86	43, 39, 85	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		xrletr 11455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
89	61, 58, 62, 88	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 89	mpan2d 678	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	90	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	84, 91	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	46, 48, 67, 92	lecasei 9739	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	93	a1d 26	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	ralrimiva 2846	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	4	limsupgle 13513	. . . . . . . . . 10 $/\$ $/\$ $/\$
97	47, 51, 34, 44, 96	syl211anc 1270	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	mpbird 235	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	38	ltpnfd 11423	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		simplrr 769	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		breq1 4429	. . . . . . . . . 10
102		breq1 4429	. . . . . . . . . 10
103	101, 102	ifboth 3951	. . . . . . . . 9 $/\$
104	99, 100, 103	syl2anc 665	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	37, 44, 45, 98, 104	xrlelttrd 11457	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	32, 105	rexlimddv 2928	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
107	23, 106	rexlimddv 2928	. . . . 5 $/\$ $/\$ $/\$
108	7, 107	eqbrtrrd 4448	. . . 4 $/\$ $/\$ $/\$
109		imassrn 5199	. . . . . . . . 9
110		frn 5752	. . . . . . . . . 10
111	15, 110	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
112	109, 111	syl5ss 3481	. . . . . . . 8 $/\$ $/\$ $/\$
113	112, 16	syl6ss 3482	. . . . . . 7 $/\$ $/\$ $/\$
114		df-ss 3456	. . . . . . 7
115	113, 114	sylib 199	. . . . . 6 $/\$ $/\$ $/\$
116	115, 112	eqsstrd 3504	. . . . 5 $/\$ $/\$ $/\$
117		simpl1 1008	. . . . . . . . . . 11 $/\$ $/\$ $/\$
118		flcl 12028	. . . . . . . . . . . . . 14
119	118	adantl 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	peano2zd 11043	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	120, 117	ifcld 3958	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122	117	zred 11040	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123	120	zred 11040	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		max1 11480	. . . . . . . . . . . 12 $/\$
125	122, 123, 124	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
126		eluz2 11165	. . . . . . . . . . 11 $/\$ $/\$
127	117, 121, 125, 126	syl3anbrc 1189	. . . . . . . . . 10 $/\$ $/\$ $/\$
128	127, 9	syl6eleqr 2528	. . . . . . . . 9 $/\$ $/\$ $/\$
129		fdm 5750	. . . . . . . . . 10
130	15, 129	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
131	128, 130	eleqtrrd 2520	. . . . . . . 8 $/\$ $/\$ $/\$
132	121	zred 11040	. . . . . . . . 9 $/\$ $/\$ $/\$
133		fllep1 12034	. . . . . . . . . . 11
134	133	adantl 467	. . . . . . . . . 10 $/\$ $/\$ $/\$
135		max2 11482	. . . . . . . . . . 11 $/\$
136	122, 123, 135	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
137	33, 123, 132, 134, 136	letrd 9791	. . . . . . . . 9 $/\$ $/\$ $/\$
138		elicopnf 11730	. . . . . . . . . 10 $/\$
139	138	adantl 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
140	132, 137, 139	mpbir2and 930	. . . . . . . 8 $/\$ $/\$ $/\$
141		inelcm 3853	. . . . . . . 8 $/\$
142	131, 140, 141	syl2anc 665	. . . . . . 7 $/\$ $/\$ $/\$
143		imadisj 5207	. . . . . . . 8
144	143	necon3bii 2699	. . . . . . 7
145	142, 144	sylibr 215	. . . . . 6 $/\$ $/\$ $/\$
146	115, 145	eqnetrd 2724	. . . . 5 $/\$ $/\$ $/\$
147		supxrre1 11616	. . . . 5 $/\$
148	116, 146, 147	syl2anc 665	. . . 4 $/\$ $/\$ $/\$
149	108, 148	mpbird 235	. . 3 $/\$ $/\$ $/\$
150	7, 149	eqeltrd 2517	. 2 $/\$ $/\$ $/\$
151	3, 5, 150	fmpt2d 6068	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1870

wne 2625

wral 2782

wrex 2783

cvv 3087

cin 3441

wss 3442

c0 3767

cif 3915 class class class wbr 4426

cmpt 4484

cdm 4854

crn 4855

cima 4857

wf 5597

cfv 5601 (class class class)co 6305

cfn 7577

csup 7960

cr 9537

c1 9539

caddc 9541

cpnf 9671

cxr 9673

clt 9674

cle 9675

cz 10937

cuz 11159

cico 11637

cfz 11782

cfl 12023

clsp 13502

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-oadd 7194 df-er 7371 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-sup 7962 df-inf 7963 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-nn 10610 df-n0 10870 df-z 10938 df-uz 11160 df-ico 11641 df-fz 11783 df-fl 12025 df-limsup 13504

This theorem is referenced by: mbflimsup 22500

W3C validator