limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 12943

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 11106	. . . 4
2	1	supex 7701	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 12938	. . . 4
7	6	adantl 463	. . 3 $/\$ $/\$ $/\$
8		simpl3 986	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 10868	. . . . . . . . . . 11
11	9, 10	eqsstri 3374	. . . . . . . . . 10
12		zssre 10641	. . . . . . . . . 10
13	11, 12	sstri 3353	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 985	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9415	. . . . . . . . 9
17		fss 5555	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 655	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11080	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 12941	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1211	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 11778	. . . . . . . 8
25	15	adantr 462	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11436	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2524	. . . . . . . . . 10
28		ffvelrn 5829	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 474	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2789	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10267	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 656	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 458	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 718	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 12937	. . . . . . . . . 10
36	35	ffvelrni 5830	. . . . . . . . 9
37	34, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 748	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3342	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 748	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 462	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 5830	. . . . . . . . . 10
43	41, 42	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		ifcl 3819	. . . . . . . . 9 $/\$
45	39, 43, 44	syl2anc 654	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	40	ad2antrr 718	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	sselda 3344	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		xrleid 11115	. . . . . . . . . . . . . . . . 17
51	43, 50	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	18	ad2antrr 718	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	4	limsupgle 12939	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
54	48, 52, 41, 43, 53	syl211anc 1217	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	r19.21bi 2804	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	47, 42	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	39	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		xrmax1 11135	. . . . . . . . . . . . . . . 16 $/\$
61	58, 59, 60	syl2anc 654	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	52	ffvelrnda 5831	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	45	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		xrletr 11120	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
65	62, 58, 63, 64	syl3anc 1211	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	61, 65	mpan2d 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	57, 67	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		simpr 458	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	69, 9	syl6eleq 2523	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	41	flcld 11632	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		elfz5 11432	. . . . . . . . . . . . . . . . 17 $/\$
74	70, 72, 73	syl2anc 654	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	11, 69	sseldi 3342	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		flge 11639	. . . . . . . . . . . . . . . . 17 $/\$
77	47, 75, 76	syl2anc 654	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	74, 77	bitr4d 256	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	biimpar 482	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80		simprr 749	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	80	ad2antrr 718	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82		fveq2 5679	. . . . . . . . . . . . . . . 16
83	82	breq1d 4290	. . . . . . . . . . . . . . 15
84	83	rspcv 3058	. . . . . . . . . . . . . 14
85	79, 81, 84	sylc 60	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		xrmax2 11136	. . . . . . . . . . . . . . . . 17 $/\$
87	43, 39, 86	syl2anc 654	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	adantr 462	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		xrletr 11120	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	62, 59, 63, 89	syl3anc 1211	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	88, 90	mpan2d 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	91	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	85, 92	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	47, 49, 68, 93	lecasei 9468	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	a1d 25	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	ralrimiva 2789	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	4	limsupgle 12939	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	48, 52, 34, 45, 97	syl211anc 1217	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ltpnf 11090	. . . . . . . . . 10
101	38, 100	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simplrr 753	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		breq1 4283	. . . . . . . . . 10
104		breq1 4283	. . . . . . . . . 10
105	103, 104	ifboth 3813	. . . . . . . . 9 $/\$
106	101, 102, 105	syl2anc 654	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	37, 45, 46, 99, 106	xrlelttrd 11122	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108	32, 107	rexlimddv 2835	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	23, 108	rexlimddv 2835	. . . . 5 $/\$ $/\$ $/\$
110	7, 109	eqbrtrrd 4302	. . . 4 $/\$ $/\$ $/\$
111		imassrn 5168	. . . . . . . . 9
112		frn 5553	. . . . . . . . . 10
113	15, 112	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
114	111, 113	syl5ss 3355	. . . . . . . 8 $/\$ $/\$ $/\$
115	114, 16	syl6ss 3356	. . . . . . 7 $/\$ $/\$ $/\$
116		df-ss 3330	. . . . . . 7
117	115, 116	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
118	117, 114	eqsstrd 3378	. . . . 5 $/\$ $/\$ $/\$
119		simpl1 984	. . . . . . . . . . 11 $/\$ $/\$ $/\$
120		flcl 11629	. . . . . . . . . . . . . 14
121	120	adantl 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122	121	peano2zd 10738	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123		ifcl 3819	. . . . . . . . . . . 12 $/\$
124	122, 119, 123	syl2anc 654	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	119	zred 10735	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	122	zred 10735	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
127		max1 11145	. . . . . . . . . . . 12 $/\$
128	125, 126, 127	syl2anc 654	. . . . . . . . . . 11 $/\$ $/\$ $/\$
129		eluz2 10855	. . . . . . . . . . 11 $/\$ $/\$
130	119, 124, 128, 129	syl3anbrc 1165	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	130, 9	syl6eleqr 2524	. . . . . . . . 9 $/\$ $/\$ $/\$
132		fdm 5551	. . . . . . . . . 10
133	15, 132	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
134	131, 133	eleqtrrd 2510	. . . . . . . 8 $/\$ $/\$ $/\$
135	124	zred 10735	. . . . . . . . 9 $/\$ $/\$ $/\$
136		fllep1 11635	. . . . . . . . . . 11
137	136	adantl 463	. . . . . . . . . 10 $/\$ $/\$ $/\$
138		max2 11147	. . . . . . . . . . 11 $/\$
139	125, 126, 138	syl2anc 654	. . . . . . . . . 10 $/\$ $/\$ $/\$
140	33, 126, 135, 137, 139	letrd 9516	. . . . . . . . 9 $/\$ $/\$ $/\$
141		elicopnf 11373	. . . . . . . . . 10 $/\$
142	141	adantl 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
143	135, 140, 142	mpbir2and 906	. . . . . . . 8 $/\$ $/\$ $/\$
144		inelcm 3721	. . . . . . . 8 $/\$
145	134, 143, 144	syl2anc 654	. . . . . . 7 $/\$ $/\$ $/\$
146		imadisj 5176	. . . . . . . 8
147	146	necon3bii 2630	. . . . . . 7
148	145, 147	sylibr 212	. . . . . 6 $/\$ $/\$ $/\$
149	117, 148	eqnetrd 2616	. . . . 5 $/\$ $/\$ $/\$
150		supxrre1 11281	. . . . 5 $/\$
151	118, 149, 150	syl2anc 654	. . . 4 $/\$ $/\$ $/\$
152	110, 151	mpbird 232	. . 3 $/\$ $/\$ $/\$
153	7, 152	eqeltrd 2507	. 2 $/\$ $/\$ $/\$
154	3, 5, 153	fmpt2d 5860	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1362

wcel 1755

wne 2596

wral 2705

wrex 2706

cvv 2962

cin 3315

wss 3316

c0 3625

cif 3779 class class class wbr 4280

cmpt 4338

cdm 4827

crn 4828

cima 4830

wf 5402

cfv 5406 (class class class)co 6080

cfn 7298

csup 7678

cr 9269

c1 9271

caddc 9273

cpnf 9403

cxr 9405

clt 9406

cle 9407

cz 10634

cuz 10849

cico 11290

cfz 11424

cfl 11624

clsp 12932

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-om 6466 df-1st 6566 df-2nd 6567 df-recs 6818 df-rdg 6852 df-1o 6908 df-oadd 6912 df-er 7089 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-sup 7679 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-nn 10311 df-n0 10568 df-z 10635 df-uz 10850 df-ico 11294 df-fz 11425 df-fl 11626 df-limsup 12933

This theorem is referenced by: mbflimsup 20986

W3C validator