Metamath Proof Explorer

Theorem infleinflem1

Description: Lemma for infleinf , case B =/= (/) /\ -oo < inf ( B , RR* , < ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses infleinflem1.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
infleinflem1.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
infleinflem1.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ+ )
infleinflem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
infleinflem1.i ⊢ ( 𝜑 → 𝑋 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) )
infleinflem1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
infleinflem1.l ⊢ ( 𝜑 → 𝑍 ≤ ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) )
Assertion infleinflem1 ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )

Proof

Step Hyp Ref Expression
1 infleinflem1.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
2 infleinflem1.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
3 infleinflem1.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ+ )
4 infleinflem1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 infleinflem1.i ⊢ ( 𝜑 → 𝑋 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) )
6 infleinflem1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
7 infleinflem1.l ⊢ ( 𝜑 → 𝑍 ≤ ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) )
8 infxrcl ⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
9 1 8 syl ⊢ ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
10 id ⊢ ( inf ( 𝐴 , ℝ* , < ) ∈ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
11 9 10 syl ⊢ ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
12 1 6 sseldd ⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
13 infxrcl ⊢ ( 𝐵 ⊆ ℝ* → inf ( 𝐵 , ℝ* , < ) ∈ ℝ* )
14 2 13 syl ⊢ ( 𝜑 → inf ( 𝐵 , ℝ* , < ) ∈ ℝ* )
15 rpxr ⊢ ( 𝑊 ∈ ℝ+ → 𝑊 ∈ ℝ* )
16 3 15 syl ⊢ ( 𝜑 → 𝑊 ∈ ℝ* )
17 14 16 xaddcld ⊢ ( 𝜑 → ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) ∈ ℝ* )
18 infxrlb ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑍 ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑍 )
19 1 6 18 syl2anc ⊢ ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ 𝑍 )
20 2 sselda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ℝ* )
21 4 20 mpdan ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
22 3 rpred ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
23 22 rehalfcld ⊢ ( 𝜑 → ( 𝑊 / 2 ) ∈ ℝ )
24 23 rexrd ⊢ ( 𝜑 → ( 𝑊 / 2 ) ∈ ℝ* )
25 21 24 xaddcld ⊢ ( 𝜑 → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ∈ ℝ* )
26 pnfge ⊢ ( ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ∈ ℝ* → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ +∞ )
27 25 26 syl ⊢ ( 𝜑 → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ +∞ )
28 27 adantr ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ +∞ )
29 oveq1 ⊢ ( inf ( 𝐵 , ℝ* , < ) = +∞ → ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) = ( +∞ +𝑒 𝑊 ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) = ( +∞ +𝑒 𝑊 ) )
31 rpre ⊢ ( 𝑊 ∈ ℝ+ → 𝑊 ∈ ℝ )
32 renemnf ⊢ ( 𝑊 ∈ ℝ → 𝑊 ≠ -∞ )
33 31 32 syl ⊢ ( 𝑊 ∈ ℝ+ → 𝑊 ≠ -∞ )
34 xaddpnf2 ⊢ ( ( 𝑊 ∈ ℝ* ∧ 𝑊 ≠ -∞ ) → ( +∞ +𝑒 𝑊 ) = +∞ )
35 15 33 34 syl2anc ⊢ ( 𝑊 ∈ ℝ+ → ( +∞ +𝑒 𝑊 ) = +∞ )
36 3 35 syl ⊢ ( 𝜑 → ( +∞ +𝑒 𝑊 ) = +∞ )
37 36 adantr ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( +∞ +𝑒 𝑊 ) = +∞ )
38 30 37 eqtr2d ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = +∞ ) → +∞ = ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
39 28 38 breqtrd ⊢ ( ( 𝜑 ∧ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
40 2 4 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
41 14 24 xaddcld ⊢ ( 𝜑 → ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) ∈ ℝ* )
42 rphalfcl ⊢ ( 𝑊 ∈ ℝ+ → ( 𝑊 / 2 ) ∈ ℝ+ )
43 3 42 syl ⊢ ( 𝜑 → ( 𝑊 / 2 ) ∈ ℝ+ )
44 43 rpxrd ⊢ ( 𝜑 → ( 𝑊 / 2 ) ∈ ℝ* )
45 40 41 44 5 xleadd1d ⊢ ( 𝜑 → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ ( ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) +𝑒 ( 𝑊 / 2 ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ ( ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) +𝑒 ( 𝑊 / 2 ) ) )
47 14 adantr ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → inf ( 𝐵 , ℝ* , < ) ∈ ℝ* )
48 neqne ⊢ ( ¬ inf ( 𝐵 , ℝ* , < ) = +∞ → inf ( 𝐵 , ℝ* , < ) ≠ +∞ )
49 48 adantl ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → inf ( 𝐵 , ℝ* , < ) ≠ +∞ )
50 44 adantr ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( 𝑊 / 2 ) ∈ ℝ* )
51 3 adantr ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → 𝑊 ∈ ℝ+ )
52 rpre ⊢ ( ( 𝑊 / 2 ) ∈ ℝ+ → ( 𝑊 / 2 ) ∈ ℝ )
53 renepnf ⊢ ( ( 𝑊 / 2 ) ∈ ℝ → ( 𝑊 / 2 ) ≠ +∞ )
54 51 42 52 53 4syl ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( 𝑊 / 2 ) ≠ +∞ )
55 xaddass2 ⊢ ( ( ( inf ( 𝐵 , ℝ* , < ) ∈ ℝ* ∧ inf ( 𝐵 , ℝ* , < ) ≠ +∞ ) ∧ ( ( 𝑊 / 2 ) ∈ ℝ* ∧ ( 𝑊 / 2 ) ≠ +∞ ) ∧ ( ( 𝑊 / 2 ) ∈ ℝ* ∧ ( 𝑊 / 2 ) ≠ +∞ ) ) → ( ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) +𝑒 ( 𝑊 / 2 ) ) = ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( ( 𝑊 / 2 ) +𝑒 ( 𝑊 / 2 ) ) ) )
56 47 49 50 54 50 54 55 syl222anc ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) +𝑒 ( 𝑊 / 2 ) ) = ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( ( 𝑊 / 2 ) +𝑒 ( 𝑊 / 2 ) ) ) )
57 rehalfcl ⊢ ( 𝑊 ∈ ℝ → ( 𝑊 / 2 ) ∈ ℝ )
58 57 57 rexaddd ⊢ ( 𝑊 ∈ ℝ → ( ( 𝑊 / 2 ) +𝑒 ( 𝑊 / 2 ) ) = ( ( 𝑊 / 2 ) + ( 𝑊 / 2 ) ) )
59 recn ⊢ ( 𝑊 ∈ ℝ → 𝑊 ∈ ℂ )
60 2halves ⊢ ( 𝑊 ∈ ℂ → ( ( 𝑊 / 2 ) + ( 𝑊 / 2 ) ) = 𝑊 )
61 59 60 syl ⊢ ( 𝑊 ∈ ℝ → ( ( 𝑊 / 2 ) + ( 𝑊 / 2 ) ) = 𝑊 )
62 58 61 eqtrd ⊢ ( 𝑊 ∈ ℝ → ( ( 𝑊 / 2 ) +𝑒 ( 𝑊 / 2 ) ) = 𝑊 )
63 62 oveq2d ⊢ ( 𝑊 ∈ ℝ → ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( ( 𝑊 / 2 ) +𝑒 ( 𝑊 / 2 ) ) ) = ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
64 51 31 63 3syl ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( ( 𝑊 / 2 ) +𝑒 ( 𝑊 / 2 ) ) ) = ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
65 56 64 eqtrd ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( ( inf ( 𝐵 , ℝ* , < ) +𝑒 ( 𝑊 / 2 ) ) +𝑒 ( 𝑊 / 2 ) ) = ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
66 46 65 breqtrd ⊢ ( ( 𝜑 ∧ ¬ inf ( 𝐵 , ℝ* , < ) = +∞ ) → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
67 39 66 pm2.61dan ⊢ ( 𝜑 → ( 𝑋 +𝑒 ( 𝑊 / 2 ) ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
68 12 25 17 7 67 xrletrd ⊢ ( 𝜑 → 𝑍 ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )
69 11 12 17 19 68 xrletrd ⊢ ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ ( inf ( 𝐵 , ℝ* , < ) +𝑒 𝑊 ) )