Metamath Proof Explorer

Theorem esumdivc

Description: An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Hypotheses esumdivc.a ⊢ φ → A ∈ V
esumdivc.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
esumdivc.c ⊢ φ → C ∈ ℝ +
Assertion esumdivc ⊢ φ → ∑ * k ∈ A B ÷ 𝑒 C = ∑ * k ∈ A B ÷ 𝑒 C

Proof

Step Hyp Ref Expression
1 esumdivc.a ⊢ φ → A ∈ V
2 esumdivc.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
3 esumdivc.c ⊢ φ → C ∈ ℝ +
4 1red ⊢ φ → 1 ∈ ℝ
5 3 rpred ⊢ φ → C ∈ ℝ
6 3 rpne0d ⊢ φ → C ≠ 0
7 rexdiv ⊢ 1 ∈ ℝ ∧ C ∈ ℝ ∧ C ≠ 0 → 1 ÷ 𝑒 C = 1 C
8 4 5 6 7 syl3anc ⊢ φ → 1 ÷ 𝑒 C = 1 C
9 ioorp ⊢ 0 +∞ = ℝ +
10 ioossico ⊢ 0 +∞ ⊆ 0 +∞
11 9 10 eqsstrri ⊢ ℝ + ⊆ 0 +∞
12 3 rpreccld ⊢ φ → 1 C ∈ ℝ +
13 11 12 sselid ⊢ φ → 1 C ∈ 0 +∞
14 8 13 eqeltrd ⊢ φ → 1 ÷ 𝑒 C ∈ 0 +∞
15 1 2 14 esummulc1 ⊢ φ → ∑ * k ∈ A B ⋅ 𝑒 1 ÷ 𝑒 C = ∑ * k ∈ A B ⋅ 𝑒 1 ÷ 𝑒 C
16 iccssxr ⊢ 0 +∞ ⊆ ℝ *
17 2 ralrimiva ⊢ φ → ∀ k ∈ A B ∈ 0 +∞
18 nfcv ⊢ Ⅎ _ k A
19 18 esumcl ⊢ A ∈ V ∧ ∀ k ∈ A B ∈ 0 +∞ → ∑ * k ∈ A B ∈ 0 +∞
20 1 17 19 syl2anc ⊢ φ → ∑ * k ∈ A B ∈ 0 +∞
21 16 20 sselid ⊢ φ → ∑ * k ∈ A B ∈ ℝ *
22 xdivrec ⊢ ∑ * k ∈ A B ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → ∑ * k ∈ A B ÷ 𝑒 C = ∑ * k ∈ A B ⋅ 𝑒 1 ÷ 𝑒 C
23 21 5 6 22 syl3anc ⊢ φ → ∑ * k ∈ A B ÷ 𝑒 C = ∑ * k ∈ A B ⋅ 𝑒 1 ÷ 𝑒 C
24 16 2 sselid ⊢ φ ∧ k ∈ A → B ∈ ℝ *
25 5 adantr ⊢ φ ∧ k ∈ A → C ∈ ℝ
26 6 adantr ⊢ φ ∧ k ∈ A → C ≠ 0
27 xdivrec ⊢ B ∈ ℝ * ∧ C ∈ ℝ ∧ C ≠ 0 → B ÷ 𝑒 C = B ⋅ 𝑒 1 ÷ 𝑒 C
28 24 25 26 27 syl3anc ⊢ φ ∧ k ∈ A → B ÷ 𝑒 C = B ⋅ 𝑒 1 ÷ 𝑒 C
29 28 esumeq2dv ⊢ φ → ∑ * k ∈ A B ÷ 𝑒 C = ∑ * k ∈ A B ⋅ 𝑒 1 ÷ 𝑒 C
30 15 23 29 3eqtr4d ⊢ φ → ∑ * k ∈ A B ÷ 𝑒 C = ∑ * k ∈ A B ÷ 𝑒 C