# Metamath Proof Explorer

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 ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
xrlexaddrp.2 ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
xrlexaddrp.3 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {A}\le {B}{+}_{𝑒}{x}$
Assertion xrlexaddrp ${⊢}{\phi }\to {A}\le {B}$

### Proof

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