supxrge

Description: If an extended 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	supxrge.xph	$⊢ Ⅎ x φ$
	supxrge.a	$⊢ φ \to A \subseteq ℝ^{*}$
	supxrge.b	$⊢ φ \to B \in ℝ^{*}$
	supxrge.y	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} x$
Assertion	supxrge	$⊢ φ \to B \leq sup (A ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		supxrge.xph	$⊢ Ⅎ x φ$
2		supxrge.a	$⊢ φ \to A \subseteq ℝ^{*}$
3		supxrge.b	$⊢ φ \to B \in ℝ^{*}$
4		supxrge.y	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} x$
5		pnfge	$⊢ B \in ℝ^{*} \to B \leq +∞$
6	3 5	syl	$⊢ φ \to B \leq +∞$
7	6	adantr	$⊢ (φ \land +∞ \in A) \to B \leq +∞$
8	2	adantr	$⊢ (φ \land +∞ \in A) \to A \subseteq ℝ^{*}$
9		simpr	$⊢ (φ \land +∞ \in A) \to +∞ \in A$
10		supxrpnf	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to sup (A ℝ^{} <) = +∞$
11	8 9 10	syl2anc	$⊢ (φ \land +∞ \in A) \to sup (A ℝ^{*} <) = +∞$
12	11	eqcomd	$⊢ (φ \land +∞ \in A) \to +∞ = sup (A ℝ^{*} <)$
13	7 12	breqtrd	$⊢ (φ \land +∞ \in A) \to B \leq sup (A ℝ^{*} <)$
14		simpr	$⊢ (φ \land B = −∞) \to B = −∞$
15		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
16	2 15	syl	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
17		mnfle	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to −∞ \leq sup (A ℝ^{*} <)$
18	16 17	syl	$⊢ φ \to −∞ \leq sup (A ℝ^{*} <)$
19	18	adantr	$⊢ (φ \land B = −∞) \to −∞ \leq sup (A ℝ^{*} <)$
20	14 19	eqbrtrd	$⊢ (φ \land B = −∞) \to B \leq sup (A ℝ^{*} <)$
21	20	adantlr	$⊢ ((φ \land \neg +∞ \in A) \land B = −∞) \to B \leq sup (A ℝ^{*} <)$
22		simpl	$⊢ ((φ \land \neg +∞ \in A) \land \neg B = −∞) \to (φ \land \neg +∞ \in A)$
23		neqne	$⊢ \neg B = −∞ \to B \neq −∞$
24	23	adantl	$⊢ ((φ \land \neg +∞ \in A) \land \neg B = −∞) \to B \neq −∞$
25		nfv	$⊢ Ⅎ w ((φ \land \neg +∞ \in A) \land B \neq −∞)$
26	2	adantr	$⊢ (φ \land \neg +∞ \in A) \to A \subseteq ℝ^{*}$
27	26	adantr	$⊢ ((φ \land \neg +∞ \in A) \land B \neq −∞) \to A \subseteq ℝ^{*}$
28	3	adantr	$⊢ (φ \land \neg +∞ \in A) \to B \in ℝ^{*}$
29	28	adantr	$⊢ ((φ \land \neg +∞ \in A) \land B \neq −∞) \to B \in ℝ^{*}$
30		simpl	$⊢ (φ \land w \in ℝ^{+}) \to φ$
31		rphalfcl	$⊢ w \in ℝ^{+} \to \frac{w}{2} \in ℝ^{+}$
32	31	adantl	$⊢ (φ \land w \in ℝ^{+}) \to \frac{w}{2} \in ℝ^{+}$
33		ovex	$⊢ \frac{w}{2} \in V$
34		nfcv	$⊢ \underline{Ⅎ} x (\frac{w}{2})$
35		nfv	$⊢ Ⅎ x \frac{w}{2} \in ℝ^{+}$
36	1 35	nfan	$⊢ Ⅎ x (φ \land \frac{w}{2} \in ℝ^{+})$
37		nfv	$⊢ Ⅎ x \exists y \in A B \leq y +_{𝑒} (\frac{w}{2})$
38	36 37	nfim	$⊢ Ⅎ x ((φ \land \frac{w}{2} \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} (\frac{w}{2}))$
39		eleq1	$⊢ x = \frac{w}{2} \to (x \in ℝ^{+} \leftrightarrow \frac{w}{2} \in ℝ^{+})$
40	39	anbi2d	$⊢ x = \frac{w}{2} \to ((φ \land x \in ℝ^{+}) \leftrightarrow (φ \land \frac{w}{2} \in ℝ^{+}))$
41		oveq2	$⊢ x = \frac{w}{2} \to y +_{𝑒} x = y +_{𝑒} (\frac{w}{2})$
42	41	breq2d	$⊢ x = \frac{w}{2} \to (B \leq y +_{𝑒} x \leftrightarrow B \leq y +_{𝑒} (\frac{w}{2}))$
43	42	rexbidv	$⊢ x = \frac{w}{2} \to (\exists y \in A B \leq y +_{𝑒} x \leftrightarrow \exists y \in A B \leq y +_{𝑒} (\frac{w}{2}))$
44	40 43	imbi12d	$⊢ x = \frac{w}{2} \to (((φ \land x \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} x) \leftrightarrow ((φ \land \frac{w}{2} \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} (\frac{w}{2})))$
45	34 38 44 4	vtoclgf	$⊢ \frac{w}{2} \in V \to ((φ \land \frac{w}{2} \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} (\frac{w}{2}))$
46	33 45	ax-mp	$⊢ (φ \land \frac{w}{2} \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} (\frac{w}{2})$
47	30 32 46	syl2anc	$⊢ (φ \land w \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} (\frac{w}{2})$
48	47	adantlr	$⊢ ((φ \land \neg +∞ \in A) \land w \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} (\frac{w}{2})$
49	48	adantlr	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to \exists y \in A B \leq y +_{𝑒} (\frac{w}{2})$
50		nfv	$⊢ Ⅎ y (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+})$
51		neneq	$⊢ B \neq −∞ \to \neg B = −∞$
52	51	adantl	$⊢ (φ \land B \neq −∞) \to \neg B = −∞$
53	3	adantr	$⊢ (φ \land B \neq −∞) \to B \in ℝ^{*}$
54		ngtmnft	$⊢ B \in ℝ^{*} \to (B = −∞ \leftrightarrow \neg −∞ < B)$
55	53 54	syl	$⊢ (φ \land B \neq −∞) \to (B = −∞ \leftrightarrow \neg −∞ < B)$
56	52 55	mtbid	$⊢ (φ \land B \neq −∞) \to \neg \neg −∞ < B$
57	56	notnotrd	$⊢ (φ \land B \neq −∞) \to −∞ < B$
58	57	ad4ant13	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to −∞ < B$
59	58	3ad2ant1	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to −∞ < B$
60	29	adantr	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to B \in ℝ^{*}$
61	60	3ad2ant1	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to B \in ℝ^{*}$
62	61	adantr	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to B \in ℝ^{*}$
63		mnfxr	$⊢ −∞ \in ℝ^{*}$
64	63	a1i	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to −∞ \in ℝ^{*}$
65		simpl3	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to B \leq y +_{𝑒} (\frac{w}{2})$
66		simpr	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to \neg −∞ < y$
67	2	sselda	$⊢ (φ \land y \in A) \to y \in ℝ^{*}$
68	67	adantr	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y \in ℝ^{*}$
69		ngtmnft	$⊢ y \in ℝ^{*} \to (y = −∞ \leftrightarrow \neg −∞ < y)$
70	68 69	syl	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to (y = −∞ \leftrightarrow \neg −∞ < y)$
71	66 70	mpbird	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y = −∞$
72	71	oveq1d	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y +_{𝑒} (\frac{w}{2}) = −∞ +_{𝑒} (\frac{w}{2})$
73	72	adantllr	$⊢ (((φ \land w \in ℝ^{+}) \land y \in A) \land \neg −∞ < y) \to y +_{𝑒} (\frac{w}{2}) = −∞ +_{𝑒} (\frac{w}{2})$
74	31	rpxrd	$⊢ w \in ℝ^{+} \to \frac{w}{2} \in ℝ^{*}$
75	31	rpred	$⊢ w \in ℝ^{+} \to \frac{w}{2} \in ℝ$
76		renepnf	$⊢ \frac{w}{2} \in ℝ \to \frac{w}{2} \neq +∞$
77	75 76	syl	$⊢ w \in ℝ^{+} \to \frac{w}{2} \neq +∞$
78		xaddmnf2	$⊢ (\frac{w}{2} \in ℝ^{*} \land \frac{w}{2} \neq +∞) \to −∞ +_{𝑒} (\frac{w}{2}) = −∞$
79	74 77 78	syl2anc	$⊢ w \in ℝ^{+} \to −∞ +_{𝑒} (\frac{w}{2}) = −∞$
80	79	adantl	$⊢ (φ \land w \in ℝ^{+}) \to −∞ +_{𝑒} (\frac{w}{2}) = −∞$
81	80	ad2antrr	$⊢ (((φ \land w \in ℝ^{+}) \land y \in A) \land \neg −∞ < y) \to −∞ +_{𝑒} (\frac{w}{2}) = −∞$
82	73 81	eqtrd	$⊢ (((φ \land w \in ℝ^{+}) \land y \in A) \land \neg −∞ < y) \to y +_{𝑒} (\frac{w}{2}) = −∞$
83	82	adantl3r	$⊢ ((((φ \land \neg +∞ \in A) \land w \in ℝ^{+}) \land y \in A) \land \neg −∞ < y) \to y +_{𝑒} (\frac{w}{2}) = −∞$
84	83	adantl3r	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A) \land \neg −∞ < y) \to y +_{𝑒} (\frac{w}{2}) = −∞$
85	84	3adantl3	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to y +_{𝑒} (\frac{w}{2}) = −∞$
86	65 85	breqtrd	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to B \leq −∞$
87		mnfle	$⊢ B \in ℝ^{*} \to −∞ \leq B$
88	3 87	syl	$⊢ φ \to −∞ \leq B$
89	88	adantr	$⊢ (φ \land \neg +∞ \in A) \to −∞ \leq B$
90	89	ad3antrrr	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land \neg −∞ < y) \to −∞ \leq B$
91	90	3ad2antl1	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to −∞ \leq B$
92	62 64 86 91	xrletrid	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to B = −∞$
93		simpllr	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land \neg −∞ < y) \to B \neq −∞$
94	93	3ad2antl1	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to B \neq −∞$
95	94	neneqd	$⊢ (((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \land \neg −∞ < y) \to \neg B = −∞$
96	92 95	condan	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to −∞ < y$
97		simpr	$⊢ ((φ \land y \in A) \land \neg y < +∞) \to \neg y < +∞$
98	67	adantr	$⊢ ((φ \land y \in A) \land \neg y < +∞) \to y \in ℝ^{*}$
99		nltpnft	$⊢ y \in ℝ^{*} \to (y = +∞ \leftrightarrow \neg y < +∞)$
100	98 99	syl	$⊢ ((φ \land y \in A) \land \neg y < +∞) \to (y = +∞ \leftrightarrow \neg y < +∞)$
101	97 100	mpbird	$⊢ ((φ \land y \in A) \land \neg y < +∞) \to y = +∞$
102	101	eqcomd	$⊢ ((φ \land y \in A) \land \neg y < +∞) \to +∞ = y$
103		simpr	$⊢ (φ \land y \in A) \to y \in A$
104	103	adantr	$⊢ ((φ \land y \in A) \land \neg y < +∞) \to y \in A$
105	102 104	eqeltrd	$⊢ ((φ \land y \in A) \land \neg y < +∞) \to +∞ \in A$
106	105	3adantl2	$⊢ ((φ \land \neg +∞ \in A \land y \in A) \land \neg y < +∞) \to +∞ \in A$
107		simpl2	$⊢ ((φ \land \neg +∞ \in A \land y \in A) \land \neg y < +∞) \to \neg +∞ \in A$
108	106 107	condan	$⊢ (φ \land \neg +∞ \in A \land y \in A) \to y < +∞$
109	108	ad5ant125	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A) \to y < +∞$
110	109	3adant3	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y < +∞$
111	96 110	jca	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to (−∞ < y \land y < +∞)$
112	67	ad5ant15	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A) \to y \in ℝ^{*}$
113	112	3adant3	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y \in ℝ^{*}$
114		xrrebnd	$⊢ y \in ℝ^{*} \to (y \in ℝ \leftrightarrow (−∞ < y \land y < +∞))$
115	113 114	syl	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to (y \in ℝ \leftrightarrow (−∞ < y \land y < +∞))$
116	111 115	mpbird	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y \in ℝ$
117	75	adantl	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to \frac{w}{2} \in ℝ$
118	117	3ad2ant1	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to \frac{w}{2} \in ℝ$
119		rexadd	$⊢ (y \in ℝ \land \frac{w}{2} \in ℝ) \to y +_{𝑒} (\frac{w}{2}) = y + (\frac{w}{2})$
120	116 118 119	syl2anc	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y +_{𝑒} (\frac{w}{2}) = y + (\frac{w}{2})$
121	116 118	readdcld	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y + (\frac{w}{2}) \in ℝ$
122	120 121	eqeltrd	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y +_{𝑒} (\frac{w}{2}) \in ℝ$
123	122	rexrd	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y +_{𝑒} (\frac{w}{2}) \in ℝ^{*}$
124		pnfxr	$⊢ +∞ \in ℝ^{*}$
125	124	a1i	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to +∞ \in ℝ^{*}$
126		simp3	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to B \leq y +_{𝑒} (\frac{w}{2})$
127	122	ltpnfd	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y +_{𝑒} (\frac{w}{2}) < +∞$
128	61 123 125 126 127	xrlelttrd	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to B < +∞$
129	59 128	jca	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to (−∞ < B \land B < +∞)$
130		xrrebnd	$⊢ B \in ℝ^{*} \to (B \in ℝ \leftrightarrow (−∞ < B \land B < +∞))$
131	61 130	syl	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to (B \in ℝ \leftrightarrow (−∞ < B \land B < +∞))$
132	129 131	mpbird	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to B \in ℝ$
133		rpre	$⊢ w \in ℝ^{+} \to w \in ℝ$
134	133	adantl	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to w \in ℝ$
135	134	3ad2ant1	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to w \in ℝ$
136		rexadd	$⊢ (y \in ℝ \land w \in ℝ) \to y +_{𝑒} w = y + w$
137	116 135 136	syl2anc	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y +_{𝑒} w = y + w$
138	116 135	readdcld	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y + w \in ℝ$
139	137 138	eqeltrd	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y +_{𝑒} w \in ℝ$
140		rphalflt	$⊢ w \in ℝ^{+} \to \frac{w}{2} < w$
141	140	adantl	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to \frac{w}{2} < w$
142	141	3ad2ant1	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to \frac{w}{2} < w$
143	118 135 116 142	ltadd2dd	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y + (\frac{w}{2}) < y + w$
144	120 137	breq12d	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to (y +_{𝑒} (\frac{w}{2}) < y +_{𝑒} w \leftrightarrow y + (\frac{w}{2}) < y + w)$
145	143 144	mpbird	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to y +_{𝑒} (\frac{w}{2}) < y +_{𝑒} w$
146	132 122 139 126 145	lelttrd	$⊢ ((((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \land y \in A \land B \leq y +_{𝑒} (\frac{w}{2})) \to B < y +_{𝑒} w$
147	146	3exp	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to (y \in A \to (B \leq y +_{𝑒} (\frac{w}{2}) \to B < y +_{𝑒} w))$
148	50 147	reximdai	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to (\exists y \in A B \leq y +_{𝑒} (\frac{w}{2}) \to \exists y \in A B < y +_{𝑒} w)$
149	49 148	mpd	$⊢ (((φ \land \neg +∞ \in A) \land B \neq −∞) \land w \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} w$
150	25 27 29 149	supxrgelem	$⊢ ((φ \land \neg +∞ \in A) \land B \neq −∞) \to B \leq sup (A ℝ^{*} <)$
151	22 24 150	syl2anc	$⊢ ((φ \land \neg +∞ \in A) \land \neg B = −∞) \to B \leq sup (A ℝ^{*} <)$
152	21 151	pm2.61dan	$⊢ (φ \land \neg +∞ \in A) \to B \leq sup (A ℝ^{*} <)$
153	13 152	pm2.61dan	$⊢ φ \to B \leq sup (A ℝ^{*} <)$

Metamath Proof Explorer

Theorem supxrge

Proof