supxrgelem

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

Proof

Step	Hyp	Ref	Expression
1		supxrgelem.xph	$⊢ Ⅎ x φ$
2		supxrgelem.a	$⊢ φ \to A \subseteq ℝ^{*}$
3		supxrgelem.b	$⊢ φ \to B \in ℝ^{*}$
4		supxrgelem.y	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} x$
5		pnfge	$⊢ B \in ℝ^{*} \to B \leq +∞$
6	3 5	syl	$⊢ φ \to B \leq +∞$
7	6	adantr	$⊢ (φ \land sup (A ℝ^{*} <) = +∞) \to B \leq +∞$
8		id	$⊢ sup (A ℝ^{} <) = +∞ \to sup (A ℝ^{} <) = +∞$
9	8	eqcomd	$⊢ sup (A ℝ^{} <) = +∞ \to +∞ = sup (A ℝ^{} <)$
10	9	adantl	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to +∞ = sup (A ℝ^{} <)$
11	7 10	breqtrd	$⊢ (φ \land sup (A ℝ^{} <) = +∞) \to B \leq sup (A ℝ^{} <)$
12		simpl	$⊢ (φ \land \neg sup (A ℝ^{*} <) = +∞) \to φ$
13		1rp	$⊢ 1 \in ℝ^{+}$
14		nfcv	$⊢ \underline{Ⅎ} x 1$
15		nfv	$⊢ Ⅎ x 1 \in ℝ^{+}$
16	1 15	nfan	$⊢ Ⅎ x (φ \land 1 \in ℝ^{+})$
17		nfv	$⊢ Ⅎ x \exists y \in A B < y +_{𝑒} 1$
18	16 17	nfim	$⊢ Ⅎ x ((φ \land 1 \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} 1)$
19		eleq1	$⊢ x = 1 \to (x \in ℝ^{+} \leftrightarrow 1 \in ℝ^{+})$
20	19	anbi2d	$⊢ x = 1 \to ((φ \land x \in ℝ^{+}) \leftrightarrow (φ \land 1 \in ℝ^{+}))$
21		oveq2	$⊢ x = 1 \to y +_{𝑒} x = y +_{𝑒} 1$
22	21	breq2d	$⊢ x = 1 \to (B < y +_{𝑒} x \leftrightarrow B < y +_{𝑒} 1)$
23	22	rexbidv	$⊢ x = 1 \to (\exists y \in A B < y +_{𝑒} x \leftrightarrow \exists y \in A B < y +_{𝑒} 1)$
24	20 23	imbi12d	$⊢ x = 1 \to (((φ \land x \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} x) \leftrightarrow ((φ \land 1 \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} 1))$
25	14 18 24 4	vtoclgf	$⊢ 1 \in ℝ^{+} \to ((φ \land 1 \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} 1)$
26	13 25	ax-mp	$⊢ (φ \land 1 \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} 1$
27	13 26	mpan2	$⊢ φ \to \exists y \in A B < y +_{𝑒} 1$
28	27	adantr	$⊢ (φ \land \neg sup (A ℝ^{*} <) = +∞) \to \exists y \in A B < y +_{𝑒} 1$
29		mnfxr	$⊢ −∞ \in ℝ^{*}$
30	29	a1i	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to −∞ \in ℝ^{*}$
31	2	sselda	$⊢ (φ \land y \in A) \to y \in ℝ^{*}$
32	31	3adant3	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to y \in ℝ^{*}$
33		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
34	2 33	syl	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
35	34	3ad2ant1	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to sup (A ℝ^{} <) \in ℝ^{}$
36		simpl3	$⊢ ((φ \land y \in A \land B < y +_{𝑒} 1) \land \neg −∞ < y) \to B < y +_{𝑒} 1$
37		simpr	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to \neg −∞ < y$
38	31	adantr	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y \in ℝ^{*}$
39		ngtmnft	$⊢ y \in ℝ^{*} \to (y = −∞ \leftrightarrow \neg −∞ < y)$
40	38 39	syl	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to (y = −∞ \leftrightarrow \neg −∞ < y)$
41	37 40	mpbird	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y = −∞$
42	41	oveq1d	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y +_{𝑒} 1 = −∞ +_{𝑒} 1$
43		1xr	$⊢ 1 \in ℝ^{*}$
44	43	a1i	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to 1 \in ℝ^{*}$
45		1re	$⊢ 1 \in ℝ$
46		renepnf	$⊢ 1 \in ℝ \to 1 \neq +∞$
47	45 46	ax-mp	$⊢ 1 \neq +∞$
48	47	a1i	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to 1 \neq +∞$
49		xaddmnf2	$⊢ (1 \in ℝ^{*} \land 1 \neq +∞) \to −∞ +_{𝑒} 1 = −∞$
50	44 48 49	syl2anc	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to −∞ +_{𝑒} 1 = −∞$
51	42 50	eqtrd	$⊢ ((φ \land y \in A) \land \neg −∞ < y) \to y +_{𝑒} 1 = −∞$
52	51	3adantl3	$⊢ ((φ \land y \in A \land B < y +_{𝑒} 1) \land \neg −∞ < y) \to y +_{𝑒} 1 = −∞$
53	36 52	breqtrd	$⊢ ((φ \land y \in A \land B < y +_{𝑒} 1) \land \neg −∞ < y) \to B < −∞$
54		nltmnf	$⊢ B \in ℝ^{*} \to \neg B < −∞$
55	3 54	syl	$⊢ φ \to \neg B < −∞$
56	55	adantr	$⊢ (φ \land \neg −∞ < y) \to \neg B < −∞$
57	56	3ad2antl1	$⊢ ((φ \land y \in A \land B < y +_{𝑒} 1) \land \neg −∞ < y) \to \neg B < −∞$
58	53 57	condan	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to −∞ < y$
59	2	adantr	$⊢ (φ \land y \in A) \to A \subseteq ℝ^{*}$
60		simpr	$⊢ (φ \land y \in A) \to y \in A$
61		supxrub	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \leq sup (A ℝ^{} <)$
62	59 60 61	syl2anc	$⊢ (φ \land y \in A) \to y \leq sup (A ℝ^{*} <)$
63	62	3adant3	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to y \leq sup (A ℝ^{*} <)$
64	30 32 35 58 63	xrltletrd	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to −∞ < sup (A ℝ^{*} <)$
65	64	3exp	$⊢ φ \to (y \in A \to (B < y +_{𝑒} 1 \to −∞ < sup (A ℝ^{*} <)))$
66	65	adantr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (y \in A \to (B < y +_{𝑒} 1 \to −∞ < sup (A ℝ^{} <)))$
67	66	rexlimdv	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (\exists y \in A B < y +_{𝑒} 1 \to −∞ < sup (A ℝ^{} <))$
68	28 67	mpd	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to −∞ < sup (A ℝ^{} <)$
69		simpr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to \neg sup (A ℝ^{} <) = +∞$
70		nltpnft	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
71	34 70	syl	$⊢ φ \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{} <) < +∞)$
72	71	adantr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (sup (A ℝ^{} <) = +∞ \leftrightarrow \neg sup (A ℝ^{*} <) < +∞)$
73	69 72	mtbid	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to \neg \neg sup (A ℝ^{} <) < +∞$
74	73	notnotrd	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) < +∞$
75	68 74	jca	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞)$
76	34	adantr	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) \in ℝ^{*}$
77		xrrebnd	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{*} <) < +∞))$
78	76 77	syl	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to (sup (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{} <) < +∞))$
79	75 78	mpbird	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to sup (A ℝ^{} <) \in ℝ$
80		simpl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to (φ \land sup (A ℝ^{*} <) \in ℝ)$
81		simpr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to \neg B \leq sup (A ℝ^{*} <)$
82	34	adantr	$⊢ (φ \land \neg B \leq sup (A ℝ^{} <)) \to sup (A ℝ^{} <) \in ℝ^{*}$
83	3	adantr	$⊢ (φ \land \neg B \leq sup (A ℝ^{} <)) \to B \in ℝ^{}$
84		xrltnle	$⊢ (sup (A ℝ^{} <) \in ℝ^{} \land B \in ℝ^{}) \to (sup (A ℝ^{} <) < B \leftrightarrow \neg B \leq sup (A ℝ^{*} <))$
85	82 83 84	syl2anc	$⊢ (φ \land \neg B \leq sup (A ℝ^{} <)) \to (sup (A ℝ^{} <) < B \leftrightarrow \neg B \leq sup (A ℝ^{*} <))$
86	85	adantlr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to (sup (A ℝ^{} <) < B \leftrightarrow \neg B \leq sup (A ℝ^{} <))$
87	81 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	29	a1i	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to −∞ \in ℝ^{*}$
90	88 34	syl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to sup (A ℝ^{} <) \in ℝ^{}$
91	88 3	syl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B \in ℝ^{*}$
92		mnfle	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to −∞ \leq sup (A ℝ^{*} <)$
93	34 92	syl	$⊢ φ \to −∞ \leq sup (A ℝ^{*} <)$
94	93	ad2antrr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to −∞ \leq sup (A ℝ^{*} <)$
95		simpr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to sup (A ℝ^{*} <) < B$
96	89 90 91 94 95	xrlelttrd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to −∞ < B$
97		id	$⊢ φ \to φ$
98	13	a1i	$⊢ φ \to 1 \in ℝ^{+}$
99	97 98 26	syl2anc	$⊢ φ \to \exists y \in A B < y +_{𝑒} 1$
100	99	ad2antrr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to \exists y \in A B < y +_{𝑒} 1$
101	3	3ad2ant1	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to B \in ℝ^{*}$
102	43	a1i	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to 1 \in ℝ^{*}$
103	32 102	jca	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to (y \in ℝ^{} \land 1 \in ℝ^{})$
104		xaddcl	$⊢ (y \in ℝ^{} \land 1 \in ℝ^{}) \to y +_{𝑒} 1 \in ℝ^{*}$
105	103 104	syl	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to y +_{𝑒} 1 \in ℝ^{*}$
106		pnfxr	$⊢ +∞ \in ℝ^{*}$
107	106	a1i	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to +∞ \in ℝ^{*}$
108		simp3	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to B < y +_{𝑒} 1$
109	31 43 104	sylancl	$⊢ (φ \land y \in A) \to y +_{𝑒} 1 \in ℝ^{*}$
110		pnfge	$⊢ y +_{𝑒} 1 \in ℝ^{*} \to y +_{𝑒} 1 \leq +∞$
111	109 110	syl	$⊢ (φ \land y \in A) \to y +_{𝑒} 1 \leq +∞$
112	111	3adant3	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to y +_{𝑒} 1 \leq +∞$
113	101 105 107 108 112	xrltletrd	$⊢ (φ \land y \in A \land B < y +_{𝑒} 1) \to B < +∞$
114	113	3exp	$⊢ φ \to (y \in A \to (B < y +_{𝑒} 1 \to B < +∞))$
115	114	rexlimdv	$⊢ φ \to (\exists y \in A B < y +_{𝑒} 1 \to B < +∞)$
116	88 115	syl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (\exists y \in A B < y +_{𝑒} 1 \to B < +∞)$
117	100 116	mpd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B < +∞$
118	96 117	jca	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (−∞ < B \land B < +∞)$
119		xrrebnd	$⊢ B \in ℝ^{*} \to (B \in ℝ \leftrightarrow (−∞ < B \land B < +∞))$
120	91 119	syl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (B \in ℝ \leftrightarrow (−∞ < B \land B < +∞))$
121	118 120	mpbird	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B \in ℝ$
122		simpr	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to sup (A ℝ^{} <) \in ℝ$
123	122	adantr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to sup (A ℝ^{*} <) \in ℝ$
124	121 123	resubcld	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - sup (A ℝ^{*} <) \in ℝ$
125	27 115	mpd	$⊢ φ \to B < +∞$
126	125	ad2antrr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B < +∞$
127	96 126	jca	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (−∞ < B \land B < +∞)$
128	127 120	mpbird	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B \in ℝ$
129	123 128	posdifd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (sup (A ℝ^{} <) < B \leftrightarrow 0 < B - sup (A ℝ^{} <))$
130	95 129	mpbid	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to 0 < B - sup (A ℝ^{*} <)$
131	124 130	elrpd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - sup (A ℝ^{*} <) \in ℝ^{+}$
132		ovex	$⊢ B - sup (A ℝ^{*} <) \in V$
133		nfcv	$⊢ \underline{Ⅎ} x (B - sup (A ℝ^{*} <))$
134		nfv	$⊢ Ⅎ x B - sup (A ℝ^{*} <) \in ℝ^{+}$
135	1 134	nfan	$⊢ Ⅎ x (φ \land B - sup (A ℝ^{*} <) \in ℝ^{+})$
136		nfv	$⊢ Ⅎ x \exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{*} <))$
137	135 136	nfim	$⊢ Ⅎ x ((φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{} <)))$
138		eleq1	$⊢ x = B - sup (A ℝ^{} <) \to (x \in ℝ^{+} \leftrightarrow B - sup (A ℝ^{} <) \in ℝ^{+})$
139	138	anbi2d	$⊢ x = B - sup (A ℝ^{} <) \to ((φ \land x \in ℝ^{+}) \leftrightarrow (φ \land B - sup (A ℝ^{} <) \in ℝ^{+}))$
140		oveq2	$⊢ x = B - sup (A ℝ^{} <) \to y +_{𝑒} x = y +_{𝑒} (B - sup (A ℝ^{} <))$
141	140	breq2d	$⊢ x = B - sup (A ℝ^{} <) \to (B < y +_{𝑒} x \leftrightarrow B < y +_{𝑒} (B - sup (A ℝ^{} <)))$
142	141	rexbidv	$⊢ x = B - sup (A ℝ^{} <) \to (\exists y \in A B < y +_{𝑒} x \leftrightarrow \exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{} <)))$
143	139 142	imbi12d	$⊢ x = B - sup (A ℝ^{} <) \to (((φ \land x \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} x) \leftrightarrow ((φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{*} <))))$
144	133 137 143 4	vtoclgf	$⊢ B - sup (A ℝ^{} <) \in V \to ((φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{*} <)))$
145	132 144	ax-mp	$⊢ (φ \land B - sup (A ℝ^{} <) \in ℝ^{+}) \to \exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{} <))$
146	88 131 145	syl2anc	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to \exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{*} <))$
147		ltpnf	$⊢ sup (A ℝ^{} <) \in ℝ \to sup (A ℝ^{} <) < +∞$
148	147	adantr	$⊢ (sup (A ℝ^{} <) \in ℝ \land y = +∞) \to sup (A ℝ^{} <) < +∞$
149		id	$⊢ y = +∞ \to y = +∞$
150	149	eqcomd	$⊢ y = +∞ \to +∞ = y$
151	150	adantl	$⊢ (sup (A ℝ^{*} <) \in ℝ \land y = +∞) \to +∞ = y$
152	148 151	breqtrd	$⊢ (sup (A ℝ^{} <) \in ℝ \land y = +∞) \to sup (A ℝ^{} <) < y$
153	152	adantll	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land y = +∞) \to sup (A ℝ^{} <) < y$
154	153	ad5ant15	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land y = +∞) \to sup (A ℝ^{} <) < y$
155		simplll	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land \neg y = +∞) \to ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{*} <) < B)$
156		simpl	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land \neg −∞ < y) \to ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <)))$
157	88 41	sylanl1	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land \neg −∞ < y) \to y = −∞$
158	157	adantlr	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg −∞ < y) \to y = −∞$
159		simplr	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land y = −∞) \to B < y +_{𝑒} (B - sup (A ℝ^{} <))$
160		oveq1	$⊢ y = −∞ \to y +_{𝑒} (B - sup (A ℝ^{} <)) = −∞ +_{𝑒} (B - sup (A ℝ^{} <))$
161	160	adantl	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land y = −∞) \to y +_{𝑒} (B - sup (A ℝ^{} <)) = −∞ +_{𝑒} (B - sup (A ℝ^{*} <))$
162	128 123	resubcld	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - sup (A ℝ^{*} <) \in ℝ$
163	162	rexrd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - sup (A ℝ^{} <) \in ℝ^{}$
164	163	ad3antrrr	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land y = −∞) \to B - sup (A ℝ^{} <) \in ℝ^{*}$
165		renepnf	$⊢ B - sup (A ℝ^{} <) \in ℝ \to B - sup (A ℝ^{} <) \neq +∞$
166	124 165	syl	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - sup (A ℝ^{*} <) \neq +∞$
167	166	ad3antrrr	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land y = −∞) \to B - sup (A ℝ^{} <) \neq +∞$
168		xaddmnf2	$⊢ (B - sup (A ℝ^{} <) \in ℝ^{} \land B - sup (A ℝ^{} <) \neq +∞) \to −∞ +_{𝑒} (B - sup (A ℝ^{} <)) = −∞$
169	164 167 168	syl2anc	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land y = −∞) \to −∞ +_{𝑒} (B - sup (A ℝ^{} <)) = −∞$
170	161 169	eqtrd	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land y = −∞) \to y +_{𝑒} (B - sup (A ℝ^{} <)) = −∞$
171	159 170	breqtrd	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land y = −∞) \to B < −∞$
172	156 158 171	syl2anc	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg −∞ < y) \to B < −∞$
173	55	ad5antr	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg −∞ < y) \to \neg B < −∞$
174	172 173	condan	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \to −∞ < y$
175	174	adantr	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg y = +∞) \to −∞ < y$
176		simp3	$⊢ (φ \land y \in A \land \neg y = +∞) \to \neg y = +∞$
177	31	3adant3	$⊢ (φ \land y \in A \land \neg y = +∞) \to y \in ℝ^{*}$
178		nltpnft	$⊢ y \in ℝ^{*} \to (y = +∞ \leftrightarrow \neg y < +∞)$
179	177 178	syl	$⊢ (φ \land y \in A \land \neg y = +∞) \to (y = +∞ \leftrightarrow \neg y < +∞)$
180	176 179	mtbid	$⊢ (φ \land y \in A \land \neg y = +∞) \to \neg \neg y < +∞$
181	180	notnotrd	$⊢ (φ \land y \in A \land \neg y = +∞) \to y < +∞$
182	181	3adant1r	$⊢ ((φ \land sup (A ℝ^{*} <) \in ℝ) \land y \in A \land \neg y = +∞) \to y < +∞$
183	182	ad5ant135	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg y = +∞) \to y < +∞$
184	175 183	jca	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg y = +∞) \to (−∞ < y \land y < +∞)$
185	31	adantlr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land y \in A) \to y \in ℝ^{}$
186	185	ad5ant13	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land \neg y = +∞) \to y \in ℝ^{}$
187		xrrebnd	$⊢ y \in ℝ^{*} \to (y \in ℝ \leftrightarrow (−∞ < y \land y < +∞))$
188	186 187	syl	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg y = +∞) \to (y \in ℝ \leftrightarrow (−∞ < y \land y < +∞))$
189	184 188	mpbird	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \land \neg y = +∞) \to y \in ℝ$
190		simplr	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land \neg y = +∞) \to B < y +_{𝑒} (B - sup (A ℝ^{} <))$
191	121	ad2antrr	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \to B \in ℝ$
192		simpr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y \in ℝ$
193	124	adantr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to B - sup (A ℝ^{*} <) \in ℝ$
194		rexadd	$⊢ (y \in ℝ \land B - sup (A ℝ^{} <) \in ℝ) \to y +_{𝑒} (B - sup (A ℝ^{} <)) = y + B - sup (A ℝ^{*} <)$
195	192 193 194	syl2anc	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y +_{𝑒} (B - sup (A ℝ^{} <)) = y + B - sup (A ℝ^{} <)$
196	192 193	readdcld	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y + B - sup (A ℝ^{*} <) \in ℝ$
197	195 196	eqeltrd	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y +_{𝑒} (B - sup (A ℝ^{*} <)) \in ℝ$
198	197	adantr	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to y +_{𝑒} (B - sup (A ℝ^{} <)) \in ℝ$
199		simpr	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to B < y +_{𝑒} (B - sup (A ℝ^{} <))$
200	191 198 191 199	ltsub1dd	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to B - B < (y +_{𝑒} (B - sup (A ℝ^{} <))) - B$
201	121	recnd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B \in ℂ$
202	201	subidd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to B - B = 0$
203	202	ad2antrr	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \to B - B = 0$
204	201	adantr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to B \in ℂ$
205	192	recnd	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y \in ℂ$
206	122	recnd	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to sup (A ℝ^{} <) \in ℂ$
207	206	ad2antrr	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to sup (A ℝ^{*} <) \in ℂ$
208	205 207	subcld	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y - sup (A ℝ^{*} <) \in ℂ$
209	205 204 207	addsub12d	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y + B - sup (A ℝ^{} <) = B + y - sup (A ℝ^{} <)$
210	195 209	eqtrd	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to y +_{𝑒} (B - sup (A ℝ^{} <)) = B + y - sup (A ℝ^{} <)$
211	204 208 210	mvrladdd	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \to (y +_{𝑒} (B - sup (A ℝ^{} <))) - B = y - sup (A ℝ^{} <)$
212	211	adantr	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to (y +_{𝑒} (B - sup (A ℝ^{} <))) - B = y - sup (A ℝ^{*} <)$
213	203 212	breq12d	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to (B - B < (y +_{𝑒} (B - sup (A ℝ^{} <))) - B \leftrightarrow 0 < y - sup (A ℝ^{*} <))$
214	200 213	mpbid	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to 0 < y - sup (A ℝ^{} <)$
215	123	ad2antrr	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to sup (A ℝ^{} <) \in ℝ$
216		simplr	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{*} <))) \to y \in ℝ$
217	215 216	posdifd	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to (sup (A ℝ^{} <) < y \leftrightarrow 0 < y - sup (A ℝ^{*} <))$
218	214 217	mpbird	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in ℝ) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to sup (A ℝ^{} <) < y$
219	155 189 190 218	syl21anc	$⊢ (((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \land \neg y = +∞) \to sup (A ℝ^{} <) < y$
220	154 219	pm2.61dan	$⊢ ((((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \land B < y +_{𝑒} (B - sup (A ℝ^{} <))) \to sup (A ℝ^{} <) < y$
221	220	ex	$⊢ (((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \land y \in A) \to (B < y +_{𝑒} (B - sup (A ℝ^{} <)) \to sup (A ℝ^{} <) < y)$
222	221	reximdva	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to (\exists y \in A B < y +_{𝑒} (B - sup (A ℝ^{} <)) \to \exists y \in A sup (A ℝ^{} <) < y)$
223	146 222	mpd	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land sup (A ℝ^{} <) < B) \to \exists y \in A sup (A ℝ^{*} <) < y$
224	80 87 223	syl2anc	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to \exists y \in A sup (A ℝ^{*} <) < y$
225	59 33	syl	$⊢ (φ \land y \in A) \to sup (A ℝ^{} <) \in ℝ^{}$
226	31 225	xrlenltd	$⊢ (φ \land y \in A) \to (y \leq sup (A ℝ^{} <) \leftrightarrow \neg sup (A ℝ^{} <) < y)$
227	62 226	mpbid	$⊢ (φ \land y \in A) \to \neg sup (A ℝ^{*} <) < y$
228	227	ralrimiva	$⊢ φ \to \forall y \in A \neg sup (A ℝ^{*} <) < y$
229		ralnex	$⊢ \forall y \in A \neg sup (A ℝ^{} <) < y \leftrightarrow \neg \exists y \in A sup (A ℝ^{} <) < y$
230	228 229	sylib	$⊢ φ \to \neg \exists y \in A sup (A ℝ^{*} <) < y$
231	230	ad2antrr	$⊢ ((φ \land sup (A ℝ^{} <) \in ℝ) \land \neg B \leq sup (A ℝ^{} <)) \to \neg \exists y \in A sup (A ℝ^{*} <) < y$
232	224 231	condan	$⊢ (φ \land sup (A ℝ^{} <) \in ℝ) \to B \leq sup (A ℝ^{} <)$
233	12 79 232	syl2anc	$⊢ (φ \land \neg sup (A ℝ^{} <) = +∞) \to B \leq sup (A ℝ^{} <)$
234	11 233	pm2.61dan	$⊢ φ \to B \leq sup (A ℝ^{*} <)$

Metamath Proof Explorer

Theorem supxrgelem

Proof