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

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 xaddlid ⊢ ( +∞ ∈ ℝ* → ( 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 xaddrid ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 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 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )