limsupgre - Metamath Proof Explorer

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

Theorem limsupgre 13315

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 11372	. . . 4
2	1	supex 7940	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 13310	. . . 4
7	6	adantl 466	. . 3 $/\$ $/\$ $/\$
8		simpl3 1001	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 11125	. . . . . . . . . . 11
11	9, 10	eqsstri 3529	. . . . . . . . . 10
12		zssre 10892	. . . . . . . . . 10
13	11, 12	sstri 3508	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 1000	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9654	. . . . . . . . 9
17		fss 5745	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11346	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsuplt 13313	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 12084	. . . . . . . 8
25	15	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11709	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2556	. . . . . . . . . 10
28		ffvelrn 6030	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2871	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10512	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 13309	. . . . . . . . . 10
36	35	ffvelrni 6031	. . . . . . . . 9
37	34, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 756	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3497	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 756	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 6031	. . . . . . . . . 10
43	41, 42	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	39, 43	ifcld 3987	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	40	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	47	sselda 3499	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		xrleid 11381	. . . . . . . . . . . . . . . . 17
50	43, 49	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	18	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	4	limsupgle 13311	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
53	47, 51, 41, 43, 52	syl211anc 1234	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	50, 53	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	r19.21bi 2826	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	46, 42	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	39	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		xrmax1 11401	. . . . . . . . . . . . . . . 16 $/\$
60	57, 58, 59	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	51	ffvelrnda 6032	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	44	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		xrletr 11386	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
64	61, 57, 62, 63	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	60, 64	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	65	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	56, 66	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68, 9	syl6eleq 2555	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	41	flcld 11937	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		elfz5 11705	. . . . . . . . . . . . . . . . 17 $/\$
73	69, 71, 72	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 68	sseldi 3497	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		flge 11944	. . . . . . . . . . . . . . . . 17 $/\$
76	46, 74, 75	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	73, 76	bitr4d 256	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	biimpar 485	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprr 757	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		fveq2 5872	. . . . . . . . . . . . . . . 16
82	81	breq1d 4466	. . . . . . . . . . . . . . 15
83	82	rspcv 3206	. . . . . . . . . . . . . 14
84	78, 80, 83	sylc 60	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		xrmax2 11402	. . . . . . . . . . . . . . . . 17 $/\$
86	43, 39, 85	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		xrletr 11386	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
89	61, 58, 62, 88	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 89	mpan2d 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	90	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	84, 91	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	46, 48, 67, 92	lecasei 9707	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	93	a1d 25	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	ralrimiva 2871	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	4	limsupgle 13311	. . . . . . . . . 10 $/\$ $/\$ $/\$
97	47, 51, 34, 44, 96	syl211anc 1234	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		ltpnf 11356	. . . . . . . . . 10
100	38, 99	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		simplrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		breq1 4459	. . . . . . . . . 10
103		breq1 4459	. . . . . . . . . 10
104	102, 103	ifboth 3980	. . . . . . . . 9 $/\$
105	100, 101, 104	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	37, 44, 45, 98, 105	xrlelttrd 11388	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	32, 106	rexlimddv 2953	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
108	23, 107	rexlimddv 2953	. . . . 5 $/\$ $/\$ $/\$
109	7, 108	eqbrtrrd 4478	. . . 4 $/\$ $/\$ $/\$
110		imassrn 5358	. . . . . . . . 9
111		frn 5743	. . . . . . . . . 10
112	15, 111	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
113	110, 112	syl5ss 3510	. . . . . . . 8 $/\$ $/\$ $/\$
114	113, 16	syl6ss 3511	. . . . . . 7 $/\$ $/\$ $/\$
115		df-ss 3485	. . . . . . 7
116	114, 115	sylib 196	. . . . . 6 $/\$ $/\$ $/\$
117	116, 113	eqsstrd 3533	. . . . 5 $/\$ $/\$ $/\$
118		simpl1 999	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119		flcl 11934	. . . . . . . . . . . . . 14
120	119	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	120	peano2zd 10993	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
122	121, 118	ifcld 3987	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	118	zred 10990	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124	121	zred 10990	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125		max1 11411	. . . . . . . . . . . 12 $/\$
126	123, 124, 125	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
127		eluz2 11112	. . . . . . . . . . 11 $/\$ $/\$
128	118, 122, 126, 127	syl3anbrc 1180	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	128, 9	syl6eleqr 2556	. . . . . . . . 9 $/\$ $/\$ $/\$
130		fdm 5741	. . . . . . . . . 10
131	15, 130	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
132	129, 131	eleqtrrd 2548	. . . . . . . 8 $/\$ $/\$ $/\$
133	122	zred 10990	. . . . . . . . 9 $/\$ $/\$ $/\$
134		fllep1 11940	. . . . . . . . . . 11
135	134	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$
136		max2 11413	. . . . . . . . . . 11 $/\$
137	123, 124, 136	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
138	33, 124, 133, 135, 137	letrd 9756	. . . . . . . . 9 $/\$ $/\$ $/\$
139		elicopnf 11645	. . . . . . . . . 10 $/\$
140	139	adantl 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
141	133, 138, 140	mpbir2and 922	. . . . . . . 8 $/\$ $/\$ $/\$
142		inelcm 3884	. . . . . . . 8 $/\$
143	132, 141, 142	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$
144		imadisj 5366	. . . . . . . 8
145	144	necon3bii 2725	. . . . . . 7
146	143, 145	sylibr 212	. . . . . 6 $/\$ $/\$ $/\$
147	116, 146	eqnetrd 2750	. . . . 5 $/\$ $/\$ $/\$
148		supxrre1 11547	. . . . 5 $/\$
149	117, 147, 148	syl2anc 661	. . . 4 $/\$ $/\$ $/\$
150	109, 149	mpbird 232	. . 3 $/\$ $/\$ $/\$
151	7, 150	eqeltrd 2545	. 2 $/\$ $/\$ $/\$
152	3, 5, 151	fmpt2d 6062	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1395

wcel 1819

wne 2652

wral 2807

wrex 2808

cvv 3109

cin 3470

wss 3471

c0 3793

cif 3944 class class class wbr 4456

cmpt 4515

cdm 5008

crn 5009

cima 5011

wf 5590

cfv 5594 (class class class)co 6296

cfn 7535

csup 7918

cr 9508

c1 9510

caddc 9512

cpnf 9642

cxr 9644

clt 9645

cle 9646

cz 10885

cuz 11106

cico 11556

cfz 11697

cfl 11929

clsp 13304

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-n0 10817 df-z 10886 df-uz 11107 df-ico 11560 df-fz 11698 df-fl 11931 df-limsup 13305

This theorem is referenced by: mbflimsup 22198

W3C validator