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 
|- ( ph -> A C_ RR* )
infleinflem1.b 
|- ( ph -> B C_ RR* )
infleinflem1.w 
|- ( ph -> W e. RR+ )
infleinflem1.x 
|- ( ph -> X e. B )
infleinflem1.i 
|- ( ph -> X <_ ( inf ( B , RR* , < ) +e ( W / 2 ) ) )
infleinflem1.z 
|- ( ph -> Z e. A )
infleinflem1.l 
|- ( ph -> Z <_ ( X +e ( W / 2 ) ) )
Assertion infleinflem1 
|- ( ph -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e W ) )

Proof

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