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 φ A *
infleinflem1.b φ B *
infleinflem1.w φ W +
infleinflem1.x φ X B
infleinflem1.i φ X inf B * < + 𝑒 W 2
infleinflem1.z φ Z A
infleinflem1.l φ Z X + 𝑒 W 2
Assertion infleinflem1 φ inf A * < inf B * < + 𝑒 W

Proof

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