Metamath Proof Explorer

Theorem xrge0adddir

Description: Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017)

Ref Expression
Assertion xrge0adddir ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
2 simpl1 ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 ∈ ( 0 [,) +∞ ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
3 1 2 sselid ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 ∈ ( 0 [,) +∞ ) ) → 𝐴 ∈ ℝ* )
4 simpl2 ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5 1 4 sselid ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℝ* )
6 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
7 simpr ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 ∈ ( 0 [,) +∞ ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
8 6 7 sselid ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 ∈ ( 0 [,) +∞ ) ) → 𝐶 ∈ ℝ )
9 xadddir ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )
10 3 5 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )
11 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ( 0 [,] +∞ ) )
12 1 11 sselid ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ* )
13 simpll2 ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
14 1 13 sselid ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → 𝐵 ∈ ℝ* )
15 12 14 xaddcld ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* )
16 simpr ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → 0 < 𝐴 )
17 xrge0addgt0 ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝐴 ) → 0 < ( 𝐴 +𝑒 𝐵 ) )
18 11 13 16 17 syl21anc ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → 0 < ( 𝐴 +𝑒 𝐵 ) )
19 xmulpnf1 ⊢ ( ( ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* ∧ 0 < ( 𝐴 +𝑒 𝐵 ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e +∞ ) = +∞ )
20 15 18 19 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( ( 𝐴 +𝑒 𝐵 ) ·e +∞ ) = +∞ )
21 oveq2 ⊢ ( 𝐶 = +∞ → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 +𝑒 𝐵 ) ·e +∞ ) )
22 21 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 +𝑒 𝐵 ) ·e +∞ ) )
23 simpll3 ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
24 ge0xmulcl ⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 ·e 𝐶 ) ∈ ( 0 [,] +∞ ) )
25 13 23 24 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( 𝐵 ·e 𝐶 ) ∈ ( 0 [,] +∞ ) )
26 1 25 sselid ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( 𝐵 ·e 𝐶 ) ∈ ℝ* )
27 xrge0neqmnf ⊢ ( ( 𝐵 ·e 𝐶 ) ∈ ( 0 [,] +∞ ) → ( 𝐵 ·e 𝐶 ) ≠ -∞ )
28 25 27 syl ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( 𝐵 ·e 𝐶 ) ≠ -∞ )
29 xaddpnf2 ⊢ ( ( ( 𝐵 ·e 𝐶 ) ∈ ℝ* ∧ ( 𝐵 ·e 𝐶 ) ≠ -∞ ) → ( +∞ +𝑒 ( 𝐵 ·e 𝐶 ) ) = +∞ )
30 26 28 29 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( +∞ +𝑒 ( 𝐵 ·e 𝐶 ) ) = +∞ )
31 20 22 30 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( +∞ +𝑒 ( 𝐵 ·e 𝐶 ) ) )
32 oveq2 ⊢ ( 𝐶 = +∞ → ( 𝐴 ·e 𝐶 ) = ( 𝐴 ·e +∞ ) )
33 32 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e 𝐶 ) = ( 𝐴 ·e +∞ ) )
34 xmulpnf1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )
35 12 16 34 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )
36 33 35 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( 𝐴 ·e 𝐶 ) = +∞ )
37 36 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( +∞ +𝑒 ( 𝐵 ·e 𝐶 ) ) )
38 31 37 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 < 𝐴 ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )
39 simpll3 ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
40 1 39 sselid ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → 𝐶 ∈ ℝ* )
41 xmul02 ⊢ ( 𝐶 ∈ ℝ* → ( 0 ·e 𝐶 ) = 0 )
42 40 41 syl ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( 0 ·e 𝐶 ) = 0 )
43 42 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( ( 0 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( 0 +𝑒 ( 𝐵 ·e 𝐶 ) ) )
44 oveq1 ⊢ ( 0 = 𝐴 → ( 0 ·e 𝐶 ) = ( 𝐴 ·e 𝐶 ) )
45 44 adantl ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( 0 ·e 𝐶 ) = ( 𝐴 ·e 𝐶 ) )
46 45 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( ( 0 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )
47 simpll2 ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
48 1 47 sselid ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → 𝐵 ∈ ℝ* )
49 48 40 xmulcld ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( 𝐵 ·e 𝐶 ) ∈ ℝ* )
50 xaddid2 ⊢ ( ( 𝐵 ·e 𝐶 ) ∈ ℝ* → ( 0 +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( 𝐵 ·e 𝐶 ) )
51 49 50 syl ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( 0 +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( 𝐵 ·e 𝐶 ) )
52 43 46 51 3eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( 𝐵 ·e 𝐶 ) )
53 xaddid2 ⊢ ( 𝐵 ∈ ℝ* → ( 0 +𝑒 𝐵 ) = 𝐵 )
54 48 53 syl ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( 0 +𝑒 𝐵 ) = 𝐵 )
55 54 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( ( 0 +𝑒 𝐵 ) ·e 𝐶 ) = ( 𝐵 ·e 𝐶 ) )
56 oveq1 ⊢ ( 0 = 𝐴 → ( 0 +𝑒 𝐵 ) = ( 𝐴 +𝑒 𝐵 ) )
57 56 oveq1d ⊢ ( 0 = 𝐴 → ( ( 0 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) )
58 57 adantl ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( ( 0 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) )
59 52 55 58 3eqtr2rd ⊢ ( ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) ∧ 0 = 𝐴 ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )
60 0xr ⊢ 0 ∈ ℝ*
61 60 a1i ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) → 0 ∈ ℝ* )
62 simpl1 ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
63 1 62 sselid ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) → 𝐴 ∈ ℝ* )
64 pnfxr ⊢ +∞ ∈ ℝ*
65 64 a1i ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) → +∞ ∈ ℝ* )
66 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐴 )
67 61 65 62 66 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) → 0 ≤ 𝐴 )
68 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
69 68 biimpa ⊢ ( ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ 0 ≤ 𝐴 ) → ( 0 < 𝐴 ∨ 0 = 𝐴 ) )
70 61 63 67 69 syl21anc ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) → ( 0 < 𝐴 ∨ 0 = 𝐴 ) )
71 38 59 70 mpjaodan ⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )
72 0lepnf ⊢ 0 ≤ +∞
73 eliccelico ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → ( 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( 𝐶 ∈ ( 0 [,) +∞ ) ∨ 𝐶 = +∞ ) ) )
74 60 64 72 73 mp3an ⊢ ( 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( 𝐶 ∈ ( 0 [,) +∞ ) ∨ 𝐶 = +∞ ) )
75 74 3anbi3i ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) ↔ ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ ( 𝐶 ∈ ( 0 [,) +∞ ) ∨ 𝐶 = +∞ ) ) )
76 75 simp3bi ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ∈ ( 0 [,) +∞ ) ∨ 𝐶 = +∞ ) )
77 10 71 76 mpjaodan ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )