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

Metamath Proof Explorer

Theorem xadddilem

Description: Lemma for xadddi . (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
2 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
5 adddi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )
6 2 3 4 5 syl3an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )
7 6 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )
8 readdcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
9 rexmul ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 + 𝐶 ) ) = ( 𝐴 · ( 𝐵 + 𝐶 ) ) )
10 8 9 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ·e ( 𝐵 + 𝐶 ) ) = ( 𝐴 · ( 𝐵 + 𝐶 ) ) )
11 10 anassrs ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 + 𝐶 ) ) = ( 𝐴 · ( 𝐵 + 𝐶 ) ) )
12 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
13 12 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
14 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
15 14 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
16 13 15 rexaddd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) +𝑒 ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )
17 7 11 16 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) +𝑒 ( 𝐴 · 𝐶 ) ) )
18 rexadd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 + 𝐶 ) )
19 18 adantll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 + 𝐶 ) )
20 19 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e ( 𝐵 + 𝐶 ) ) )
21 rexmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = ( 𝐴 · 𝐵 ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = ( 𝐴 · 𝐵 ) )
23 rexmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐶 ) = ( 𝐴 · 𝐶 ) )
24 23 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐶 ) = ( 𝐴 · 𝐶 ) )
25 22 24 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) +𝑒 ( 𝐴 · 𝐶 ) ) )
26 17 20 25 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
27 1 26 sylanl1 ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
28 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
29 28 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
30 xmulpnf1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )
31 29 30 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )
32 31 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e +∞ ) = +∞ )
33 21 12 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) ∈ ℝ )
34 1 33 sylan ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) ∈ ℝ )
35 rexr ⊢ ( ( 𝐴 ·e 𝐵 ) ∈ ℝ → ( 𝐴 ·e 𝐵 ) ∈ ℝ* )
36 renemnf ⊢ ( ( 𝐴 ·e 𝐵 ) ∈ ℝ → ( 𝐴 ·e 𝐵 ) ≠ -∞ )
37 xaddpnf1 ⊢ ( ( ( 𝐴 ·e 𝐵 ) ∈ ℝ* ∧ ( 𝐴 ·e 𝐵 ) ≠ -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 +∞ ) = +∞ )
38 35 36 37 syl2anc ⊢ ( ( 𝐴 ·e 𝐵 ) ∈ ℝ → ( ( 𝐴 ·e 𝐵 ) +𝑒 +∞ ) = +∞ )
39 34 38 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 +∞ ) = +∞ )
40 32 39 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e +∞ ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 +∞ ) )
41 40 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e +∞ ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 +∞ ) )
42 oveq2 ⊢ ( 𝐶 = +∞ → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 +𝑒 +∞ ) )
43 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
44 renemnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ -∞ )
45 xaddpnf1 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → ( 𝐵 +𝑒 +∞ ) = +∞ )
46 43 44 45 syl2anc ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 +𝑒 +∞ ) = +∞ )
47 46 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 +𝑒 +∞ ) = +∞ )
48 42 47 sylan9eqr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = +∞ ) → ( 𝐵 +𝑒 𝐶 ) = +∞ )
49 48 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e +∞ ) )
50 oveq2 ⊢ ( 𝐶 = +∞ → ( 𝐴 ·e 𝐶 ) = ( 𝐴 ·e +∞ ) )
51 50 32 sylan9eqr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e 𝐶 ) = +∞ )
52 51 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 +∞ ) )
53 41 49 52 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
54 xmulmnf1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e -∞ ) = -∞ )
55 29 54 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e -∞ ) = -∞ )
56 55 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e -∞ ) = -∞ )
57 56 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e -∞ ) = -∞ )
58 34 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e 𝐵 ) ∈ ℝ )
59 renepnf ⊢ ( ( 𝐴 ·e 𝐵 ) ∈ ℝ → ( 𝐴 ·e 𝐵 ) ≠ +∞ )
60 xaddmnf1 ⊢ ( ( ( 𝐴 ·e 𝐵 ) ∈ ℝ* ∧ ( 𝐴 ·e 𝐵 ) ≠ +∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 -∞ ) = -∞ )
61 35 59 60 syl2anc ⊢ ( ( 𝐴 ·e 𝐵 ) ∈ ℝ → ( ( 𝐴 ·e 𝐵 ) +𝑒 -∞ ) = -∞ )
62 58 61 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 -∞ ) = -∞ )
63 57 62 eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e -∞ ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 -∞ ) )
64 oveq2 ⊢ ( 𝐶 = -∞ → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 +𝑒 -∞ ) )
65 renepnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ +∞ )
66 xaddmnf1 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → ( 𝐵 +𝑒 -∞ ) = -∞ )
67 43 65 66 syl2anc ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 +𝑒 -∞ ) = -∞ )
68 67 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 +𝑒 -∞ ) = -∞ )
69 64 68 sylan9eqr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( 𝐵 +𝑒 𝐶 ) = -∞ )
70 69 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e -∞ ) )
71 oveq2 ⊢ ( 𝐶 = -∞ → ( 𝐴 ·e 𝐶 ) = ( 𝐴 ·e -∞ ) )
72 71 56 sylan9eqr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e 𝐶 ) = -∞ )
73 72 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 -∞ ) )
74 63 70 73 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
75 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → 𝐶 ∈ ℝ* )
76 elxr ⊢ ( 𝐶 ∈ ℝ* ↔ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
77 75 76 sylib ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
78 77 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
79 27 53 74 78 mpjao3dan ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
80 31 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e +∞ ) = +∞ )
81 1 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) → 𝐴 ∈ ℝ )
82 23 14 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐶 ) ∈ ℝ )
83 81 82 sylan ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐶 ) ∈ ℝ )
84 rexr ⊢ ( ( 𝐴 ·e 𝐶 ) ∈ ℝ → ( 𝐴 ·e 𝐶 ) ∈ ℝ* )
85 renemnf ⊢ ( ( 𝐴 ·e 𝐶 ) ∈ ℝ → ( 𝐴 ·e 𝐶 ) ≠ -∞ )
86 xaddpnf2 ⊢ ( ( ( 𝐴 ·e 𝐶 ) ∈ ℝ* ∧ ( 𝐴 ·e 𝐶 ) ≠ -∞ ) → ( +∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) = +∞ )
87 84 85 86 syl2anc ⊢ ( ( 𝐴 ·e 𝐶 ) ∈ ℝ → ( +∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) = +∞ )
88 83 87 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( +∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) = +∞ )
89 80 88 eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e +∞ ) = ( +∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) )
90 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) → 𝐵 = +∞ )
91 90 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) → ( 𝐵 +𝑒 𝐶 ) = ( +∞ +𝑒 𝐶 ) )
92 rexr ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
93 renemnf ⊢ ( 𝐶 ∈ ℝ → 𝐶 ≠ -∞ )
94 xaddpnf2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) → ( +∞ +𝑒 𝐶 ) = +∞ )
95 92 93 94 syl2anc ⊢ ( 𝐶 ∈ ℝ → ( +∞ +𝑒 𝐶 ) = +∞ )
96 91 95 sylan9eq ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐵 +𝑒 𝐶 ) = +∞ )
97 96 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e +∞ ) )
98 oveq2 ⊢ ( 𝐵 = +∞ → ( 𝐴 ·e 𝐵 ) = ( 𝐴 ·e +∞ ) )
99 98 31 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) → ( 𝐴 ·e 𝐵 ) = +∞ )
100 99 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = +∞ )
101 100 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( +∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) )
102 89 97 101 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
103 pnfxr ⊢ +∞ ∈ ℝ*
104 pnfnemnf ⊢ +∞ ≠ -∞
105 xaddpnf1 ⊢ ( ( +∞ ∈ ℝ* ∧ +∞ ≠ -∞ ) → ( +∞ +𝑒 +∞ ) = +∞ )
106 103 104 105 mp2an ⊢ ( +∞ +𝑒 +∞ ) = +∞
107 31 31 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) = ( +∞ +𝑒 +∞ ) )
108 106 107 31 3eqtr4a ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) = ( 𝐴 ·e +∞ ) )
109 108 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) = ( 𝐴 ·e +∞ ) )
110 98 50 oveqan12d ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = +∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) )
111 110 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) )
112 oveq12 ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = +∞ ) → ( 𝐵 +𝑒 𝐶 ) = ( +∞ +𝑒 +∞ ) )
113 112 106 eqtrdi ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = +∞ ) → ( 𝐵 +𝑒 𝐶 ) = +∞ )
114 113 oveq2d ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e +∞ ) )
115 114 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e +∞ ) )
116 109 111 115 3eqtr4rd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
117 pnfaddmnf ⊢ ( +∞ +𝑒 -∞ ) = 0
118 31 55 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) = ( +∞ +𝑒 -∞ ) )
119 xmul01 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = 0 )
120 1 28 119 3syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e 0 ) = 0 )
121 117 118 120 3eqtr4a ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) = ( 𝐴 ·e 0 ) )
122 121 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) = ( 𝐴 ·e 0 ) )
123 98 71 oveqan12d ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) )
124 123 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e +∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) )
125 oveq12 ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = -∞ ) → ( 𝐵 +𝑒 𝐶 ) = ( +∞ +𝑒 -∞ ) )
126 125 117 eqtrdi ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = -∞ ) → ( 𝐵 +𝑒 𝐶 ) = 0 )
127 126 oveq2d ⊢ ( ( 𝐵 = +∞ ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e 0 ) )
128 127 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e 0 ) )
129 122 124 128 3eqtr4rd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
130 77 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) → ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
131 102 116 129 130 mpjao3dan ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
132 55 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e -∞ ) = -∞ )
133 1 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) → 𝐴 ∈ ℝ )
134 133 82 sylan ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐶 ) ∈ ℝ )
135 renepnf ⊢ ( ( 𝐴 ·e 𝐶 ) ∈ ℝ → ( 𝐴 ·e 𝐶 ) ≠ +∞ )
136 xaddmnf2 ⊢ ( ( ( 𝐴 ·e 𝐶 ) ∈ ℝ* ∧ ( 𝐴 ·e 𝐶 ) ≠ +∞ ) → ( -∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) = -∞ )
137 84 135 136 syl2anc ⊢ ( ( 𝐴 ·e 𝐶 ) ∈ ℝ → ( -∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) = -∞ )
138 134 137 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( -∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) = -∞ )
139 132 138 eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e -∞ ) = ( -∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) )
140 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) → 𝐵 = -∞ )
141 140 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) → ( 𝐵 +𝑒 𝐶 ) = ( -∞ +𝑒 𝐶 ) )
142 renepnf ⊢ ( 𝐶 ∈ ℝ → 𝐶 ≠ +∞ )
143 xaddmnf2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) → ( -∞ +𝑒 𝐶 ) = -∞ )
144 92 142 143 syl2anc ⊢ ( 𝐶 ∈ ℝ → ( -∞ +𝑒 𝐶 ) = -∞ )
145 141 144 sylan9eq ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐵 +𝑒 𝐶 ) = -∞ )
146 145 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e -∞ ) )
147 oveq2 ⊢ ( 𝐵 = -∞ → ( 𝐴 ·e 𝐵 ) = ( 𝐴 ·e -∞ ) )
148 147 55 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) → ( 𝐴 ·e 𝐵 ) = -∞ )
149 148 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = -∞ )
150 149 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( -∞ +𝑒 ( 𝐴 ·e 𝐶 ) ) )
151 139 146 150 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
152 55 31 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) = ( -∞ +𝑒 +∞ ) )
153 mnfaddpnf ⊢ ( -∞ +𝑒 +∞ ) = 0
154 152 153 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) = 0 )
155 120 154 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e 0 ) = ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) )
156 155 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e 0 ) = ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) )
157 oveq12 ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = +∞ ) → ( 𝐵 +𝑒 𝐶 ) = ( -∞ +𝑒 +∞ ) )
158 157 153 eqtrdi ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = +∞ ) → ( 𝐵 +𝑒 𝐶 ) = 0 )
159 158 oveq2d ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e 0 ) )
160 159 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e 0 ) )
161 147 50 oveqan12d ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = +∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) )
162 161 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e +∞ ) ) )
163 156 160 162 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = +∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
164 mnfxr ⊢ -∞ ∈ ℝ*
165 mnfnepnf ⊢ -∞ ≠ +∞
166 xaddmnf1 ⊢ ( ( -∞ ∈ ℝ* ∧ -∞ ≠ +∞ ) → ( -∞ +𝑒 -∞ ) = -∞ )
167 164 165 166 mp2an ⊢ ( -∞ +𝑒 -∞ ) = -∞
168 55 55 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) = ( -∞ +𝑒 -∞ ) )
169 167 168 55 3eqtr4a ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) = ( 𝐴 ·e -∞ ) )
170 169 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) = ( 𝐴 ·e -∞ ) )
171 147 71 oveqan12d ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) )
172 171 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) = ( ( 𝐴 ·e -∞ ) +𝑒 ( 𝐴 ·e -∞ ) ) )
173 oveq12 ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = -∞ ) → ( 𝐵 +𝑒 𝐶 ) = ( -∞ +𝑒 -∞ ) )
174 173 167 eqtrdi ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = -∞ ) → ( 𝐵 +𝑒 𝐶 ) = -∞ )
175 174 oveq2d ⊢ ( ( 𝐵 = -∞ ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e -∞ ) )
176 175 adantll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( 𝐴 ·e -∞ ) )
177 170 172 176 3eqtr4rd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) ∧ 𝐶 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
178 77 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) → ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
179 151 163 177 178 mpjao3dan ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) ∧ 𝐵 = -∞ ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )
180 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → 𝐵 ∈ ℝ* )
181 elxr ⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
182 180 181 sylib ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
183 79 131 179 182 mpjao3dan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )