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

Metamath Proof Explorer

Theorem xsubge0

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

Ref Expression
Assertion xsubge0 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ ( 𝐴 +𝑒 -𝑒 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )

Proof

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