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

Metamath Proof Explorer

Theorem xpncan

Description: Extended real version of pncan . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xpncan ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 rexneg ⊢ ( 𝐵 ∈ ℝ → -𝑒 𝐵 = - 𝐵 )
2 1 adantl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → -𝑒 𝐵 = - 𝐵 )
3 2 oveq2d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐵 ) = ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) )
4 renegcl ⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
5 4 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → - 𝐵 ∈ ℝ )
6 rexr ⊢ ( - 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ* )
7 renepnf ⊢ ( - 𝐵 ∈ ℝ → - 𝐵 ≠ +∞ )
8 xaddmnf2 ⊢ ( ( - 𝐵 ∈ ℝ* ∧ - 𝐵 ≠ +∞ ) → ( -∞ +𝑒 - 𝐵 ) = -∞ )
9 6 7 8 syl2anc ⊢ ( - 𝐵 ∈ ℝ → ( -∞ +𝑒 - 𝐵 ) = -∞ )
10 5 9 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( -∞ +𝑒 - 𝐵 ) = -∞ )
11 oveq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 +𝑒 𝐵 ) = ( -∞ +𝑒 𝐵 ) )
12 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
13 renepnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ +∞ )
14 xaddmnf2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → ( -∞ +𝑒 𝐵 ) = -∞ )
15 12 13 14 syl2anc ⊢ ( 𝐵 ∈ ℝ → ( -∞ +𝑒 𝐵 ) = -∞ )
16 15 adantl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( -∞ +𝑒 𝐵 ) = -∞ )
17 11 16 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( 𝐴 +𝑒 𝐵 ) = -∞ )
18 17 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = ( -∞ +𝑒 - 𝐵 ) )
19 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → 𝐴 = -∞ )
20 10 18 19 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = 𝐴 )
21 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐴 ∈ ℝ* )
22 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐴 ≠ -∞ )
23 12 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ∈ ℝ* )
24 renemnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ -∞ )
25 24 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ≠ -∞ )
26 4 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → - 𝐵 ∈ ℝ )
27 26 6 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → - 𝐵 ∈ ℝ* )
28 renemnf ⊢ ( - 𝐵 ∈ ℝ → - 𝐵 ≠ -∞ )
29 26 28 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → - 𝐵 ≠ -∞ )
30 xaddass ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( - 𝐵 ∈ ℝ* ∧ - 𝐵 ≠ -∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) )
31 21 22 23 25 27 29 30 syl222anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) )
32 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ∈ ℝ )
33 32 26 rexaddd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐵 +𝑒 - 𝐵 ) = ( 𝐵 + - 𝐵 ) )
34 32 recnd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ∈ ℂ )
35 34 negidd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐵 + - 𝐵 ) = 0 )
36 33 35 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐵 +𝑒 - 𝐵 ) = 0 )
37 36 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) = ( 𝐴 +𝑒 0 ) )
38 xaddrid ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 0 ) = 𝐴 )
39 38 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 0 ) = 𝐴 )
40 37 39 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) = 𝐴 )
41 31 40 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = 𝐴 )
42 20 41 pm2.61dane ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = 𝐴 )
43 3 42 eqtrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐵 ) = 𝐴 )