Metamath Proof Explorer

Theorem xsubge0

Description: Extended real version of subge0 . (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion xsubge0 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → 0 ≤ A + 𝑒 − B ↔ B ≤ A

Proof

Step Hyp Ref Expression
1 elxr ⊢ B ∈ ℝ * ↔ B ∈ ℝ ∨ B = +∞ ∨ B = −∞
2 0xr ⊢ 0 ∈ ℝ *
3 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
4 xnegcl ⊢ B ∈ ℝ * → − B ∈ ℝ *
5 xaddcl ⊢ A ∈ ℝ * ∧ − B ∈ ℝ * → A + 𝑒 − B ∈ ℝ *
6 4 5 sylan2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 − B ∈ ℝ *
7 3 6 sylan2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ → A + 𝑒 − B ∈ ℝ *
8 simpr ⊢ A ∈ ℝ * ∧ B ∈ ℝ → B ∈ ℝ
9 xleadd1 ⊢ 0 ∈ ℝ * ∧ A + 𝑒 − B ∈ ℝ * ∧ B ∈ ℝ → 0 ≤ A + 𝑒 − B ↔ 0 + 𝑒 B ≤ A + 𝑒 − B + 𝑒 B
10 2 7 8 9 mp3an2i ⊢ A ∈ ℝ * ∧ B ∈ ℝ → 0 ≤ A + 𝑒 − B ↔ 0 + 𝑒 B ≤ A + 𝑒 − B + 𝑒 B
11 3 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ → B ∈ ℝ *
12 xaddlid ⊢ B ∈ ℝ * → 0 + 𝑒 B = B
13 11 12 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ → 0 + 𝑒 B = B
14 xnpcan ⊢ A ∈ ℝ * ∧ B ∈ ℝ → A + 𝑒 − B + 𝑒 B = A
15 13 14 breq12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ → 0 + 𝑒 B ≤ A + 𝑒 − B + 𝑒 B ↔ B ≤ A
16 10 15 bitrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ → 0 ≤ A + 𝑒 − B ↔ B ≤ A
17 pnfxr ⊢ +∞ ∈ ℝ *
18 xrletri3 ⊢ A ∈ ℝ * ∧ +∞ ∈ ℝ * → A = +∞ ↔ A ≤ +∞ ∧ +∞ ≤ A
19 17 18 mpan2 ⊢ A ∈ ℝ * → A = +∞ ↔ A ≤ +∞ ∧ +∞ ≤ A
20 mnflt0 ⊢ −∞ < 0
21 mnfxr ⊢ −∞ ∈ ℝ *
22 xrltnle ⊢ −∞ ∈ ℝ * ∧ 0 ∈ ℝ * → −∞ < 0 ↔ ¬ 0 ≤ −∞
23 21 2 22 mp2an ⊢ −∞ < 0 ↔ ¬ 0 ≤ −∞
24 20 23 mpbi ⊢ ¬ 0 ≤ −∞
25 xaddmnf1 ⊢ A ∈ ℝ * ∧ A ≠ +∞ → A + 𝑒 −∞ = −∞
26 25 breq2d ⊢ A ∈ ℝ * ∧ A ≠ +∞ → 0 ≤ A + 𝑒 −∞ ↔ 0 ≤ −∞
27 24 26 mtbiri ⊢ A ∈ ℝ * ∧ A ≠ +∞ → ¬ 0 ≤ A + 𝑒 −∞
28 27 ex ⊢ A ∈ ℝ * → A ≠ +∞ → ¬ 0 ≤ A + 𝑒 −∞
29 28 necon4ad ⊢ A ∈ ℝ * → 0 ≤ A + 𝑒 −∞ → A = +∞
30 0le0 ⊢ 0 ≤ 0
31 oveq1 ⊢ A = +∞ → A + 𝑒 −∞ = +∞ + 𝑒 −∞
32 pnfaddmnf ⊢ +∞ + 𝑒 −∞ = 0
33 31 32 eqtrdi ⊢ A = +∞ → A + 𝑒 −∞ = 0
34 30 33 breqtrrid ⊢ A = +∞ → 0 ≤ A + 𝑒 −∞
35 29 34 impbid1 ⊢ A ∈ ℝ * → 0 ≤ A + 𝑒 −∞ ↔ A = +∞
36 pnfge ⊢ A ∈ ℝ * → A ≤ +∞
37 36 biantrurd ⊢ A ∈ ℝ * → +∞ ≤ A ↔ A ≤ +∞ ∧ +∞ ≤ A
38 19 35 37 3bitr4d ⊢ A ∈ ℝ * → 0 ≤ A + 𝑒 −∞ ↔ +∞ ≤ A
39 38 adantr ⊢ A ∈ ℝ * ∧ B = +∞ → 0 ≤ A + 𝑒 −∞ ↔ +∞ ≤ A
40 xnegeq ⊢ B = +∞ → − B = − +∞
41 xnegpnf ⊢ − +∞ = −∞
42 40 41 eqtrdi ⊢ B = +∞ → − B = −∞
43 42 adantl ⊢ A ∈ ℝ * ∧ B = +∞ → − B = −∞
44 43 oveq2d ⊢ A ∈ ℝ * ∧ B = +∞ → A + 𝑒 − B = A + 𝑒 −∞
45 44 breq2d ⊢ A ∈ ℝ * ∧ B = +∞ → 0 ≤ A + 𝑒 − B ↔ 0 ≤ A + 𝑒 −∞
46 breq1 ⊢ B = +∞ → B ≤ A ↔ +∞ ≤ A
47 46 adantl ⊢ A ∈ ℝ * ∧ B = +∞ → B ≤ A ↔ +∞ ≤ A
48 39 45 47 3bitr4d ⊢ A ∈ ℝ * ∧ B = +∞ → 0 ≤ A + 𝑒 − B ↔ B ≤ A
49 oveq1 ⊢ A = −∞ → A + 𝑒 +∞ = −∞ + 𝑒 +∞
50 mnfaddpnf ⊢ −∞ + 𝑒 +∞ = 0
51 49 50 eqtrdi ⊢ A = −∞ → A + 𝑒 +∞ = 0
52 51 adantl ⊢ A ∈ ℝ * ∧ A = −∞ → A + 𝑒 +∞ = 0
53 30 52 breqtrrid ⊢ A ∈ ℝ * ∧ A = −∞ → 0 ≤ A + 𝑒 +∞
54 0lepnf ⊢ 0 ≤ +∞
55 xaddpnf1 ⊢ A ∈ ℝ * ∧ A ≠ −∞ → A + 𝑒 +∞ = +∞
56 54 55 breqtrrid ⊢ A ∈ ℝ * ∧ A ≠ −∞ → 0 ≤ A + 𝑒 +∞
57 53 56 pm2.61dane ⊢ A ∈ ℝ * → 0 ≤ A + 𝑒 +∞
58 mnfle ⊢ A ∈ ℝ * → −∞ ≤ A
59 57 58 2thd ⊢ A ∈ ℝ * → 0 ≤ A + 𝑒 +∞ ↔ −∞ ≤ A
60 59 adantr ⊢ A ∈ ℝ * ∧ B = −∞ → 0 ≤ A + 𝑒 +∞ ↔ −∞ ≤ A
61 xnegeq ⊢ B = −∞ → − B = − −∞
62 xnegmnf ⊢ − −∞ = +∞
63 61 62 eqtrdi ⊢ B = −∞ → − B = +∞
64 63 adantl ⊢ A ∈ ℝ * ∧ B = −∞ → − B = +∞
65 64 oveq2d ⊢ A ∈ ℝ * ∧ B = −∞ → A + 𝑒 − B = A + 𝑒 +∞
66 65 breq2d ⊢ A ∈ ℝ * ∧ B = −∞ → 0 ≤ A + 𝑒 − B ↔ 0 ≤ A + 𝑒 +∞
67 breq1 ⊢ B = −∞ → B ≤ A ↔ −∞ ≤ A
68 67 adantl ⊢ A ∈ ℝ * ∧ B = −∞ → B ≤ A ↔ −∞ ≤ A
69 60 66 68 3bitr4d ⊢ A ∈ ℝ * ∧ B = −∞ → 0 ≤ A + 𝑒 − B ↔ B ≤ A
70 16 48 69 3jaodan ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∨ B = +∞ ∨ B = −∞ → 0 ≤ A + 𝑒 − B ↔ B ≤ A
71 1 70 sylan2b ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → 0 ≤ A + 𝑒 − B ↔ B ≤ A