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 13543

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 13542 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 11440	. . . 4
2	1	supex 7977	. . 3
3	2	a1i 11	. 2 $/\$ $/\$ $/\$
4		limsupval.1	. . 3
5	4	a1i 11	. 2 $/\$ $/\$
6	4	limsupgval 13534	. . . 4
7	6	adantl 468	. . 3 $/\$ $/\$ $/\$
8		simpl3 1013	. . . . . . 7 $/\$ $/\$ $/\$
9		limsupgre.z	. . . . . . . . . . 11
10		uzssz 11178	. . . . . . . . . . 11
11	9, 10	eqsstri 3462	. . . . . . . . . 10
12		zssre 10944	. . . . . . . . . 10
13	11, 12	sstri 3441	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
15		simpl2 1012	. . . . . . . . 9 $/\$ $/\$ $/\$
16		ressxr 9684	. . . . . . . . 9
17		fss 5737	. . . . . . . . 9 $/\$
18	15, 16, 17	sylancl 668	. . . . . . . 8 $/\$ $/\$ $/\$
19		pnfxr 11412	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
21	4	limsupltOLD 13539	. . . . . . . 8 $/\$ $/\$
22	14, 18, 20, 21	syl3anc 1268	. . . . . . 7 $/\$ $/\$ $/\$
23	8, 22	mpbid 214	. . . . . 6 $/\$ $/\$ $/\$
24		fzfi 12185	. . . . . . . 8
25	15	adantr 467	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		elfzuz 11796	. . . . . . . . . . 11
27	26, 9	syl6eleqr 2540	. . . . . . . . . 10
28		ffvelrn 6020	. . . . . . . . . 10 $/\$
29	25, 27, 28	syl2an 480	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	29	ralrimiva 2802	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
31		fimaxre3 10553	. . . . . . . 8 $/\$
32	24, 30, 31	sylancr 669	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 463	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	ad2antrr 732	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	4	limsupgf 13533	. . . . . . . . . 10
36	35	ffvelrni 6021	. . . . . . . . 9
37	34, 36	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simprl 764	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	16, 38	sseldi 3430	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		simprl 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	adantr 467	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	35	ffvelrni 6021	. . . . . . . . . 10
43	41, 42	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	39, 43	ifcld 3924	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	19	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	40	ad2antrr 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	13	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	47	sselda 3432	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		xrleid 11449	. . . . . . . . . . . . . . . . 17
50	43, 49	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	18	ad2antrr 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	4	limsupgle 13535	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
53	47, 51, 41, 43, 52	syl211anc 1274	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	50, 53	mpbid 214	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	r19.21bi 2757	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55	imp 431	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	46, 42	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	39	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		xrmax1 11470	. . . . . . . . . . . . . . . 16 $/\$
60	57, 58, 59	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	51	ffvelrnda 6022	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	44	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		xrletr 11455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
64	61, 57, 62, 63	syl3anc 1268	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	60, 64	mpan2d 680	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	65	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	56, 66	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		simpr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68, 9	syl6eleq 2539	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	41	flcld 12034	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72		elfz5 11792	. . . . . . . . . . . . . . . . 17 $/\$
73	69, 71, 72	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 68	sseldi 3430	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		flge 12041	. . . . . . . . . . . . . . . . 17 $/\$
76	46, 74, 75	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	73, 76	bitr4d 260	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	biimpar 488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79		simprr 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ad2antrr 732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		fveq2 5865	. . . . . . . . . . . . . . . 16
82	81	breq1d 4412	. . . . . . . . . . . . . . 15
83	82	rspcv 3146	. . . . . . . . . . . . . 14
84	78, 80, 83	sylc 62	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		xrmax2 11471	. . . . . . . . . . . . . . . . 17 $/\$
86	43, 39, 85	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	86	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		xrletr 11455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
89	61, 58, 62, 88	syl3anc 1268	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	87, 89	mpan2d 680	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	90	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	84, 91	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	46, 48, 67, 92	lecasei 9740	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	93	a1d 26	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	ralrimiva 2802	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	4	limsupgle 13535	. . . . . . . . . 10 $/\$ $/\$ $/\$
97	47, 51, 34, 44, 96	syl211anc 1274	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	mpbird 236	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		ltpnf 11422	. . . . . . . . . 10
100	38, 99	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		simplrr 771	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		breq1 4405	. . . . . . . . . 10
103		breq1 4405	. . . . . . . . . 10
104	102, 103	ifboth 3917	. . . . . . . . 9 $/\$
105	100, 101, 104	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	37, 44, 45, 98, 105	xrlelttrd 11457	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	32, 106	rexlimddv 2883	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
108	23, 107	rexlimddv 2883	. . . . 5 $/\$ $/\$ $/\$
109	7, 108	eqbrtrrd 4425	. . . 4 $/\$ $/\$ $/\$
110		imassrn 5179	. . . . . . . . 9
111		frn 5735	. . . . . . . . . 10
112	15, 111	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
113	110, 112	syl5ss 3443	. . . . . . . 8 $/\$ $/\$ $/\$
114	113, 16	syl6ss 3444	. . . . . . 7 $/\$ $/\$ $/\$
115		df-ss 3418	. . . . . . 7
116	114, 115	sylib 200	. . . . . 6 $/\$ $/\$ $/\$
117	116, 113	eqsstrd 3466	. . . . 5 $/\$ $/\$ $/\$
118		simpl1 1011	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119		flcl 12031	. . . . . . . . . . . . . 14
120	119	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	120	peano2zd 11043	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
122	121, 118	ifcld 3924	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	118	zred 11040	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
124	121	zred 11040	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
125		max1 11480	. . . . . . . . . . . 12 $/\$
126	123, 124, 125	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
127		eluz2 11165	. . . . . . . . . . 11 $/\$ $/\$
128	118, 122, 126, 127	syl3anbrc 1192	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	128, 9	syl6eleqr 2540	. . . . . . . . 9 $/\$ $/\$ $/\$
130		fdm 5733	. . . . . . . . . 10
131	15, 130	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
132	129, 131	eleqtrrd 2532	. . . . . . . 8 $/\$ $/\$ $/\$
133	122	zred 11040	. . . . . . . . 9 $/\$ $/\$ $/\$
134		fllep1 12037	. . . . . . . . . . 11
135	134	adantl 468	. . . . . . . . . 10 $/\$ $/\$ $/\$
136		max2 11482	. . . . . . . . . . 11 $/\$
137	123, 124, 136	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$
138	33, 124, 133, 135, 137	letrd 9792	. . . . . . . . 9 $/\$ $/\$ $/\$
139		elicopnf 11730	. . . . . . . . . 10 $/\$
140	139	adantl 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
141	133, 138, 140	mpbir2and 933	. . . . . . . 8 $/\$ $/\$ $/\$
142		inelcm 3819	. . . . . . . 8 $/\$
143	132, 141, 142	syl2anc 667	. . . . . . 7 $/\$ $/\$ $/\$
144		imadisj 5187	. . . . . . . 8
145	144	necon3bii 2676	. . . . . . 7
146	143, 145	sylibr 216	. . . . . 6 $/\$ $/\$ $/\$
147	116, 146	eqnetrd 2691	. . . . 5 $/\$ $/\$ $/\$
148		supxrre1 11616	. . . . 5 $/\$
149	117, 147, 148	syl2anc 667	. . . 4 $/\$ $/\$ $/\$
150	109, 149	mpbird 236	. . 3 $/\$ $/\$ $/\$
151	7, 150	eqeltrd 2529	. 2 $/\$ $/\$ $/\$
152	3, 5, 151	fmpt2d 6053	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1444

wcel 1887

wne 2622

wral 2737

wrex 2738

cvv 3045

cin 3403

wss 3404

c0 3731

cif 3881 class class class wbr 4402

cmpt 4461

cdm 4834

crn 4835

cima 4837

wf 5578

cfv 5582 (class class class)co 6290

cfn 7569

csup 7954

cr 9538

c1 9540

caddc 9542

cpnf 9672

cxr 9674

clt 9675

cle 9676

cz 10937

cuz 11159

cico 11637

cfz 11784

cfl 12026

clspold 13525

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-inf 7957 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-n0 10870 df-z 10938 df-uz 11160 df-ico 11641 df-fz 11785 df-fl 12028 df-limsupOLD 13527

This theorem is referenced by: mbflimsupOLD 22624

W3C validator