Metamath Proof Explorer


Theorem xrge0npcan

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

Ref Expression
Assertion xrge0npcan ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )

Proof

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