Metamath Proof Explorer

Theorem xrge0npcan

Description: Extended nonnegative real version of npcan . (Contributed by Thierry Arnoux, 9-Jun-2017)

Ref Expression
Assertion xrge0npcan ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A → A + 𝑒 − B + 𝑒 B = A

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ 0 +∞ ⊆ ℝ *
2 simpl1 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A ∈ 0 +∞
3 1 2 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A ∈ ℝ *
4 simpr ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → B = +∞
5 simpl3 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → B ≤ A
6 4 5 eqbrtrrd ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → +∞ ≤ A
7 xgepnf ⊢ A ∈ ℝ * → +∞ ≤ A ↔ A = +∞
8 7 biimpa ⊢ A ∈ ℝ * ∧ +∞ ≤ A → A = +∞
9 3 6 8 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A = +∞
10 xnegeq ⊢ B = +∞ → − B = − +∞
11 4 10 syl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → − B = − +∞
12 9 11 oveq12d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A + 𝑒 − B = +∞ + 𝑒 − +∞
13 pnfxr ⊢ +∞ ∈ ℝ *
14 xnegid ⊢ +∞ ∈ ℝ * → +∞ + 𝑒 − +∞ = 0
15 13 14 ax-mp ⊢ +∞ + 𝑒 − +∞ = 0
16 12 15 eqtrdi ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A + 𝑒 − B = 0
17 16 oveq1d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A + 𝑒 − B + 𝑒 B = 0 + 𝑒 B
18 4 oveq2d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → 0 + 𝑒 B = 0 + 𝑒 +∞
19 xaddid2 ⊢ +∞ ∈ ℝ * → 0 + 𝑒 +∞ = +∞
20 13 19 mp1i ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → 0 + 𝑒 +∞ = +∞
21 17 18 20 3eqtrd ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A + 𝑒 − B + 𝑒 B = +∞
22 21 9 eqtr4d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ B = +∞ → A + 𝑒 − B + 𝑒 B = A
23 simpl1 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → A ∈ 0 +∞
24 1 23 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → A ∈ ℝ *
25 xrge0neqmnf ⊢ A ∈ 0 +∞ → A ≠ −∞
26 23 25 syl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → A ≠ −∞
27 simpl2 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → B ∈ 0 +∞
28 1 27 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → B ∈ ℝ *
29 28 xnegcld ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → − B ∈ ℝ *
30 simpr ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → ¬ B = +∞
31 xnegneg ⊢ B ∈ ℝ * → − − B = B
32 xnegeq ⊢ − B = −∞ → − − B = − −∞
33 31 32 sylan9req ⊢ B ∈ ℝ * ∧ − B = −∞ → B = − −∞
34 xnegmnf ⊢ − −∞ = +∞
35 33 34 eqtrdi ⊢ B ∈ ℝ * ∧ − B = −∞ → B = +∞
36 35 stoic1a ⊢ B ∈ ℝ * ∧ ¬ B = +∞ → ¬ − B = −∞
37 36 neqned ⊢ B ∈ ℝ * ∧ ¬ B = +∞ → − B ≠ −∞
38 28 30 37 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → − B ≠ −∞
39 xrge0neqmnf ⊢ B ∈ 0 +∞ → B ≠ −∞
40 27 39 syl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → B ≠ −∞
41 xaddass ⊢ A ∈ ℝ * ∧ A ≠ −∞ ∧ − B ∈ ℝ * ∧ − B ≠ −∞ ∧ B ∈ ℝ * ∧ B ≠ −∞ → A + 𝑒 − B + 𝑒 B = A + 𝑒 − B + 𝑒 B
42 24 26 29 38 28 40 41 syl222anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → A + 𝑒 − B + 𝑒 B = A + 𝑒 − B + 𝑒 B
43 xnegcl ⊢ B ∈ ℝ * → − B ∈ ℝ *
44 xaddcom ⊢ − B ∈ ℝ * ∧ B ∈ ℝ * → − B + 𝑒 B = B + 𝑒 − B
45 43 44 mpancom ⊢ B ∈ ℝ * → − B + 𝑒 B = B + 𝑒 − B
46 xnegid ⊢ B ∈ ℝ * → B + 𝑒 − B = 0
47 45 46 eqtrd ⊢ B ∈ ℝ * → − B + 𝑒 B = 0
48 47 oveq2d ⊢ B ∈ ℝ * → A + 𝑒 − B + 𝑒 B = A + 𝑒 0
49 xaddid1 ⊢ A ∈ ℝ * → A + 𝑒 0 = A
50 48 49 sylan9eqr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 − B + 𝑒 B = A
51 24 28 50 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → A + 𝑒 − B + 𝑒 B = A
52 42 51 eqtrd ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A ∧ ¬ B = +∞ → A + 𝑒 − B + 𝑒 B = A
53 22 52 pm2.61dan ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ B ≤ A → A + 𝑒 − B + 𝑒 B = A