supxrgere

Description: If a real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	supxrgere.xph	$⊢ Ⅎ x φ$
	supxrgere.a	$⊢ φ \to A \subseteq ℝ^{*}$
	supxrgere.b	$⊢ φ \to B \in ℝ$
	supxrgere.y	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in A B - x < y$
Assertion	supxrgere	$⊢ φ \to B \leq sup (A ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		supxrgere.xph	$⊢ Ⅎ x φ$
2		supxrgere.a	$⊢ φ \to A \subseteq ℝ^{*}$
3		supxrgere.b	$⊢ φ \to B \in ℝ$
4		supxrgere.y	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in A B - x < y$
5		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7	6	a1i	$⊢ B \in ℝ \to +∞ \in ℝ^{*}$
8		ltpnf	$⊢ B \in ℝ \to B < +∞$
9	5 7 8	xrltled	$⊢ B \in ℝ \to B \leq +∞$
10	3 9	syl	$⊢ φ \to B \leq +∞$
11	10	adantr	$⊢ (φ \land sup (A ℝ^{*} <) = +∞) \to B \leq +∞$
12		id	$⊢ sup (A ℝ^{} <) = +∞ \to sup (A ℝ^{} <) = +∞$
13	12	eqcomd	$⊢ sup (A ℝ^{} <) = +∞ \to +∞ = sup (A ℝ^{} <)$
14	13	adantl	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to +∞ = sup (A ℝ^{} <)$
15	11 14	breqtrd	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to B \leq sup (A ℝ^{} <)$
16		simpl	$⊢ (φ \land \neg sup (A ℝ^{*} <) = +∞) \to φ$
17		1rp	$⊢ 1 \in ℝ^{+}$
18		nfcv	$⊢ \underline{Ⅎ} x 1$
19		nfv	$⊢ Ⅎ x 1 \in ℝ^{+}$
20	1 19	nfan	$⊢ Ⅎ x (φ \land 1 \in ℝ^{+})$
21		nfv	$⊢ Ⅎ x \exists y \in A B - 1 < y$
22	20 21	nfim	$⊢ Ⅎ x ((φ \land 1 \in ℝ^{+}) \to \exists y \in A B - 1 < y)$
23		eleq1	$⊢ x = 1 \to (x \in ℝ^{+} \leftrightarrow 1 \in ℝ^{+})$
24	23	anbi2d	$⊢ x = 1 \to ((φ \land x \in ℝ^{+}) \leftrightarrow (φ \land 1 \in ℝ^{+}))$
25		oveq2	$⊢ x = 1 \to B - x = B - 1$
26	25	breq1d	$⊢ x = 1 \to (B - x < y \leftrightarrow B - 1 < y)$
27	26	rexbidv	$⊢ x = 1 \to (\exists y \in A B - x < y \leftrightarrow \exists y \in A B - 1 < y)$
28	24 27	imbi12d	$⊢ x = 1 \to (((φ \land x \in ℝ^{+}) \to \exists y \in A B - x < y) \leftrightarrow ((φ \land 1 \in ℝ^{+}) \to \exists y \in A B - 1 < y))$
29	18 22 28 4	vtoclgf	$⊢ 1 \in ℝ^{+} \to ((φ \land 1 \in ℝ^{+}) \to \exists y \in A B - 1 < y)$
30	17 29	ax-mp	$⊢ (φ \land 1 \in ℝ^{+}) \to \exists y \in A B - 1 < y$
31	17 30	mpan2	$⊢ φ \to \exists y \in A B - 1 < y$
32	31	adantr	$⊢ (φ \land \neg sup (A ℝ^{*} <) = +∞) \to \exists y \in A B - 1 < y$
33		mnfxr	$⊢ −∞ \in ℝ^{*}$
34	33	a1i	$⊢ (φ \land y \in A \land B - 1 < y) \to −∞ \in ℝ^{*}$
35	2	sselda	$⊢ (φ \land y \in A) \to y \in ℝ^{*}$
36	35	3adant3	$⊢ (φ \land y \in A \land B - 1 < y) \to y \in ℝ^{*}$
37		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
38	2 37	syl	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
39	38	3ad2ant1	$⊢ (φ \land y \in A \land B - 1 < y) \to sup (A ℝ^{} <) \in ℝ^{}$
40		peano2rem	$⊢ B \in ℝ \to B - 1 \in ℝ$
41	3 40	syl	$⊢ φ \to B - 1 \in ℝ$
42	41	rexrd	$⊢ φ \to B - 1 \in ℝ^{*}$
43	42	adantr	$⊢ (φ \land \neg −∞ < y) \to B - 1 \in ℝ^{*}$
44	43	3ad2antl1	$⊢ ((φ \land y \in A \land B - 1 < y) \land \neg −∞ < y) \to B - 1 \in ℝ^{*}$
45	36	adantr	$⊢ ((φ \land y \in A \land B - 1 < y) \land \neg −∞ < y) \to y \in ℝ^{*}$
46	33	a1i	$⊢ ((φ \land y \in A \land B - 1 < y) \land \neg −∞ < y) \to −∞ \in ℝ^{*}$
47		simpl3	$⊢ ((φ \land y \in A \land B - 1 < y) \land \neg −∞ < y) \to B - 1 < y$
48		simpr	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to \neg −∞ < y$
49	35	adantr	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y \in ℝ^{*}$
50	33	a1i	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to −∞ \in ℝ^{*}$
51		xrlenlt	$⊢ (y \in ℝ^{} \land −∞ \in ℝ^{}) \to (y \leq −∞ \leftrightarrow \neg −∞ < y)$
52	49 50 51	syl2anc	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to (y \leq −∞ \leftrightarrow \neg −∞ < y)$
53	48 52	mpbird	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y \leq −∞$
54	53	3adantl3	$⊢ ((φ \land y \in A \land B - 1 < y) \land \neg −∞ < y) \to y \leq −∞$
55	44 45 46 47 54	xrltletrd	$⊢ ((φ \land y \in A \land B - 1 < y) \land \neg −∞ < y) \to B - 1 < −∞$
56		nltmnf	$⊢ B - 1 \in ℝ^{*} \to \neg B - 1 < −∞$
57	42 56	syl	$⊢ φ \to \neg B - 1 < −∞$
58	57	adantr	$⊢ (φ \land \neg −∞ < y) \to \neg B - 1 < −∞$
59	58	3ad2antl1	$⊢ ((φ \land y \in A \land B - 1 < y) \land \neg −∞ < y) \to \neg B - 1 < −∞$
60	55 59	condan	$⊢ (φ \land y \in A \land B - 1 < y) \to −∞ < y$
61	2	adantr	$⊢ (φ \land y \in A) \to A \subseteq ℝ^{*}$
62		simpr	$⊢ (φ \land y \in A) \to y \in A$
63		supxrub	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \leq sup (A ℝ^{} <)$
64	61 62 63	syl2anc	$⊢ (φ \land y \in A) \to y \leq sup (A ℝ^{*} <)$
65	64	3adant3	$⊢ (φ \land y \in A \land B - 1 < y) \to y \leq sup (A ℝ^{*} <)$
66	34 36 39 60 65	xrltletrd	$⊢ (φ \land y \in A \land B - 1 < y) \to −∞ < sup (A ℝ^{*} <)$
67	66	3exp	$⊢ φ \to (y \in A \to (B - 1 < y \to −∞ < sup (A ℝ^{*} <)))$
68	67	adantr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (y \in A \to (B - 1 < y \to −∞ < sup (A ℝ^{} <)))$
69	68	rexlimdv	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (\exists y \in A B - 1 < y \to −∞ < sup (A ℝ^{} <))$
70	32 69	mpd	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to −∞ < sup (A ℝ^{} <)$
71		simpr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to \neg sup (A ℝ^{} <) = +∞$
72		nltpnft	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
73	38 72	syl	$⊢ φ \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
74	73	adantr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{*} <) < +∞)$
75	71 74	mtbid	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to \neg \neg sup (A ℝ^{} <) < +∞$
76	75	notnotrd	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) < +∞$
77	70 76	jca	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞)$
78	38	adantr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) \in ℝ^{*}$
79		xrrebnd	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞))$
80	78 79	syl	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{} <) < +∞))$
81	77 80	mpbird	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) \in ℝ$
82		simpl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to (φ \land sup (A ℝ^{*} <) \in ℝ)$
83		simpr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to \neg B \leq sup (A ℝ^{*} <)$
84	82	simprd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to sup (A ℝ^{*} <) \in ℝ$
85	3	ad2antrr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to B \in ℝ$
86	84 85	ltnled	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to (sup (A ℝ^{} <) < B \leftrightarrow \neg B \leq sup (A ℝ^{} <))$
87	83 86	mpbird	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to sup (A ℝ^{*} <) < B$
88		simpll	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to φ$
89	3	adantr	$⊢ (φ \land sup (A ℝ^{*} <) \in ℝ) \to B \in ℝ$
90		simpr	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to sup (A ℝ^{} <) \in ℝ$
91	89 90	resubcld	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to B - sup (A ℝ^{} <) \in ℝ$
92	91	adantr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - sup (A ℝ^{*} <) \in ℝ$
93		simpr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to sup (A ℝ^{*} <) < B$
94	90	adantr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to sup (A ℝ^{*} <) \in ℝ$
95	88 3	syl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B \in ℝ$
96	94 95	posdifd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (sup (A ℝ^{} <) < B \leftrightarrow 0 < B - sup (A ℝ^{} <))$
97	93 96	mpbid	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to 0 < B - sup (A ℝ^{*} <)$
98	92 97	elrpd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - sup (A ℝ^{*} <) \in ℝ^{+}$
99		ovex	$⊢ B - sup (A ℝ^{*} <) \in V$
100		nfcv	$⊢ \underline{Ⅎ} x (B - sup (A ℝ^{*} <))$
101		nfv	$⊢ Ⅎ x B - sup (A ℝ^{*} <) \in ℝ^{+}$
102	1 101	nfan	$⊢ Ⅎ x (φ \land B - sup (A ℝ^{*} <) \in ℝ^{+})$
103		nfv	$⊢ Ⅎ x \exists y \in A B - (B - sup (A ℝ^{*} <)) < y$
104	102 103	nfim	$⊢ Ⅎ x ((φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B - (B - sup (A ℝ^{} <)) < y)$
105		eleq1	$⊢ x = B - sup (A ℝ^{} <) \to (x \in ℝ^{+} \leftrightarrow B - sup (A ℝ^{} <) \in ℝ^{+})$
106	105	anbi2d	$⊢ x = B - sup (A ℝ^{} <) \to ((φ \land x \in ℝ^{+}) \leftrightarrow (φ \land B - sup (A ℝ^{} <) \in ℝ^{+}))$
107		oveq2	$⊢ x = B - sup (A ℝ^{} <) \to B - x = B - (B - sup (A ℝ^{} <))$
108	107	breq1d	$⊢ x = B - sup (A ℝ^{} <) \to (B - x < y \leftrightarrow B - (B - sup (A ℝ^{} <)) < y)$
109	108	rexbidv	$⊢ x = B - sup (A ℝ^{} <) \to (\exists y \in A B - x < y \leftrightarrow \exists y \in A B - (B - sup (A ℝ^{} <)) < y)$
110	106 109	imbi12d	$⊢ x = B - sup (A ℝ^{} <) \to (((φ \land x \in ℝ^{+}) \to \exists y \in A B - x < y) \leftrightarrow ((φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B - (B - sup (A ℝ^{*} <)) < y))$
111	100 104 110 4	vtoclgf	$⊢ B - sup (A ℝ^{} <) \in V \to ((φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B - (B - sup (A ℝ^{*} <)) < y)$
112	99 111	ax-mp	$⊢ (φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B - (B - sup (A ℝ^{} <)) < y$
113	88 98 112	syl2anc	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to \exists y \in A B - (B - sup (A ℝ^{*} <)) < y$
114	3	recnd	$⊢ φ \to B \in ℂ$
115	114	ad3antrrr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land B - (B - sup (A ℝ^{*} <)) < y) \to B \in ℂ$
116	90	recnd	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to sup (A ℝ^{} <) \in ℂ$
117	116	ad2antrr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land B - (B - sup (A ℝ^{} <)) < y) \to sup (A ℝ^{} <) \in ℂ$
118	115 117	nncand	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land B - (B - sup (A ℝ^{} <)) < y) \to B - (B - sup (A ℝ^{} <)) = sup (A ℝ^{*} <)$
119	118	eqcomd	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land B - (B - sup (A ℝ^{} <)) < y) \to sup (A ℝ^{} <) = B - (B - sup (A ℝ^{*} <))$
120		simpr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land B - (B - sup (A ℝ^{} <)) < y) \to B - (B - sup (A ℝ^{} <)) < y$
121	119 120	eqbrtrd	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land B - (B - sup (A ℝ^{} <)) < y) \to sup (A ℝ^{} <) < y$
122	121	ex	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (B - (B - sup (A ℝ^{} <)) < y \to sup (A ℝ^{} <) < y)$
123	122	adantr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \to (B - (B - sup (A ℝ^{} <)) < y \to sup (A ℝ^{} <) < y)$
124	123	reximdva	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (\exists y \in A B - (B - sup (A ℝ^{} <)) < y \to \exists y \in A sup (A ℝ^{} <) < y)$
125	113 124	mpd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to \exists y \in A sup (A ℝ^{*} <) < y$
126	82 87 125	syl2anc	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to \exists y \in A sup (A ℝ^{*} <) < y$
127	61 37	syl	$⊢ (φ \land y \in A) \to sup (A ℝ^{} <) \in ℝ^{}$
128	35 127	xrlenltd	$⊢ (φ \land y \in A) \to (y \leq sup (A ℝ^{} <) \leftrightarrow \neg sup (A ℝ^{} <) < y)$
129	64 128	mpbid	$⊢ (φ \land y \in A) \to \neg sup (A ℝ^{*} <) < y$
130	129	ralrimiva	$⊢ φ \to \forall y \in A \neg sup (A ℝ^{*} <) < y$
131		ralnex	$⊢ \forall y \in A \neg sup (A ℝ^{} <) < y \leftrightarrow \neg \exists y \in A sup (A ℝ^{} <) < y$
132	130 131	sylib	$⊢ φ \to \neg \exists y \in A sup (A ℝ^{*} <) < y$
133	132	ad2antrr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to \neg \exists y \in A sup (A ℝ^{*} <) < y$
134	126 133	condan	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to B \leq sup (A ℝ^{} <)$
135	16 81 134	syl2anc	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to B \leq sup (A ℝ^{} <)$
136	15 135	pm2.61dan	$⊢ φ \to B \leq sup (A ℝ^{*} <)$

Metamath Proof Explorer

Theorem supxrgere

Proof