Metamath Proof Explorer

Theorem xrlexaddrp

Description: If an extended real number A can be approximated from above, adding positive reals to B , then A is less than or equal to B . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses xrlexaddrp.1 
|- ( ph -> A e. RR* )
xrlexaddrp.2 
|- ( ph -> B e. RR* )
xrlexaddrp.3 
|- ( ( ph /\ x e. RR+ ) -> A <_ ( B +e x ) )
Assertion xrlexaddrp 
|- ( ph -> A <_ B )

Proof

Step Hyp Ref Expression
1 xrlexaddrp.1 
 |-  ( ph -> A e. RR* )
2 xrlexaddrp.2 
 |-  ( ph -> B e. RR* )
3 xrlexaddrp.3 
 |-  ( ( ph /\ x e. RR+ ) -> A <_ ( B +e x ) )
4 pnfge 
 |-  ( A e. RR* -> A <_ +oo )
5 1 4 syl 
 |-  ( ph -> A <_ +oo )
6 5 adantr 
 |-  ( ( ph /\ B = +oo ) -> A <_ +oo )
7 id 
 |-  ( B = +oo -> B = +oo )
8 7 eqcomd 
 |-  ( B = +oo -> +oo = B )
9 8 adantl 
 |-  ( ( ph /\ B = +oo ) -> +oo = B )
10 6 9 breqtrd 
 |-  ( ( ph /\ B = +oo ) -> A <_ B )
11 simpl 
 |-  ( ( ph /\ -. B = +oo ) -> ph )
12 neqne 
 |-  ( -. B = +oo -> B =/= +oo )
13 12 adantl 
 |-  ( ( ph /\ -. B = +oo ) -> B =/= +oo )
14 simpr 
 |-  ( ( ph /\ A = -oo ) -> A = -oo )
15 mnfle 
 |-  ( B e. RR* -> -oo <_ B )
16 2 15 syl 
 |-  ( ph -> -oo <_ B )
17 16 adantr 
 |-  ( ( ph /\ A = -oo ) -> -oo <_ B )
18 14 17 eqbrtrd 
 |-  ( ( ph /\ A = -oo ) -> A <_ B )
19 18 adantlr 
 |-  ( ( ( ph /\ B =/= +oo ) /\ A = -oo ) -> A <_ B )
20 simpl 
 |-  ( ( ( ph /\ B =/= +oo ) /\ -. A = -oo ) -> ( ph /\ B =/= +oo ) )
21 neqne 
 |-  ( -. A = -oo -> A =/= -oo )
22 21 adantl 
 |-  ( ( ( ph /\ B =/= +oo ) /\ -. A = -oo ) -> A =/= -oo )
23 simpll 
 |-  ( ( ( ph /\ B =/= +oo ) /\ A =/= -oo ) -> ph )
24 2 adantr 
 |-  ( ( ph /\ B =/= +oo ) -> B e. RR* )
25 simpr 
 |-  ( ( ph /\ B =/= +oo ) -> B =/= +oo )
26 24 25 jca 
 |-  ( ( ph /\ B =/= +oo ) -> ( B e. RR* /\ B =/= +oo ) )
27 xrnepnf 
 |-  ( ( B e. RR* /\ B =/= +oo ) <-> ( B e. RR \/ B = -oo ) )
28 26 27 sylib 
 |-  ( ( ph /\ B =/= +oo ) -> ( B e. RR \/ B = -oo ) )
29 28 adantr 
 |-  ( ( ( ph /\ B =/= +oo ) /\ -. B e. RR ) -> ( B e. RR \/ B = -oo ) )
30 simpr 
 |-  ( ( ( ph /\ B =/= +oo ) /\ -. B e. RR ) -> -. B e. RR )
31 pm2.53 
 |-  ( ( B e. RR \/ B = -oo ) -> ( -. B e. RR -> B = -oo ) )
32 29 30 31 sylc 
 |-  ( ( ( ph /\ B =/= +oo ) /\ -. B e. RR ) -> B = -oo )
33 32 adantlr 
 |-  ( ( ( ( ph /\ B =/= +oo ) /\ A =/= -oo ) /\ -. B e. RR ) -> B = -oo )
34 id 
 |-  ( ph -> ph )
35 1rp 
 |-  1 e. RR+
36 35 a1i 
 |-  ( ph -> 1 e. RR+ )
37 1re 
 |-  1 e. RR
38 37 elexi 
 |-  1 e. _V
39 eleq1 
 |-  ( x = 1 -> ( x e. RR+ <-> 1 e. RR+ ) )
40 39 anbi2d 
 |-  ( x = 1 -> ( ( ph /\ x e. RR+ ) <-> ( ph /\ 1 e. RR+ ) ) )
41 oveq2 
 |-  ( x = 1 -> ( B +e x ) = ( B +e 1 ) )
42 41 breq2d 
 |-  ( x = 1 -> ( A <_ ( B +e x ) <-> A <_ ( B +e 1 ) ) )
43 40 42 imbi12d 
 |-  ( x = 1 -> ( ( ( ph /\ x e. RR+ ) -> A <_ ( B +e x ) ) <-> ( ( ph /\ 1 e. RR+ ) -> A <_ ( B +e 1 ) ) ) )
44 38 43 3 vtocl 
 |-  ( ( ph /\ 1 e. RR+ ) -> A <_ ( B +e 1 ) )
45 34 36 44 syl2anc 
 |-  ( ph -> A <_ ( B +e 1 ) )
46 45 ad2antrr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> A <_ ( B +e 1 ) )
47 oveq1 
 |-  ( B = -oo -> ( B +e 1 ) = ( -oo +e 1 ) )
48 1xr 
 |-  1 e. RR*
49 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
50 37 49 ax-mp 
 |-  1 < +oo
51 37 50 ltneii 
 |-  1 =/= +oo
52 xaddmnf2 
 |-  ( ( 1 e. RR* /\ 1 =/= +oo ) -> ( -oo +e 1 ) = -oo )
53 48 51 52 mp2an 
 |-  ( -oo +e 1 ) = -oo
54 53 a1i 
 |-  ( B = -oo -> ( -oo +e 1 ) = -oo )
55 47 54 eqtr2d 
 |-  ( B = -oo -> -oo = ( B +e 1 ) )
56 55 adantl 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> -oo = ( B +e 1 ) )
57 56 eqcomd 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> ( B +e 1 ) = -oo )
58 1 adantr 
 |-  ( ( ph /\ A =/= -oo ) -> A e. RR* )
59 simpr 
 |-  ( ( ph /\ A =/= -oo ) -> A =/= -oo )
60 nemnftgtmnft 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> -oo < A )
61 58 59 60 syl2anc 
 |-  ( ( ph /\ A =/= -oo ) -> -oo < A )
62 61 adantr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> -oo < A )
63 57 62 eqbrtrd 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> ( B +e 1 ) < A )
64 2 ad2antrr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> B e. RR* )
65 48 a1i 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> 1 e. RR* )
66 64 65 xaddcld 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> ( B +e 1 ) e. RR* )
67 1 ad2antrr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> A e. RR* )
68 xrltnle 
 |-  ( ( ( B +e 1 ) e. RR* /\ A e. RR* ) -> ( ( B +e 1 ) < A <-> -. A <_ ( B +e 1 ) ) )
69 66 67 68 syl2anc 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> ( ( B +e 1 ) < A <-> -. A <_ ( B +e 1 ) ) )
70 63 69 mpbid 
 |-  ( ( ( ph /\ A =/= -oo ) /\ B = -oo ) -> -. A <_ ( B +e 1 ) )
71 46 70 pm2.65da 
 |-  ( ( ph /\ A =/= -oo ) -> -. B = -oo )
72 71 neqned 
 |-  ( ( ph /\ A =/= -oo ) -> B =/= -oo )
73 72 ad4ant13 
 |-  ( ( ( ( ph /\ B =/= +oo ) /\ A =/= -oo ) /\ -. B e. RR ) -> B =/= -oo )
74 73 neneqd 
 |-  ( ( ( ( ph /\ B =/= +oo ) /\ A =/= -oo ) /\ -. B e. RR ) -> -. B = -oo )
75 33 74 condan 
 |-  ( ( ( ph /\ B =/= +oo ) /\ A =/= -oo ) -> B e. RR )
76 3 adantlr 
 |-  ( ( ( ph /\ B e. RR ) /\ x e. RR+ ) -> A <_ ( B +e x ) )
77 simpl 
 |-  ( ( B e. RR /\ x e. RR+ ) -> B e. RR )
78 rpre 
 |-  ( x e. RR+ -> x e. RR )
79 78 adantl 
 |-  ( ( B e. RR /\ x e. RR+ ) -> x e. RR )
80 rexadd 
 |-  ( ( B e. RR /\ x e. RR ) -> ( B +e x ) = ( B + x ) )
81 77 79 80 syl2anc 
 |-  ( ( B e. RR /\ x e. RR+ ) -> ( B +e x ) = ( B + x ) )
82 81 adantll 
 |-  ( ( ( ph /\ B e. RR ) /\ x e. RR+ ) -> ( B +e x ) = ( B + x ) )
83 76 82 breqtrd 
 |-  ( ( ( ph /\ B e. RR ) /\ x e. RR+ ) -> A <_ ( B + x ) )
84 83 ralrimiva 
 |-  ( ( ph /\ B e. RR ) -> A. x e. RR+ A <_ ( B + x ) )
85 1 adantr 
 |-  ( ( ph /\ B e. RR ) -> A e. RR* )
86 simpr 
 |-  ( ( ph /\ B e. RR ) -> B e. RR )
87 xralrple 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )
88 85 86 87 syl2anc 
 |-  ( ( ph /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )
89 84 88 mpbird 
 |-  ( ( ph /\ B e. RR ) -> A <_ B )
90 23 75 89 syl2anc 
 |-  ( ( ( ph /\ B =/= +oo ) /\ A =/= -oo ) -> A <_ B )
91 20 22 90 syl2anc 
 |-  ( ( ( ph /\ B =/= +oo ) /\ -. A = -oo ) -> A <_ B )
92 19 91 pm2.61dan 
 |-  ( ( ph /\ B =/= +oo ) -> A <_ B )
93 11 13 92 syl2anc 
 |-  ( ( ph /\ -. B = +oo ) -> A <_ B )
94 10 93 pm2.61dan 
 |-  ( ph -> A <_ B )