This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ( 𝐴 , ℝ* , < ) +𝑒 𝐵 ) )