This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xrlexaddrp.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
xrlexaddrp.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 +𝑒 𝑥 ) )
Assertion xrlexaddrp ( 𝜑 → 𝐴 ≤ 𝐵 )

Proof

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