limsupgreOLD - Metamath Proof Explorer

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

Theorem limsupgreOLD 13620

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.) Obsolete version of limsupgre 13619 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)

**Hypotheses**
Ref	Expression
limsupval.1
limsupgre.z

**Assertion**
Ref	Expression
limsupgreOLD	$/\$ $/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem limsupgreOLD Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrltso 11463	. . . 4
2	1	supex 7995	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 13611	. . . 4
7	6	adantl 473	. . 3 $/\$ $/\$ $/\$
8		simpl3 1035	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 11202	. . . . . . . . . . 11
11	9, 10	eqsstri 3448	. . . . . . . . . 10
12		zssre 10968	. . . . . . . . . 10
13	11, 12	sstri 3427	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 1034	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9702	. . . . . . . . 9
17		fss 5749	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 675	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11435	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsupltOLD 13616	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1292	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 215	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 12223	. . . . . . . 8
25	15	adantr 472	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11822	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2560	. . . . . . . . . 10
28		ffvelrn 6035	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 485	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2809	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10575	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 676	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 740	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 13610	. . . . . . . . . 10
36	35	ffvelrni 6036	. . . . . . . . 9
37	34, 36	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 772	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3416	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 772	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 472	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 6036	. . . . . . . . . 10
43	41, 42	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	39, 43	ifcld 3915	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	40	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	47	sselda 3418	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		xrleid 11472	. . . . . . . . . . . . . . . . 17
50	43, 49	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	18	ad2antrr 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	4	limsupgle 13612	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
53	47, 51, 41, 43, 52	syl211anc 1298	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	50, 53	mpbid 215	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	r19.21bi 2776	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	imp 436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	46, 42	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	39	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		xrmax1 11493	. . . . . . . . . . . . . . . 16 $/\$
60	57, 58, 59	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	51	ffvelrnda 6037	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	44	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		xrletr 11478	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
64	61, 57, 62, 63	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	60, 64	mpan2d 688	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	65	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	56, 66	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simpr 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68, 9	syl6eleq 2559	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	41	flcld 12067	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		elfz5 11818	. . . . . . . . . . . . . . . . 17 $/\$
73	69, 71, 72	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 68	sseldi 3416	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		flge 12074	. . . . . . . . . . . . . . . . 17 $/\$
76	46, 74, 75	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	73, 76	bitr4d 264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	biimpar 493	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprr 774	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		fveq2 5879	. . . . . . . . . . . . . . . 16
82	81	breq1d 4405	. . . . . . . . . . . . . . 15
83	82	rspcv 3132	. . . . . . . . . . . . . 14
84	78, 80, 83	sylc 61	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		xrmax2 11494	. . . . . . . . . . . . . . . . 17 $/\$
86	43, 39, 85	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		xrletr 11478	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
89	61, 58, 62, 88	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 89	mpan2d 688	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	90	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	84, 91	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	46, 48, 67, 92	lecasei 9758	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	93	a1d 25	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	ralrimiva 2809	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	4	limsupgle 13612	. . . . . . . . . 10 $/\$ $/\$ $/\$
97	47, 51, 34, 44, 96	syl211anc 1298	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	mpbird 240	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		ltpnf 11445	. . . . . . . . . 10
100	38, 99	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		simplrr 779	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		breq1 4398	. . . . . . . . . 10
103		breq1 4398	. . . . . . . . . 10
104	102, 103	ifboth 3908	. . . . . . . . 9 $/\$
105	100, 101, 104	syl2anc 673	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	37, 44, 45, 98, 105	xrlelttrd 11480	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	32, 106	rexlimddv 2875	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
108	23, 107	rexlimddv 2875	. . . . 5 $/\$ $/\$ $/\$
109	7, 108	eqbrtrrd 4418	. . . 4 $/\$ $/\$ $/\$
110		imassrn 5185	. . . . . . . . 9
111		frn 5747	. . . . . . . . . 10
112	15, 111	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
113	110, 112	syl5ss 3429	. . . . . . . 8 $/\$ $/\$ $/\$
114	113, 16	syl6ss 3430	. . . . . . 7 $/\$ $/\$ $/\$
115		df-ss 3404	. . . . . . 7
116	114, 115	sylib 201	. . . . . 6 $/\$ $/\$ $/\$
117	116, 113	eqsstrd 3452	. . . . 5 $/\$ $/\$ $/\$
118		simpl1 1033	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119		flcl 12064	. . . . . . . . . . . . . 14
120	119	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	120	peano2zd 11066	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
122	121, 118	ifcld 3915	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	118	zred 11063	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124	121	zred 11063	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125		max1 11503	. . . . . . . . . . . 12 $/\$
126	123, 124, 125	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$
127		eluz2 11188	. . . . . . . . . . 11 $/\$ $/\$
128	118, 122, 126, 127	syl3anbrc 1214	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	128, 9	syl6eleqr 2560	. . . . . . . . 9 $/\$ $/\$ $/\$
130		fdm 5745	. . . . . . . . . 10
131	15, 130	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
132	129, 131	eleqtrrd 2552	. . . . . . . 8 $/\$ $/\$ $/\$
133	122	zred 11063	. . . . . . . . 9 $/\$ $/\$ $/\$
134		fllep1 12070	. . . . . . . . . . 11
135	134	adantl 473	. . . . . . . . . 10 $/\$ $/\$ $/\$
136		max2 11505	. . . . . . . . . . 11 $/\$
137	123, 124, 136	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$
138	33, 124, 133, 135, 137	letrd 9809	. . . . . . . . 9 $/\$ $/\$ $/\$
139		elicopnf 11755	. . . . . . . . . 10 $/\$
140	139	adantl 473	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
141	133, 138, 140	mpbir2and 936	. . . . . . . 8 $/\$ $/\$ $/\$
142		inelcm 3823	. . . . . . . 8 $/\$
143	132, 141, 142	syl2anc 673	. . . . . . 7 $/\$ $/\$ $/\$
144		imadisj 5193	. . . . . . . 8
145	144	necon3bii 2695	. . . . . . 7
146	143, 145	sylibr 217	. . . . . 6 $/\$ $/\$ $/\$
147	116, 146	eqnetrd 2710	. . . . 5 $/\$ $/\$ $/\$
148		supxrre1 11641	. . . . 5 $/\$
149	117, 147, 148	syl2anc 673	. . . 4 $/\$ $/\$ $/\$
150	109, 149	mpbird 240	. . 3 $/\$ $/\$ $/\$
151	7, 150	eqeltrd 2549	. 2 $/\$ $/\$ $/\$
152	3, 5, 151	fmpt2d 6069	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031

cin 3389

wss 3390

c0 3722

cif 3872 class class class wbr 4395

cmpt 4454

cdm 4839

crn 4840

cima 4842

wf 5585

cfv 5589 (class class class)co 6308

cfn 7587

csup 7972

cr 9556

c1 9558

caddc 9560

cpnf 9690

cxr 9692

clt 9693

cle 9694

cz 10961

cuz 11182

cico 11662

cfz 11810

cfl 12059

clspold 13602

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-inf 7975 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-n0 10894 df-z 10962 df-uz 11183 df-ico 11666 df-fz 11811 df-fl 12061 df-limsupOLD 13604

This theorem is referenced by: mbflimsupOLD 22703

W3C validator