Step |
Hyp |
Ref |
Expression |
1 |
|
xrge0adddir |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) ) |
2 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
3 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ ( 0 [,] +∞ ) ) |
4 |
2 3
|
sselid |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ ℝ* ) |
5 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ( 0 [,] +∞ ) ) |
6 |
2 5
|
sselid |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ℝ* ) |
7 |
4 6
|
xaddcld |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* ) |
8 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ( 0 [,] +∞ ) ) |
9 |
2 8
|
sselid |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ℝ* ) |
10 |
|
xmulcom |
⊢ ( ( ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) ) |
11 |
7 9 10
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) ) |
12 |
|
xmulcom |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ·e 𝐶 ) = ( 𝐶 ·e 𝐴 ) ) |
13 |
4 9 12
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ·e 𝐶 ) = ( 𝐶 ·e 𝐴 ) ) |
14 |
|
xmulcom |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) ) |
15 |
6 9 14
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) ) |
16 |
13 15
|
oveq12d |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) ) |
17 |
1 11 16
|
3eqtr3d |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) ) |