limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 13535

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 11437	. . . 4
2	1	supex 7974	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 13527	. . . 4
7	6	adantl 468	. . 3 $/\$ $/\$ $/\$
8		simpl3 1012	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 11175	. . . . . . . . . . 11
11	9, 10	eqsstri 3461	. . . . . . . . . 10
12		zssre 10941	. . . . . . . . . 10
13	11, 12	sstri 3440	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 1011	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9681	. . . . . . . . 9
17		fss 5735	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 667	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11409	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 13531	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1267	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 214	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 12182	. . . . . . . 8
25	15	adantr 467	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11793	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2539	. . . . . . . . . 10
28		ffvelrn 6018	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 480	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2801	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10550	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 668	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 463	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 731	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 13526	. . . . . . . . . 10
36	35	ffvelrni 6019	. . . . . . . . 9
37	34, 36	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 763	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3429	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 763	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 467	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 6019	. . . . . . . . . 10
43	41, 42	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	39, 43	ifcld 3923	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	40	ad2antrr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	47	sselda 3431	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		xrleid 11446	. . . . . . . . . . . . . . . . 17
50	43, 49	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	18	ad2antrr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	4	limsupgle 13528	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
53	47, 51, 41, 43, 52	syl211anc 1273	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	50, 53	mpbid 214	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	r19.21bi 2756	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	imp 431	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	46, 42	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	39	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		xrmax1 11467	. . . . . . . . . . . . . . . 16 $/\$
60	57, 58, 59	syl2anc 666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	51	ffvelrnda 6020	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	44	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		xrletr 11452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
64	61, 57, 62, 63	syl3anc 1267	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	60, 64	mpan2d 679	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	65	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	56, 66	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simpr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68, 9	syl6eleq 2538	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	41	flcld 12031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		elfz5 11789	. . . . . . . . . . . . . . . . 17 $/\$
73	69, 71, 72	syl2anc 666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 68	sseldi 3429	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		flge 12038	. . . . . . . . . . . . . . . . 17 $/\$
76	46, 74, 75	syl2anc 666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	73, 76	bitr4d 260	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	biimpar 488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprr 765	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		fveq2 5863	. . . . . . . . . . . . . . . 16
82	81	breq1d 4411	. . . . . . . . . . . . . . 15
83	82	rspcv 3145	. . . . . . . . . . . . . 14
84	78, 80, 83	sylc 62	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		xrmax2 11468	. . . . . . . . . . . . . . . . 17 $/\$
86	43, 39, 85	syl2anc 666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		xrletr 11452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
89	61, 58, 62, 88	syl3anc 1267	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 89	mpan2d 679	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	90	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	84, 91	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	46, 48, 67, 92	lecasei 9737	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	93	a1d 26	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	ralrimiva 2801	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	4	limsupgle 13528	. . . . . . . . . 10 $/\$ $/\$ $/\$
97	47, 51, 34, 44, 96	syl211anc 1273	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	mpbird 236	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	38	ltpnfd 11420	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		simplrr 770	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		breq1 4404	. . . . . . . . . 10
102		breq1 4404	. . . . . . . . . 10
103	101, 102	ifboth 3916	. . . . . . . . 9 $/\$
104	99, 100, 103	syl2anc 666	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	37, 44, 45, 98, 104	xrlelttrd 11454	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	32, 105	rexlimddv 2882	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
107	23, 106	rexlimddv 2882	. . . . 5 $/\$ $/\$ $/\$
108	7, 107	eqbrtrrd 4424	. . . 4 $/\$ $/\$ $/\$
109		imassrn 5178	. . . . . . . . 9
110		frn 5733	. . . . . . . . . 10
111	15, 110	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
112	109, 111	syl5ss 3442	. . . . . . . 8 $/\$ $/\$ $/\$
113	112, 16	syl6ss 3443	. . . . . . 7 $/\$ $/\$ $/\$
114		df-ss 3417	. . . . . . 7
115	113, 114	sylib 200	. . . . . 6 $/\$ $/\$ $/\$
116	115, 112	eqsstrd 3465	. . . . 5 $/\$ $/\$ $/\$
117		simpl1 1010	. . . . . . . . . . 11 $/\$ $/\$ $/\$
118		flcl 12028	. . . . . . . . . . . . . 14
119	118	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	peano2zd 11040	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	120, 117	ifcld 3923	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122	117	zred 11037	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123	120	zred 11037	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124		max1 11477	. . . . . . . . . . . 12 $/\$
125	122, 123, 124	syl2anc 666	. . . . . . . . . . 11 $/\$ $/\$ $/\$
126		eluz2 11162	. . . . . . . . . . 11 $/\$ $/\$
127	117, 121, 125, 126	syl3anbrc 1191	. . . . . . . . . 10 $/\$ $/\$ $/\$
128	127, 9	syl6eleqr 2539	. . . . . . . . 9 $/\$ $/\$ $/\$
129		fdm 5731	. . . . . . . . . 10
130	15, 129	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
131	128, 130	eleqtrrd 2531	. . . . . . . 8 $/\$ $/\$ $/\$
132	121	zred 11037	. . . . . . . . 9 $/\$ $/\$ $/\$
133		fllep1 12034	. . . . . . . . . . 11
134	133	adantl 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
135		max2 11479	. . . . . . . . . . 11 $/\$
136	122, 123, 135	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$ $/\$
137	33, 123, 132, 134, 136	letrd 9789	. . . . . . . . 9 $/\$ $/\$ $/\$
138		elicopnf 11727	. . . . . . . . . 10 $/\$
139	138	adantl 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
140	132, 137, 139	mpbir2and 932	. . . . . . . 8 $/\$ $/\$ $/\$
141		inelcm 3818	. . . . . . . 8 $/\$
142	131, 140, 141	syl2anc 666	. . . . . . 7 $/\$ $/\$ $/\$
143		imadisj 5186	. . . . . . . 8
144	143	necon3bii 2675	. . . . . . 7
145	142, 144	sylibr 216	. . . . . 6 $/\$ $/\$ $/\$
146	115, 145	eqnetrd 2690	. . . . 5 $/\$ $/\$ $/\$
147		supxrre1 11613	. . . . 5 $/\$
148	116, 146, 147	syl2anc 666	. . . 4 $/\$ $/\$ $/\$
149	108, 148	mpbird 236	. . 3 $/\$ $/\$ $/\$
150	7, 149	eqeltrd 2528	. 2 $/\$ $/\$ $/\$
151	3, 5, 150	fmpt2d 6051	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wne 2621

wral 2736

wrex 2737

cvv 3044

cin 3402

wss 3403

c0 3730

cif 3880 class class class wbr 4401

cmpt 4460

cdm 4833

crn 4834

cima 4836

wf 5577

cfv 5581 (class class class)co 6288

cfn 7566

csup 7951

cr 9535

c1 9537

caddc 9539

cpnf 9669

cxr 9671

clt 9672

cle 9673

cz 10934

cuz 11156

cico 11634

cfz 11781

cfl 12023

clsp 13517

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-sup 7953 df-inf 7954 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-n0 10867 df-z 10935 df-uz 11157 df-ico 11638 df-fz 11782 df-fl 12025 df-limsup 13519

This theorem is referenced by: mbflimsup 22616

W3C validator