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

Metamath Proof Explorer

Theorem xadddi2

Description: The assumption that the multiplier be real in xadddi can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xadddi2 ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
2 simp2l ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → 𝐵 ∈ ℝ* )
3 2 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℝ* )
4 simp3l ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → 𝐶 ∈ ℝ* )
5 4 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 ∈ ℝ ) → 𝐶 ∈ ℝ* )
6 xadddi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
7 1 3 5 6 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
8 pnfxr ⊢ +∞ ∈ ℝ*
9 4 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 𝐶 ∈ ℝ* )
10 xmulcl ⊢ ( ( +∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( +∞ ·e 𝐶 ) ∈ ℝ* )
11 8 9 10 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( +∞ ·e 𝐶 ) ∈ ℝ* )
12 simpl3r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 0 ≤ 𝐶 )
13 0lepnf ⊢ 0 ≤ +∞
14 xmulge0 ⊢ ( ( ( +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → 0 ≤ ( +∞ ·e 𝐶 ) )
15 8 13 14 mpanl12 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) → 0 ≤ ( +∞ ·e 𝐶 ) )
16 4 12 15 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 0 ≤ ( +∞ ·e 𝐶 ) )
17 ge0nemnf ⊢ ( ( ( +∞ ·e 𝐶 ) ∈ ℝ* ∧ 0 ≤ ( +∞ ·e 𝐶 ) ) → ( +∞ ·e 𝐶 ) ≠ -∞ )
18 11 16 17 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( +∞ ·e 𝐶 ) ≠ -∞ )
19 18 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = +∞ ) → ( +∞ ·e 𝐶 ) ≠ -∞ )
20 xaddpnf2 ⊢ ( ( ( +∞ ·e 𝐶 ) ∈ ℝ* ∧ ( +∞ ·e 𝐶 ) ≠ -∞ ) → ( +∞ +𝑒 ( +∞ ·e 𝐶 ) ) = +∞ )
21 11 19 20 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = +∞ ) → ( +∞ +𝑒 ( +∞ ·e 𝐶 ) ) = +∞ )
22 oveq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 ·e 𝐵 ) = ( +∞ ·e 𝐵 ) )
23 oveq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 ·e 𝐶 ) = ( +∞ ·e 𝐶 ) )
24 22 23 oveq12d ⊢ ( 𝐴 = +∞ → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( +∞ ·e 𝐵 ) +𝑒 ( +∞ ·e 𝐶 ) ) )
25 xmulpnf2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) → ( +∞ ·e 𝐵 ) = +∞ )
26 2 25 sylan ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( +∞ ·e 𝐵 ) = +∞ )
27 26 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( ( +∞ ·e 𝐵 ) +𝑒 ( +∞ ·e 𝐶 ) ) = ( +∞ +𝑒 ( +∞ ·e 𝐶 ) ) )
28 24 27 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = +∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( +∞ +𝑒 ( +∞ ·e 𝐶 ) ) )
29 oveq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( +∞ ·e ( 𝐵 +𝑒 𝐶 ) ) )
30 xaddcl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
31 2 4 30 syl2anc ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
32 0xr ⊢ 0 ∈ ℝ*
33 32 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 0 ∈ ℝ* )
34 2 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ* )
35 31 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
36 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 0 < 𝐵 )
37 34 xaddridd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( 𝐵 +𝑒 0 ) = 𝐵 )
38 xleadd2a ⊢ ( ( ( 0 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 0 ≤ 𝐶 ) → ( 𝐵 +𝑒 0 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
39 33 9 34 12 38 syl31anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( 𝐵 +𝑒 0 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
40 37 39 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 𝐵 ≤ ( 𝐵 +𝑒 𝐶 ) )
41 33 34 35 36 40 xrltletrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 0 < ( 𝐵 +𝑒 𝐶 ) )
42 xmulpnf2 ⊢ ( ( ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* ∧ 0 < ( 𝐵 +𝑒 𝐶 ) ) → ( +∞ ·e ( 𝐵 +𝑒 𝐶 ) ) = +∞ )
43 31 41 42 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( +∞ ·e ( 𝐵 +𝑒 𝐶 ) ) = +∞ )
44 29 43 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = +∞ )
45 21 28 44 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
46 mnfxr ⊢ -∞ ∈ ℝ*
47 xmulcl ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( -∞ ·e 𝐶 ) ∈ ℝ* )
48 46 9 47 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -∞ ·e 𝐶 ) ∈ ℝ* )
49 xmulneg1 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( -𝑒 -∞ ·e 𝐶 ) = -𝑒 ( -∞ ·e 𝐶 ) )
50 46 9 49 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -𝑒 -∞ ·e 𝐶 ) = -𝑒 ( -∞ ·e 𝐶 ) )
51 xnegmnf ⊢ -𝑒 -∞ = +∞
52 51 oveq1i ⊢ ( -𝑒 -∞ ·e 𝐶 ) = ( +∞ ·e 𝐶 )
53 50 52 eqtr3di ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → -𝑒 ( -∞ ·e 𝐶 ) = ( +∞ ·e 𝐶 ) )
54 xnegpnf ⊢ -𝑒 +∞ = -∞
55 54 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → -𝑒 +∞ = -∞ )
56 53 55 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -𝑒 ( -∞ ·e 𝐶 ) = -𝑒 +∞ ↔ ( +∞ ·e 𝐶 ) = -∞ ) )
57 xneg11 ⊢ ( ( ( -∞ ·e 𝐶 ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -𝑒 ( -∞ ·e 𝐶 ) = -𝑒 +∞ ↔ ( -∞ ·e 𝐶 ) = +∞ ) )
58 48 8 57 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -𝑒 ( -∞ ·e 𝐶 ) = -𝑒 +∞ ↔ ( -∞ ·e 𝐶 ) = +∞ ) )
59 56 58 bitr3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( ( +∞ ·e 𝐶 ) = -∞ ↔ ( -∞ ·e 𝐶 ) = +∞ ) )
60 59 necon3bid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( ( +∞ ·e 𝐶 ) ≠ -∞ ↔ ( -∞ ·e 𝐶 ) ≠ +∞ ) )
61 18 60 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -∞ ·e 𝐶 ) ≠ +∞ )
62 xaddmnf2 ⊢ ( ( ( -∞ ·e 𝐶 ) ∈ ℝ* ∧ ( -∞ ·e 𝐶 ) ≠ +∞ ) → ( -∞ +𝑒 ( -∞ ·e 𝐶 ) ) = -∞ )
63 48 61 62 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -∞ +𝑒 ( -∞ ·e 𝐶 ) ) = -∞ )
64 63 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = -∞ ) → ( -∞ +𝑒 ( -∞ ·e 𝐶 ) ) = -∞ )
65 oveq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 ·e 𝐵 ) = ( -∞ ·e 𝐵 ) )
66 oveq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 ·e 𝐶 ) = ( -∞ ·e 𝐶 ) )
67 65 66 oveq12d ⊢ ( 𝐴 = -∞ → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( -∞ ·e 𝐵 ) +𝑒 ( -∞ ·e 𝐶 ) ) )
68 xmulmnf2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) → ( -∞ ·e 𝐵 ) = -∞ )
69 2 68 sylan ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -∞ ·e 𝐵 ) = -∞ )
70 69 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( ( -∞ ·e 𝐵 ) +𝑒 ( -∞ ·e 𝐶 ) ) = ( -∞ +𝑒 ( -∞ ·e 𝐶 ) ) )
71 67 70 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( -∞ +𝑒 ( -∞ ·e 𝐶 ) ) )
72 oveq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( -∞ ·e ( 𝐵 +𝑒 𝐶 ) ) )
73 xmulmnf2 ⊢ ( ( ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* ∧ 0 < ( 𝐵 +𝑒 𝐶 ) ) → ( -∞ ·e ( 𝐵 +𝑒 𝐶 ) ) = -∞ )
74 31 41 73 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( -∞ ·e ( 𝐵 +𝑒 𝐶 ) ) = -∞ )
75 72 74 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = -∞ )
76 64 71 75 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) ∧ 𝐴 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
77 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → 𝐴 ∈ ℝ* )
78 elxr ⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
79 77 78 sylib ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
80 7 45 76 79 mpjao3dan ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 < 𝐵 ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
81 simp1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → 𝐴 ∈ ℝ* )
82 xmulcl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ·e 𝐶 ) ∈ ℝ* )
83 81 4 82 syl2anc ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ·e 𝐶 ) ∈ ℝ* )
84 83 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 = 𝐵 ) → ( 𝐴 ·e 𝐶 ) ∈ ℝ* )
85 xaddlid ⊢ ( ( 𝐴 ·e 𝐶 ) ∈ ℝ* → ( 0 +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( 𝐴 ·e 𝐶 ) )
86 84 85 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 = 𝐵 ) → ( 0 +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( 𝐴 ·e 𝐶 ) )
87 oveq2 ⊢ ( 0 = 𝐵 → ( 𝐴 ·e 0 ) = ( 𝐴 ·e 𝐵 ) )
88 87 eqcomd ⊢ ( 0 = 𝐵 → ( 𝐴 ·e 𝐵 ) = ( 𝐴 ·e 0 ) )
89 xmul01 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = 0 )
90 89 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ·e 0 ) = 0 )
91 88 90 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 = 𝐵 ) → ( 𝐴 ·e 𝐵 ) = 0 )
92 91 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 = 𝐵 ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( 0 +𝑒 ( 𝐴 ·e 𝐶 ) ) )
93 oveq1 ⊢ ( 0 = 𝐵 → ( 0 +𝑒 𝐶 ) = ( 𝐵 +𝑒 𝐶 ) )
94 93 eqcomd ⊢ ( 0 = 𝐵 → ( 𝐵 +𝑒 𝐶 ) = ( 0 +𝑒 𝐶 ) )
95 xaddlid ⊢ ( 𝐶 ∈ ℝ* → ( 0 +𝑒 𝐶 ) = 𝐶 )
96 4 95 syl ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 0 +𝑒 𝐶 ) = 𝐶 )
97 94 96 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 = 𝐵 ) → ( 𝐵 +𝑒 𝐶 ) = 𝐶 )
98 97 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 = 𝐵 ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e 𝐶 ) )
99 86 92 98 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) ∧ 0 = 𝐵 ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
100 simp2r ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → 0 ≤ 𝐵 )
101 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) )
102 32 2 101 sylancr ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) )
103 100 102 mpbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 0 < 𝐵 ∨ 0 = 𝐵 ) )
104 80 99 103 mpjaodan ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ∧ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )