infrpge

Description: The infimum of a nonempty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	infrpge.xph	$⊢ Ⅎ x φ$
	infrpge.a	$⊢ φ \to A \subseteq ℝ^{*}$
	infrpge.an0	$⊢ φ \to A \neq \emptyset$
	infrpge.bnd	$⊢ φ \to \exists x \in ℝ \forall y \in A x \leq y$
	infrpge.b	$⊢ φ \to B \in ℝ^{+}$
Assertion	infrpge	$⊢ φ \to \exists z \in A z \leq inf (A ℝ^{*} <) +_{𝑒} B$

Proof

Step	Hyp	Ref	Expression
1		infrpge.xph	$⊢ Ⅎ x φ$
2		infrpge.a	$⊢ φ \to A \subseteq ℝ^{*}$
3		infrpge.an0	$⊢ φ \to A \neq \emptyset$
4		infrpge.bnd	$⊢ φ \to \exists x \in ℝ \forall y \in A x \leq y$
5		infrpge.b	$⊢ φ \to B \in ℝ^{+}$
6		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
7	6	biimpi	$⊢ A \neq \emptyset \to \exists z z \in A$
8	3 7	syl	$⊢ φ \to \exists z z \in A$
9	8	adantr	$⊢ (φ \land inf (A ℝ^{*} <) = +∞) \to \exists z z \in A$
10		nfv	$⊢ Ⅎ z (φ \land inf (A ℝ^{*} <) = +∞)$
11		simpr	$⊢ ((φ \land inf (A ℝ^{*} <) = +∞) \land z \in A) \to z \in A$
12	2	adantr	$⊢ (φ \land z \in A) \to A \subseteq ℝ^{*}$
13		simpr	$⊢ (φ \land z \in A) \to z \in A$
14	12 13	sseldd	$⊢ (φ \land z \in A) \to z \in ℝ^{*}$
15		pnfge	$⊢ z \in ℝ^{*} \to z \leq +∞$
16	14 15	syl	$⊢ (φ \land z \in A) \to z \leq +∞$
17	16	adantlr	$⊢ ((φ \land inf (A ℝ^{*} <) = +∞) \land z \in A) \to z \leq +∞$
18		oveq1	$⊢ inf (A ℝ^{} <) = +∞ \to inf (A ℝ^{} <) +_{𝑒} B = +∞ +_{𝑒} B$
19	18	adantl	$⊢ (φ \land inf (A ℝ^{} <) = +∞) \to inf (A ℝ^{} <) +_{𝑒} B = +∞ +_{𝑒} B$
20	5	rpxrd	$⊢ φ \to B \in ℝ^{*}$
21	5	rpred	$⊢ φ \to B \in ℝ$
22		renemnf	$⊢ B \in ℝ \to B \neq −∞$
23	21 22	syl	$⊢ φ \to B \neq −∞$
24		xaddpnf2	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to +∞ +_{𝑒} B = +∞$
25	20 23 24	syl2anc	$⊢ φ \to +∞ +_{𝑒} B = +∞$
26	25	adantr	$⊢ (φ \land inf (A ℝ^{*} <) = +∞) \to +∞ +_{𝑒} B = +∞$
27	19 26	eqtr2d	$⊢ (φ \land inf (A ℝ^{} <) = +∞) \to +∞ = inf (A ℝ^{} <) +_{𝑒} B$
28	27	adantr	$⊢ ((φ \land inf (A ℝ^{} <) = +∞) \land z \in A) \to +∞ = inf (A ℝ^{} <) +_{𝑒} B$
29	17 28	breqtrd	$⊢ ((φ \land inf (A ℝ^{} <) = +∞) \land z \in A) \to z \leq inf (A ℝ^{} <) +_{𝑒} B$
30	11 29	jca	$⊢ ((φ \land inf (A ℝ^{} <) = +∞) \land z \in A) \to (z \in A \land z \leq inf (A ℝ^{} <) +_{𝑒} B)$
31	30	ex	$⊢ (φ \land inf (A ℝ^{} <) = +∞) \to (z \in A \to (z \in A \land z \leq inf (A ℝ^{} <) +_{𝑒} B))$
32	10 31	eximd	$⊢ (φ \land inf (A ℝ^{} <) = +∞) \to (\exists z z \in A \to \exists z (z \in A \land z \leq inf (A ℝ^{} <) +_{𝑒} B))$
33	9 32	mpd	$⊢ (φ \land inf (A ℝ^{} <) = +∞) \to \exists z (z \in A \land z \leq inf (A ℝ^{} <) +_{𝑒} B)$
34		df-rex	$⊢ \exists z \in A z \leq inf (A ℝ^{} <) +_{𝑒} B \leftrightarrow \exists z (z \in A \land z \leq inf (A ℝ^{} <) +_{𝑒} B)$
35	33 34	sylibr	$⊢ (φ \land inf (A ℝ^{} <) = +∞) \to \exists z \in A z \leq inf (A ℝ^{} <) +_{𝑒} B$
36		simpl	$⊢ (φ \land \neg inf (A ℝ^{*} <) = +∞) \to φ$
37		nfv	$⊢ Ⅎ x −∞ < inf (A ℝ^{*} <)$
38		mnfxr	$⊢ −∞ \in ℝ^{*}$
39	38	a1i	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to −∞ \in ℝ^{*}$
40		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
41	40	3ad2ant2	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to x \in ℝ^{*}$
42		infxrcl	$⊢ A \subseteq ℝ^{} \to inf (A ℝ^{} <) \in ℝ^{*}$
43	2 42	syl	$⊢ φ \to inf (A ℝ^{} <) \in ℝ^{}$
44	43	3ad2ant1	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to inf (A ℝ^{} <) \in ℝ^{}$
45		mnflt	$⊢ x \in ℝ \to −∞ < x$
46	45	3ad2ant2	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to −∞ < x$
47		simp3	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to \forall y \in A x \leq y$
48	2	adantr	$⊢ (φ \land x \in ℝ) \to A \subseteq ℝ^{*}$
49	40	adantl	$⊢ (φ \land x \in ℝ) \to x \in ℝ^{*}$
50		infxrgelb	$⊢ (A \subseteq ℝ^{} \land x \in ℝ^{}) \to (x \leq inf (A ℝ^{*} <) \leftrightarrow \forall y \in A x \leq y)$
51	48 49 50	syl2anc	$⊢ (φ \land x \in ℝ) \to (x \leq inf (A ℝ^{*} <) \leftrightarrow \forall y \in A x \leq y)$
52	51	3adant3	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to (x \leq inf (A ℝ^{*} <) \leftrightarrow \forall y \in A x \leq y)$
53	47 52	mpbird	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to x \leq inf (A ℝ^{*} <)$
54	39 41 44 46 53	xrltletrd	$⊢ (φ \land x \in ℝ \land \forall y \in A x \leq y) \to −∞ < inf (A ℝ^{*} <)$
55	54	3exp	$⊢ φ \to (x \in ℝ \to (\forall y \in A x \leq y \to −∞ < inf (A ℝ^{*} <)))$
56	1 37 55	rexlimd	$⊢ φ \to (\exists x \in ℝ \forall y \in A x \leq y \to −∞ < inf (A ℝ^{*} <))$
57	4 56	mpd	$⊢ φ \to −∞ < inf (A ℝ^{*} <)$
58	57	adantr	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to −∞ < inf (A ℝ^{} <)$
59		neqne	$⊢ \neg inf (A ℝ^{} <) = +∞ \to inf (A ℝ^{} <) \neq +∞$
60	59	adantl	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to inf (A ℝ^{} <) \neq +∞$
61	43	adantr	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to inf (A ℝ^{} <) \in ℝ^{*}$
62	60 61	nepnfltpnf	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to inf (A ℝ^{} <) < +∞$
63	58 62	jca	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to (−∞ < inf (A ℝ^{} <) \land inf (A ℝ^{*} <) < +∞)$
64		xrrebnd	$⊢ inf (A ℝ^{} <) \in ℝ^{} \to (inf (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < inf (A ℝ^{} <) \land inf (A ℝ^{*} <) < +∞))$
65	43 64	syl	$⊢ φ \to (inf (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < inf (A ℝ^{} <) \land inf (A ℝ^{*} <) < +∞))$
66	65	adantr	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to (inf (A ℝ^{} <) \in ℝ \leftrightarrow (−∞ < inf (A ℝ^{} <) \land inf (A ℝ^{} <) < +∞))$
67	63 66	mpbird	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to inf (A ℝ^{} <) \in ℝ$
68		simpr	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to inf (A ℝ^{} <) \in ℝ$
69	5	adantr	$⊢ (φ \land inf (A ℝ^{*} <) \in ℝ) \to B \in ℝ^{+}$
70	68 69	ltaddrpd	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to inf (A ℝ^{} <) < inf (A ℝ^{*} <) + B$
71	21	adantr	$⊢ (φ \land inf (A ℝ^{*} <) \in ℝ) \to B \in ℝ$
72		rexadd	$⊢ (inf (A ℝ^{} <) \in ℝ \land B \in ℝ) \to inf (A ℝ^{} <) +_{𝑒} B = inf (A ℝ^{*} <) + B$
73	68 71 72	syl2anc	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to inf (A ℝ^{} <) +_{𝑒} B = inf (A ℝ^{*} <) + B$
74	73	eqcomd	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to inf (A ℝ^{} <) + B = inf (A ℝ^{*} <) +_{𝑒} B$
75	70 74	breqtrd	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to inf (A ℝ^{} <) < inf (A ℝ^{*} <) +_{𝑒} B$
76	43	adantr	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to inf (A ℝ^{} <) \in ℝ^{*}$
77	43 20	xaddcld	$⊢ φ \to inf (A ℝ^{} <) +_{𝑒} B \in ℝ^{}$
78	77	adantr	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to inf (A ℝ^{} <) +_{𝑒} B \in ℝ^{*}$
79		xrltnle	$⊢ (inf (A ℝ^{} <) \in ℝ^{} \land inf (A ℝ^{} <) +_{𝑒} B \in ℝ^{}) \to (inf (A ℝ^{} <) < inf (A ℝ^{} <) +_{𝑒} B \leftrightarrow \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <))$
80	76 78 79	syl2anc	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to (inf (A ℝ^{} <) < inf (A ℝ^{} <) +_{𝑒} B \leftrightarrow \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{*} <))$
81	75 80	mpbid	$⊢ (φ \land inf (A ℝ^{} <) \in ℝ) \to \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{*} <)$
82	36 67 81	syl2anc	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{*} <)$
83		simpr	$⊢ (φ \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <)) \to \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <)$
84		simpl	$⊢ (φ \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <)) \to φ$
85		infxrgelb	$⊢ (A \subseteq ℝ^{} \land inf (A ℝ^{} <) +_{𝑒} B \in ℝ^{}) \to (inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <) \leftrightarrow \forall z \in A inf (A ℝ^{} <) +_{𝑒} B \leq z)$
86	2 77 85	syl2anc	$⊢ φ \to (inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <) \leftrightarrow \forall z \in A inf (A ℝ^{*} <) +_{𝑒} B \leq z)$
87	84 86	syl	$⊢ (φ \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <)) \to (inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <) \leftrightarrow \forall z \in A inf (A ℝ^{*} <) +_{𝑒} B \leq z)$
88	83 87	mtbid	$⊢ (φ \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <)) \to \neg \forall z \in A inf (A ℝ^{*} <) +_{𝑒} B \leq z$
89		rexnal	$⊢ \exists z \in A \neg inf (A ℝ^{} <) +_{𝑒} B \leq z \leftrightarrow \neg \forall z \in A inf (A ℝ^{} <) +_{𝑒} B \leq z$
90	88 89	sylibr	$⊢ (φ \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq inf (A ℝ^{} <)) \to \exists z \in A \neg inf (A ℝ^{*} <) +_{𝑒} B \leq z$
91	36 82 90	syl2anc	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to \exists z \in A \neg inf (A ℝ^{} <) +_{𝑒} B \leq z$
92	14	adantr	$⊢ ((φ \land z \in A) \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq z) \to z \in ℝ^{}$
93	77	ad2antrr	$⊢ ((φ \land z \in A) \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq z) \to inf (A ℝ^{} <) +_{𝑒} B \in ℝ^{*}$
94		simpr	$⊢ ((φ \land z \in A) \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq z) \to \neg inf (A ℝ^{} <) +_{𝑒} B \leq z$
95		xrltnle	$⊢ (z \in ℝ^{} \land inf (A ℝ^{} <) +_{𝑒} B \in ℝ^{}) \to (z < inf (A ℝ^{} <) +_{𝑒} B \leftrightarrow \neg inf (A ℝ^{*} <) +_{𝑒} B \leq z)$
96	92 93 95	syl2anc	$⊢ ((φ \land z \in A) \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq z) \to (z < inf (A ℝ^{} <) +_{𝑒} B \leftrightarrow \neg inf (A ℝ^{*} <) +_{𝑒} B \leq z)$
97	94 96	mpbird	$⊢ ((φ \land z \in A) \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq z) \to z < inf (A ℝ^{} <) +_{𝑒} B$
98	92 93 97	xrltled	$⊢ ((φ \land z \in A) \land \neg inf (A ℝ^{} <) +_{𝑒} B \leq z) \to z \leq inf (A ℝ^{} <) +_{𝑒} B$
99	98	ex	$⊢ (φ \land z \in A) \to (\neg inf (A ℝ^{} <) +_{𝑒} B \leq z \to z \leq inf (A ℝ^{} <) +_{𝑒} B)$
100	99	adantlr	$⊢ ((φ \land \neg inf (A ℝ^{} <) = +∞) \land z \in A) \to (\neg inf (A ℝ^{} <) +_{𝑒} B \leq z \to z \leq inf (A ℝ^{*} <) +_{𝑒} B)$
101	100	reximdva	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to (\exists z \in A \neg inf (A ℝ^{} <) +_{𝑒} B \leq z \to \exists z \in A z \leq inf (A ℝ^{*} <) +_{𝑒} B)$
102	91 101	mpd	$⊢ (φ \land \neg inf (A ℝ^{} <) = +∞) \to \exists z \in A z \leq inf (A ℝ^{} <) +_{𝑒} B$
103	35 102	pm2.61dan	$⊢ φ \to \exists z \in A z \leq inf (A ℝ^{*} <) +_{𝑒} B$

Metamath Proof Explorer

Theorem infrpge

Proof