suplesup - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > suplesup		Structured version Visualization version Unicode version

Theorem suplesup 39555

Description: If any element of

can be approximated from below by members of

, then the supremum of

is smaller or equal to the supremum of

. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
suplesup.a
suplesup.b
suplesup.c

**Assertion**
Ref	Expression
suplesup

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem suplesup Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		suplesup.a	. . . . . 6
2		ressxr 10083	. . . . . 6
3	1, 2	syl6ss 3615	. . . . 5
4		supxrcl 12145	. . . . 5
5	3, 4	syl 17	. . . 4
6	5	adantr 481	. . 3 $/\$
7		eqidd 2623	. . . 4 $/\$
8		simpr 477	. . . 4 $/\$
9		peano2re 10209	. . . . . . . . . 10
10	9	adantl 482	. . . . . . . . 9 $/\$ $/\$
11	3	adantr 481	. . . . . . . . . . . 12 $/\$
12		supxrunb2 12150	. . . . . . . . . . . 12
13	11, 12	syl 17	. . . . . . . . . . 11 $/\$
14	8, 13	mpbird 247	. . . . . . . . . 10 $/\$
15	14	adantr 481	. . . . . . . . 9 $/\$ $/\$
16		breq1 4656	. . . . . . . . . . 11
17	16	rexbidv 3052	. . . . . . . . . 10
18	17	rspcva 3307	. . . . . . . . 9 $/\$
19	10, 15, 18	syl2anc 693	. . . . . . . 8 $/\$ $/\$
20		1rp 11836	. . . . . . . . . . . . . . . 16
21	20	a1i 11	. . . . . . . . . . . . . . 15 $/\$
22		suplesup.c	. . . . . . . . . . . . . . . 16
23	22	r19.21bi 2932	. . . . . . . . . . . . . . 15 $/\$
24		oveq2 6658	. . . . . . . . . . . . . . . . . 18
25	24	breq1d 4663	. . . . . . . . . . . . . . . . 17
26	25	rexbidv 3052	. . . . . . . . . . . . . . . 16
27	26	rspcva 3307	. . . . . . . . . . . . . . 15 $/\$
28	21, 23, 27	syl2anc 693	. . . . . . . . . . . . . 14 $/\$
29	28	adantlr 751	. . . . . . . . . . . . 13 $/\$ $/\$
30	29	3adant3 1081	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
31		nfv 1843	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
32		simp11r 1173	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
33	2, 32	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
34	1	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 $/\$
35		1red 10055	. . . . . . . . . . . . . . . . . . . 20 $/\$
36	34, 35	resubcld 10458	. . . . . . . . . . . . . . . . . . 19 $/\$
37	36	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
38	37	3adant3 1081	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
39	38	3ad2ant1 1082	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
40	2, 39	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
41		suplesup.b	. . . . . . . . . . . . . . . . . . 19
42	41	sselda 3603	. . . . . . . . . . . . . . . . . 18 $/\$
43	42	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
44	43	3ad2antl1 1223	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
45	44	3adant3 1081	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
46		simp3 1063	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
47		simp1r 1086	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
48		1red 10055	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
49	34	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
50	49	3adant3 1081	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
51	47, 48, 50	ltaddsubd 10627	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
52	46, 51	mpbid 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
53	52	3ad2ant1 1082	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
54		simp3 1063	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
55	33, 40, 45, 53, 54	xrlttrd 11990	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	3exp 1264	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
57	31, 56	reximdai 3012	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58	30, 57	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$
59	58	3exp 1264	. . . . . . . . . 10 $/\$
60	59	adantlr 751	. . . . . . . . 9 $/\$ $/\$
61	60	rexlimdv 3030	. . . . . . . 8 $/\$ $/\$
62	19, 61	mpd 15	. . . . . . 7 $/\$ $/\$
63	2	a1i 11	. . . . . . . . . . . . 13
64	63	sselda 3603	. . . . . . . . . . . 12 $/\$
65	64	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
66	43	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$
67		simpr 477	. . . . . . . . . . 11 $/\$ $/\$ $/\$
68	65, 66, 67	xrltled 39486	. . . . . . . . . 10 $/\$ $/\$ $/\$
69	68	ex 450	. . . . . . . . 9 $/\$ $/\$
70	69	adantllr 755	. . . . . . . 8 $/\$ $/\$ $/\$
71	70	reximdva 3017	. . . . . . 7 $/\$ $/\$
72	62, 71	mpd 15	. . . . . 6 $/\$ $/\$
73	72	ralrimiva 2966	. . . . 5 $/\$
74		supxrunb1 12149	. . . . . . 7
75	41, 74	syl 17	. . . . . 6
76	75	adantr 481	. . . . 5 $/\$
77	73, 76	mpbid 222	. . . 4 $/\$
78	7, 8, 77	3eqtr4d 2666	. . 3 $/\$
79	6, 78	xreqled 39546	. 2 $/\$
80		supeq1 8351	. . . . . . 7
81		xrsup0 12153	. . . . . . . 8
82	81	a1i 11	. . . . . . 7
83	80, 82	eqtrd 2656	. . . . . 6
84	83	adantl 482	. . . . 5 $/\$
85		supxrcl 12145	. . . . . . . 8
86	41, 85	syl 17	. . . . . . 7
87		mnfle 11969	. . . . . . 7
88	86, 87	syl 17	. . . . . 6
89	88	adantr 481	. . . . 5 $/\$
90	84, 89	eqbrtrd 4675	. . . 4 $/\$
91	90	adantlr 751	. . 3 $/\$ $/\$
92		simpll 790	. . . 4 $/\$ $/\$
93	1	adantr 481	. . . . . . . 8 $/\$
94		neqne 2802	. . . . . . . . 9
95	94	adantl 482	. . . . . . . 8 $/\$
96		supxrgtmnf 12159	. . . . . . . 8 $/\$
97	93, 95, 96	syl2anc 693	. . . . . . 7 $/\$
98	97	adantlr 751	. . . . . 6 $/\$ $/\$
99		simpr 477	. . . . . . . . 9 $/\$
100		simpl 473	. . . . . . . . . 10 $/\$
101		nltpnft 11995	. . . . . . . . . 10
102	100, 5, 101	3syl 18	. . . . . . . . 9 $/\$
103	99, 102	mtbid 314	. . . . . . . 8 $/\$
104		notnotr 125	. . . . . . . 8
105	103, 104	syl 17	. . . . . . 7 $/\$
106	105	adantr 481	. . . . . 6 $/\$ $/\$
107	98, 106	jca 554	. . . . 5 $/\$ $/\$ $/\$
108	92, 5	syl 17	. . . . . 6 $/\$ $/\$
109		xrrebnd 11999	. . . . . 6 $/\$
110	108, 109	syl 17	. . . . 5 $/\$ $/\$ $/\$
111	107, 110	mpbird 247	. . . 4 $/\$ $/\$
112		nfv 1843	. . . . 5 $/\$
113	41	adantr 481	. . . . 5 $/\$
114		simpr 477	. . . . 5 $/\$
115	114	adantr 481	. . . . . . . 8 $/\$ $/\$
116		simpr 477	. . . . . . . . 9 $/\$ $/\$
117	116	rphalfcld 11884	. . . . . . . 8 $/\$ $/\$
118	115, 117	ltsubrpd 11904	. . . . . . 7 $/\$ $/\$
119	3	ad2antrr 762	. . . . . . . 8 $/\$ $/\$
120		rpre 11839	. . . . . . . . . . . 12
121		2re 11090	. . . . . . . . . . . . 13
122	121	a1i 11	. . . . . . . . . . . 12
123		2ne0 11113	. . . . . . . . . . . . 13
124	123	a1i 11	. . . . . . . . . . . 12
125	120, 122, 124	redivcld 10853	. . . . . . . . . . 11
126	125	adantl 482	. . . . . . . . . 10 $/\$ $/\$
127	115, 126	resubcld 10458	. . . . . . . . 9 $/\$ $/\$
128	2, 127	sseldi 3601	. . . . . . . 8 $/\$ $/\$
129		supxrlub 12155	. . . . . . . 8 $/\$
130	119, 128, 129	syl2anc 693	. . . . . . 7 $/\$ $/\$
131	118, 130	mpbid 222	. . . . . 6 $/\$ $/\$
132		rphalfcl 11858	. . . . . . . . . . . 12
133	132	3ad2ant2 1083	. . . . . . . . . . 11 $/\$ $/\$
134	23	3adant2 1080	. . . . . . . . . . 11 $/\$ $/\$
135		oveq2 6658	. . . . . . . . . . . . . 14
136	135	breq1d 4663	. . . . . . . . . . . . 13
137	136	rexbidv 3052	. . . . . . . . . . . 12
138	137	rspcva 3307	. . . . . . . . . . 11 $/\$
139	133, 134, 138	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$
140	139	ad5ant134 1313	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
141		recn 10026	. . . . . . . . . . . . . . . . . 18
142	141	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
143	120	recnd 10068	. . . . . . . . . . . . . . . . . . 19
144	143	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
145	144	halfcld 11277	. . . . . . . . . . . . . . . . 17 $/\$
146	142, 145, 145	subsub4d 10423	. . . . . . . . . . . . . . . 16 $/\$
147	143	2halvesd 11278	. . . . . . . . . . . . . . . . . 18
148	147	oveq2d 6666	. . . . . . . . . . . . . . . . 17
149	148	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
150	146, 149	eqtr2d 2657	. . . . . . . . . . . . . . 15 $/\$
151	150	adantll 750	. . . . . . . . . . . . . 14 $/\$ $/\$
152	151	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153	152	ad3antrrr 766	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154	127, 126	resubcld 10458	. . . . . . . . . . . . . . . 16 $/\$ $/\$
155	154	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
156	155	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157	2, 156	sseldi 3601	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	120, 49	sylanl2 683	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	125	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
160	158, 159	resubcld 10458	. . . . . . . . . . . . . . . 16 $/\$ $/\$
161	160	adantllr 755	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
162	161	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	2, 162	sseldi 3601	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164		simp-6l 810	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165		simplr 792	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	164, 165, 42	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167		simp-6r 811	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168	120	ad5antlr 771	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169	168	rehalfcld 11279	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
170	167, 169	resubcld 10458	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
171		simp-4r 807	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172	164, 171, 34	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173		simpllr 799	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174	170, 172, 169, 173	ltsub1dd 10639	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175		simpr 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	157, 163, 166, 174, 175	xrlttrd 11990	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	153, 176	eqbrtrd 4675	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178	177	ex 450	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
179	178	reximdva 3017	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
180	140, 179	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
181	180	ex 450	. . . . . . 7 $/\$ $/\$ $/\$
182	181	rexlimdva 3031	. . . . . 6 $/\$ $/\$
183	131, 182	mpd 15	. . . . 5 $/\$ $/\$
184	112, 113, 114, 183	supxrgere 39549	. . . 4 $/\$
185	92, 111, 184	syl2anc 693	. . 3 $/\$ $/\$
186	91, 185	pm2.61dan 832	. 2 $/\$
187	79, 186	pm2.61dan 832	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

wss 3574

c0 3915 class class class wbr 4653 (class class class)co 6650

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cdiv 10684

c2 11070

crp 11832

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-po 5035 df-so 5036 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-sup 8348 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-2 11079 df-rp 11833

This theorem is referenced by: (None)

W3C validator