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 xaddlid ⊢+∞∈ℝ*→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 xaddrid ⊢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