limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 13076

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 11228	. . . 4
2	1	supex 7823	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 13071	. . . 4
7	6	adantl 466	. . 3 $/\$ $/\$ $/\$
8		simpl3 993	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 10990	. . . . . . . . . . 11
11	9, 10	eqsstri 3493	. . . . . . . . . 10
12		zssre 10763	. . . . . . . . . 10
13	11, 12	sstri 3472	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 992	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9537	. . . . . . . . 9
17		fss 5674	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11202	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 13074	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1219	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 11910	. . . . . . . 8
25	15	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11565	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2553	. . . . . . . . . 10
28		ffvelrn 5949	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2829	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10389	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 13070	. . . . . . . . . 10
36	35	ffvelrni 5950	. . . . . . . . 9
37	34, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 755	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3461	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 755	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 5950	. . . . . . . . . 10
43	41, 42	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		ifcl 3938	. . . . . . . . 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 3463	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		xrleid 11237	. . . . . . . . . . . . . . . . 17
51	43, 50	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	18	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	4	limsupgle 13072	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
54	48, 52, 41, 43, 53	syl211anc 1225	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	r19.21bi 2918	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	47, 42	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		xrmax1 11257	. . . . . . . . . . . . . . . 16 $/\$
61	58, 59, 60	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	52	ffvelrnda 5951	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	45	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		xrletr 11242	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
65	62, 58, 63, 64	syl3anc 1219	. . . . . . . . . . . . . . 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 2552	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	41	flcld 11764	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		elfz5 11561	. . . . . . . . . . . . . . . . 17 $/\$
74	70, 72, 73	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	11, 69	sseldi 3461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		flge 11771	. . . . . . . . . . . . . . . . 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 5798	. . . . . . . . . . . . . . . 16
83	82	breq1d 4409	. . . . . . . . . . . . . . 15
84	83	rspcv 3173	. . . . . . . . . . . . . 14
85	79, 81, 84	sylc 60	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		xrmax2 11258	. . . . . . . . . . . . . . . . 17 $/\$
87	43, 39, 86	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		xrletr 11242	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	62, 59, 63, 89	syl3anc 1219	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	88, 90	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	91	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	85, 92	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	47, 49, 68, 93	lecasei 9590	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	a1d 25	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	ralrimiva 2829	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	4	limsupgle 13072	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	48, 52, 34, 45, 97	syl211anc 1225	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		ltpnf 11212	. . . . . . . . . 10
101	38, 100	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simplrr 760	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		breq1 4402	. . . . . . . . . 10
104		breq1 4402	. . . . . . . . . 10
105	103, 104	ifboth 3932	. . . . . . . . 9 $/\$
106	101, 102, 105	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	37, 45, 46, 99, 106	xrlelttrd 11244	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108	32, 107	rexlimddv 2949	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	23, 108	rexlimddv 2949	. . . . 5 $/\$ $/\$ $/\$
110	7, 109	eqbrtrrd 4421	. . . 4 $/\$ $/\$ $/\$
111		imassrn 5287	. . . . . . . . 9
112		frn 5672	. . . . . . . . . 10
113	15, 112	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
114	111, 113	syl5ss 3474	. . . . . . . 8 $/\$ $/\$ $/\$
115	114, 16	syl6ss 3475	. . . . . . 7 $/\$ $/\$ $/\$
116		df-ss 3449	. . . . . . 7
117	115, 116	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
118	117, 114	eqsstrd 3497	. . . . 5 $/\$ $/\$ $/\$
119		simpl1 991	. . . . . . . . . . 11 $/\$ $/\$ $/\$
120		flcl 11761	. . . . . . . . . . . . . 14
121	120	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122	121	peano2zd 10860	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123		ifcl 3938	. . . . . . . . . . . 12 $/\$
124	122, 119, 123	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	119	zred 10857	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	122	zred 10857	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
127		max1 11267	. . . . . . . . . . . 12 $/\$
128	125, 126, 127	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
129		eluz2 10977	. . . . . . . . . . 11 $/\$ $/\$
130	119, 124, 128, 129	syl3anbrc 1172	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	130, 9	syl6eleqr 2553	. . . . . . . . 9 $/\$ $/\$ $/\$
132		fdm 5670	. . . . . . . . . 10
133	15, 132	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
134	131, 133	eleqtrrd 2545	. . . . . . . 8 $/\$ $/\$ $/\$
135	124	zred 10857	. . . . . . . . 9 $/\$ $/\$ $/\$
136		fllep1 11767	. . . . . . . . . . 11
137	136	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
138		max2 11269	. . . . . . . . . . 11 $/\$
139	125, 126, 138	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
140	33, 126, 135, 137, 139	letrd 9638	. . . . . . . . 9 $/\$ $/\$ $/\$
141		elicopnf 11501	. . . . . . . . . 10 $/\$
142	141	adantl 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
143	135, 140, 142	mpbir2and 913	. . . . . . . 8 $/\$ $/\$ $/\$
144		inelcm 3840	. . . . . . . 8 $/\$
145	134, 143, 144	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
146		imadisj 5295	. . . . . . . 8
147	146	necon3bii 2719	. . . . . . 7
148	145, 147	sylibr 212	. . . . . 6 $/\$ $/\$ $/\$
149	117, 148	eqnetrd 2744	. . . . 5 $/\$ $/\$ $/\$
150		supxrre1 11403	. . . . 5 $/\$
151	118, 149, 150	syl2anc 661	. . . 4 $/\$ $/\$ $/\$
152	110, 151	mpbird 232	. . 3 $/\$ $/\$ $/\$
153	7, 152	eqeltrd 2542	. 2 $/\$ $/\$ $/\$
154	3, 5, 153	fmpt2d 5981	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1370

wcel 1758

wne 2647

wral 2798

wrex 2799

cvv 3076

cin 3434

wss 3435

c0 3744

cif 3898 class class class wbr 4399

cmpt 4457

cdm 4947

crn 4948

cima 4950

wf 5521

cfv 5525 (class class class)co 6199

cfn 7419

csup 7800

cr 9391

c1 9393

caddc 9395

cpnf 9525

cxr 9527

clt 9528

cle 9529

cz 10756

cuz 10971

cico 11412

cfz 11553

cfl 11756

clsp 13065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469 ax-pre-sup 9470

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rmo 2806 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-int 4236 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-1st 6686 df-2nd 6687 df-recs 6941 df-rdg 6975 df-1o 7029 df-oadd 7033 df-er 7210 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-sup 7801 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-nn 10433 df-n0 10690 df-z 10757 df-uz 10972 df-ico 11416 df-fz 11554 df-fl 11758 df-limsup 13066

This theorem is referenced by: mbflimsup 21276

W3C validator