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	⊢ Ⅎ 𝑥 𝜑
	infrpge.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
	infrpge.an0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	infrpge.bnd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
	infrpge.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
Assertion	infrpge	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐴 𝑧 ≤ ( inf ( 𝐴 , ℝ^* , < ) +_𝑒 𝐵 ) )

Proof

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

Metamath Proof Explorer

Theorem infrpge

Proof