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 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )