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 42 52 53 3syl 
 |-  ( W e. RR+ -> ( W / 2 ) =/= +oo )
55 51 54 syl 
 |-  ( ( ph /\ -. inf ( B , RR* , < ) = +oo ) -> ( W / 2 ) =/= +oo )
56 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 ) ) ) )
57 47 49 50 55 50 55 56 syl222anc 
 |-  ( ( ph /\ -. inf ( B , RR* , < ) = +oo ) -> ( ( inf ( B , RR* , < ) +e ( W / 2 ) ) +e ( W / 2 ) ) = ( inf ( B , RR* , < ) +e ( ( W / 2 ) +e ( W / 2 ) ) ) )
58 rehalfcl 
 |-  ( W e. RR -> ( W / 2 ) e. RR )
59 58 58 rexaddd 
 |-  ( W e. RR -> ( ( W / 2 ) +e ( W / 2 ) ) = ( ( W / 2 ) + ( W / 2 ) ) )
60 recn 
 |-  ( W e. RR -> W e. CC )
61 2halves 
 |-  ( W e. CC -> ( ( W / 2 ) + ( W / 2 ) ) = W )
62 60 61 syl 
 |-  ( W e. RR -> ( ( W / 2 ) + ( W / 2 ) ) = W )
63 59 62 eqtrd 
 |-  ( W e. RR -> ( ( W / 2 ) +e ( W / 2 ) ) = W )
64 63 oveq2d 
 |-  ( W e. RR -> ( inf ( B , RR* , < ) +e ( ( W / 2 ) +e ( W / 2 ) ) ) = ( inf ( B , RR* , < ) +e W ) )
65 51 31 64 3syl 
 |-  ( ( ph /\ -. inf ( B , RR* , < ) = +oo ) -> ( inf ( B , RR* , < ) +e ( ( W / 2 ) +e ( W / 2 ) ) ) = ( inf ( B , RR* , < ) +e W ) )
66 57 65 eqtrd 
 |-  ( ( ph /\ -. inf ( B , RR* , < ) = +oo ) -> ( ( inf ( B , RR* , < ) +e ( W / 2 ) ) +e ( W / 2 ) ) = ( inf ( B , RR* , < ) +e W ) )
67 46 66 breqtrd 
 |-  ( ( ph /\ -. inf ( B , RR* , < ) = +oo ) -> ( X +e ( W / 2 ) ) <_ ( inf ( B , RR* , < ) +e W ) )
68 39 67 pm2.61dan 
 |-  ( ph -> ( X +e ( W / 2 ) ) <_ ( inf ( B , RR* , < ) +e W ) )
69 12 25 17 7 68 xrletrd 
 |-  ( ph -> Z <_ ( inf ( B , RR* , < ) +e W ) )
70 11 12 17 19 69 xrletrd 
 |-  ( ph -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e W ) )