Theorem List for Intuitionistic Logic Explorer - 11301-11400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fisumss 11301* |
Change the index set to a subset in a finite sum. (Contributed by Mario
Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) & ⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
& ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
|
Theorem | isumss2 11302* |
Change the index set of a sum by adding zeroes. The nonzero elements
are in the contained set 𝐴 and the added zeroes compose the
rest of
the containing set 𝐵 which needs to be summable.
(Contributed by
Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵)
& ⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
& ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) & ⊢ (𝜑 → ((𝑀 ∈ ℤ ∧ 𝐵 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐵) ∨ 𝐵 ∈ Fin))
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐴, 𝐶, 0)) |
|
Theorem | fsum3cvg2 11303* |
The sequence of partial sums of a finite sum converges to the whole sum.
(Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon,
2-Dec-2022.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |
|
Theorem | fsumsersdc 11304* |
Special case of series sum over a finite upper integer index set.
(Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Jim
Kingdon, 5-May-2023.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq𝑀( + , 𝐹)‘𝑁)) |
|
Theorem | fsum3cvg3 11305* |
A finite sum is convergent. (Contributed by Mario Carneiro,
24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
|
Theorem | fsum3ser 11306* |
A finite sum expressed in terms of a partial sum of an infinite series.
The recursive definition follows as fsum1 11321 and fsump1 11329, which should
make our notation clear and from which, along with closure fsumcl 11309, we
will derive the basic properties of finite sums. (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( + , 𝐹)‘𝑁)) |
|
Theorem | fsumcl2lem 11307* |
- Lemma for finite sum closures. (The "-" before "Lemma"
forces the
math content to be displayed in the Statement List - NM 11-Feb-2008.)
(Contributed by Mario Carneiro, 3-Jun-2014.)
|
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ≠ ∅)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |
|
Theorem | fsumcllem 11308* |
- Lemma for finite sum closures. (The "-" before "Lemma"
forces the
math content to be displayed in the Statement List - NM 11-Feb-2008.)
(Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro,
3-Jun-2014.)
|
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 0 ∈ 𝑆) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |
|
Theorem | fsumcl 11309* |
Closure of a finite sum of complex numbers 𝐴(𝑘). (Contributed
by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
|
Theorem | fsumrecl 11310* |
Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
|
Theorem | fsumzcl 11311* |
Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.)
(Revised by Mario Carneiro, 22-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℤ) |
|
Theorem | fsumnn0cl 11312* |
Closure of a finite sum of nonnegative integers. (Contributed by
Mario Carneiro, 23-Apr-2015.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℕ0) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈
ℕ0) |
|
Theorem | fsumrpcl 11313* |
Closure of a finite sum of positive reals. (Contributed by Mario
Carneiro, 3-Jun-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℝ+) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈
ℝ+) |
|
Theorem | fsumzcl2 11314* |
A finite sum with integer summands is an integer. (Contributed by
Alexander van der Vekens, 31-Aug-2018.)
|
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℤ) |
|
Theorem | fsumadd 11315* |
The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised
by Mario Carneiro, 22-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)) |
|
Theorem | fsumsplit 11316* |
Split a sum into two parts. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)
|
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) |
|
Theorem | fsumsplitf 11317* |
Split a sum into two parts. A version of fsumsplit 11316 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
⊢ Ⅎ𝑘𝜑
& ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) |
|
Theorem | sumsnf 11318* |
A sum of a singleton is the term. A version of sumsn 11320 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
⊢ Ⅎ𝑘𝐵
& ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵) |
|
Theorem | fsumsplitsn 11319* |
Separate out a term in a finite sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
⊢ Ⅎ𝑘𝜑
& ⊢ Ⅎ𝑘𝐷
& ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷)
& ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∪ {𝐵})𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + 𝐷)) |
|
Theorem | sumsn 11320* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵) |
|
Theorem | fsum1 11321* |
The finite sum of 𝐴(𝑘) from 𝑘 = 𝑀 to 𝑀 (i.e. a sum with
only one term) is 𝐵 i.e. 𝐴(𝑀). (Contributed by NM,
8-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
|
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (𝑀...𝑀)𝐴 = 𝐵) |
|
Theorem | sumpr 11322* |
A sum over a pair is the sum of the elements. (Contributed by Thierry
Arnoux, 12-Dec-2016.)
|
⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)
& ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)
& ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ)) & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 + 𝐸)) |
|
Theorem | sumtp 11323* |
A sum over a triple is the sum of the elements. (Contributed by AV,
24-Jul-2020.)
|
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)
& ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)
& ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺)
& ⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ)) & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐴 ≠ 𝐶)
& ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 + 𝐹) + 𝐺)) |
|
Theorem | sumsns 11324* |
A sum of a singleton is the term. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
⊢ ((𝑀 ∈ 𝑉 ∧ ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ) → Σ𝑘 ∈ {𝑀}𝐴 = ⦋𝑀 / 𝑘⦌𝐴) |
|
Theorem | fsumm1 11325* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 26-Apr-2014.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + 𝐵)) |
|
Theorem | fzosump1 11326* |
Separate out the last term in a finite sum. (Contributed by Mario
Carneiro, 13-Apr-2016.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (𝑀..^𝑁)𝐴 + 𝐵)) |
|
Theorem | fsum1p 11327* |
Separate out the first term in a finite sum. (Contributed by NM,
3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑁)𝐴 = (𝐵 + Σ𝑘 ∈ ((𝑀 + 1)...𝑁)𝐴)) |
|
Theorem | fsumsplitsnun 11328* |
Separate out a term in a finite sum by splitting the sum into two parts.
(Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by AV,
17-Dec-2021.)
|
⊢ ((𝐴 ∈ Fin ∧ (𝑍 ∈ 𝑉 ∧ 𝑍 ∉ 𝐴) ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑍})𝐵 = (Σ𝑘 ∈ 𝐴 𝐵 + ⦋𝑍 / 𝑘⦌𝐵)) |
|
Theorem | fsump1 11329* |
The addition of the next term in a finite sum of 𝐴(𝑘) is the
current term plus 𝐵 i.e. 𝐴(𝑁 + 1). (Contributed by NM,
4-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (𝑀...𝑁)𝐴 + 𝐵)) |
|
Theorem | isumclim 11330* |
An infinite sum equals the value its series converges to.
(Contributed by NM, 25-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = 𝐵) |
|
Theorem | isumclim2 11331* |
A converging series converges to its infinite sum. (Contributed by NM,
2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ 𝑍 𝐴) |
|
Theorem | isumclim3 11332* |
The sequence of partial finite sums of a converging infinite series
converges to the infinite sum of the series. Note that 𝑗 must
not
occur in 𝐴. (Contributed by NM, 9-Jan-2006.)
(Revised by Mario
Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = Σ𝑘 ∈ (𝑀...𝑗)𝐴) ⇒ ⊢ (𝜑 → 𝐹 ⇝ Σ𝑘 ∈ 𝑍 𝐴) |
|
Theorem | sumnul 11333* |
The sum of a non-convergent infinite series evaluates to the empty
set. (Contributed by Paul Chapman, 4-Nov-2007.) (Revised by Mario
Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = ∅) |
|
Theorem | isumcl 11334* |
The sum of a converging infinite series is a complex number.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℂ) |
|
Theorem | isummulc2 11335* |
An infinite sum multiplied by a constant. (Contributed by NM,
12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐵 · Σ𝑘 ∈ 𝑍 𝐴) = Σ𝑘 ∈ 𝑍 (𝐵 · 𝐴)) |
|
Theorem | isummulc1 11336* |
An infinite sum multiplied by a constant. (Contributed by NM,
13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝑍 𝐴 · 𝐵) = Σ𝑘 ∈ 𝑍 (𝐴 · 𝐵)) |
|
Theorem | isumdivapc 11337* |
An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 # 0) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝑍 𝐴 / 𝐵) = Σ𝑘 ∈ 𝑍 (𝐴 / 𝐵)) |
|
Theorem | isumrecl 11338* |
The sum of a converging infinite real series is a real number.
(Contributed by Mario Carneiro, 24-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℝ) |
|
Theorem | isumge0 11339* |
An infinite sum of nonnegative terms is nonnegative. (Contributed by
Mario Carneiro, 28-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝑍 𝐴) |
|
Theorem | isumadd 11340* |
Addition of infinite sums. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 (𝐴 + 𝐵) = (Σ𝑘 ∈ 𝑍 𝐴 + Σ𝑘 ∈ 𝑍 𝐵)) |
|
Theorem | sumsplitdc 11341* |
Split a sum into two parts. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → DECID 𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → DECID 𝑘 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐶, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = if(𝑘 ∈ 𝐵, 𝐶, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∪ 𝐵)) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) |
|
Theorem | fsump1i 11342* |
Optimized version of fsump1 11329 for making sums of a concrete number of
terms. (Contributed by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝐾 + 1) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐾 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝐾)𝐴 = 𝑆)) & ⊢ (𝜑 → (𝑆 + 𝐵) = 𝑇) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝑁)𝐴 = 𝑇)) |
|
Theorem | fsum2dlemstep 11343* |
Lemma for fsum2d 11344- induction step. (Contributed by Mario
Carneiro,
23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
|
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶)
& ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → ¬ 𝑦 ∈ 𝑥)
& ⊢ (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
& ⊢ (𝜑 → 𝑥 ∈ Fin) & ⊢ (𝜓 ↔ Σ𝑗 ∈ 𝑥 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷) |
|
Theorem | fsum2d 11344* |
Write a double sum as a sum over a two-dimensional region. Note that
𝐵(𝑗) is a function of 𝑗.
(Contributed by Mario Carneiro,
27-Apr-2014.)
|
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶)
& ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷) |
|
Theorem | fsumxp 11345* |
Combine two sums into a single sum over the cartesian product.
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶)
& ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ (𝐴 × 𝐵)𝐷) |
|
Theorem | fsumcnv 11346* |
Transform a region of summation by using the converse operation.
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
⊢ (𝑥 = 〈𝑗, 𝑘〉 → 𝐵 = 𝐷)
& ⊢ (𝑦 = 〈𝑘, 𝑗〉 → 𝐶 = 𝐷)
& ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → Rel 𝐴)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑦 ∈ ◡ 𝐴𝐶) |
|
Theorem | fisumcom2 11347* |
Interchange order of summation. Note that 𝐵(𝑗) and 𝐷(𝑘)
are not necessarily constant expressions. (Contributed by Mario
Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
(Proof shortened by JJ, 2-Aug-2021.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ Fin) & ⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐸 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑘 ∈ 𝐶 Σ𝑗 ∈ 𝐷 𝐸) |
|
Theorem | fsumcom 11348* |
Interchange order of summation. (Contributed by NM, 15-Nov-2005.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝐵 Σ𝑗 ∈ 𝐴 𝐶) |
|
Theorem | fsum0diaglem 11349* |
Lemma for fisum0diag 11350. (Contributed by Mario Carneiro,
28-Apr-2014.)
(Revised by Mario Carneiro, 8-Apr-2016.)
|
⊢ ((𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗))) → (𝑘 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 𝑘)))) |
|
Theorem | fisum0diag 11350* |
Two ways to express "the sum of 𝐴(𝑗, 𝑘) over the triangular
region 𝑀 ≤ 𝑗, 𝑀 ≤ 𝑘, 𝑗 + 𝑘 ≤ 𝑁." (Contributed by NM,
31-Dec-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
(Revised by Mario Carneiro, 8-Apr-2016.)
|
⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗)))) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)Σ𝑘 ∈ (0...(𝑁 − 𝑗))𝐴 = Σ𝑘 ∈ (0...𝑁)Σ𝑗 ∈ (0...(𝑁 − 𝑘))𝐴) |
|
Theorem | mptfzshft 11351* |
1-1 onto function in maps-to notation which shifts a finite set of
sequential integers. (Contributed by AV, 24-Aug-2019.)
|
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → (𝑗 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ (𝑗 − 𝐾)):((𝑀 + 𝐾)...(𝑁 + 𝐾))–1-1-onto→(𝑀...𝑁)) |
|
Theorem | fsumrev 11352* |
Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised
by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = (𝐾 − 𝑘) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝐵) |
|
Theorem | fsumshft 11353* |
Index shift of a finite sum. (Contributed by NM, 27-Nov-2005.)
(Revised by Mario Carneiro, 24-Apr-2014.) (Proof shortened by AV,
8-Sep-2019.)
|
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = (𝑘 − 𝐾) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵) |
|
Theorem | fsumshftm 11354* |
Negative index shift of a finite sum. (Contributed by NM,
28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = (𝑘 + 𝐾) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))𝐵) |
|
Theorem | fisumrev2 11355* |
Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised
by Mario Carneiro, 13-Apr-2016.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑗 = ((𝑀 + 𝑁) − 𝑘) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ (𝑀...𝑁)𝐵) |
|
Theorem | fisum0diag2 11356* |
Two ways to express "the sum of 𝐴(𝑗, 𝑘) over the triangular
region 0 ≤ 𝑗, 0 ≤ 𝑘, 𝑗 + 𝑘 ≤ 𝑁." (Contributed by
Mario Carneiro, 21-Jul-2014.)
|
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐴)
& ⊢ (𝑥 = (𝑘 − 𝑗) → 𝐵 = 𝐶)
& ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑘 ∈ (0...(𝑁 − 𝑗)))) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)Σ𝑘 ∈ (0...(𝑁 − 𝑗))𝐴 = Σ𝑘 ∈ (0...𝑁)Σ𝑗 ∈ (0...𝑘)𝐶) |
|
Theorem | fsummulc2 11357* |
A finite sum multiplied by a constant. (Contributed by NM,
12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐶 · Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐶 · 𝐵)) |
|
Theorem | fsummulc1 11358* |
A finite sum multiplied by a constant. (Contributed by NM,
13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶)) |
|
Theorem | fsumdivapc 11359* |
A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.)
(Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 # 0) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 / 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 / 𝐶)) |
|
Theorem | fsumneg 11360* |
Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.)
(Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -𝐵 = -Σ𝑘 ∈ 𝐴 𝐵) |
|
Theorem | fsumsub 11361* |
Split a finite sum over a subtraction. (Contributed by Scott Fenton,
12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 − 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 − Σ𝑘 ∈ 𝐴 𝐶)) |
|
Theorem | fsum2mul 11362* |
Separate the nested sum of the product 𝐶(𝑗) · 𝐷(𝑘).
(Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 (𝐶 · 𝐷) = (Σ𝑗 ∈ 𝐴 𝐶 · Σ𝑘 ∈ 𝐵 𝐷)) |
|
Theorem | fsumconst 11363* |
The sum of constant terms (𝑘 is not free in 𝐵). (Contributed
by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ 𝐴 𝐵 = ((♯‘𝐴) · 𝐵)) |
|
Theorem | fsumdifsnconst 11364* |
The sum of constant terms (𝑘 is not free in 𝐶) over an index
set excluding a singleton. (Contributed by AV, 7-Jan-2022.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ ℂ) → Σ𝑘 ∈ (𝐴 ∖ {𝐵})𝐶 = (((♯‘𝐴) − 1) · 𝐶)) |
|
Theorem | modfsummodlem1 11365* |
Lemma for modfsummod 11367. (Contributed by Alexander van der Vekens,
1-Sep-2018.)
|
⊢ (∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ) |
|
Theorem | modfsummodlemstep 11366* |
Induction step for modfsummod 11367. (Contributed by Alexander van der
Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)
& ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 mod 𝑁) = (Σ𝑘 ∈ 𝐴 (𝐵 mod 𝑁) mod 𝑁)) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 mod 𝑁) = (Σ𝑘 ∈ (𝐴 ∪ {𝑧})(𝐵 mod 𝑁) mod 𝑁)) |
|
Theorem | modfsummod 11367* |
A finite sum modulo a positive integer equals the finite sum of their
summands modulo the positive integer, modulo the positive integer.
(Contributed by Alexander van der Vekens, 1-Sep-2018.)
|
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ)
⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 mod 𝑁) = (Σ𝑘 ∈ 𝐴 (𝐵 mod 𝑁) mod 𝑁)) |
|
Theorem | fsumge0 11368* |
If all of the terms of a finite sum are nonnegative, so is the sum.
(Contributed by NM, 26-Dec-2005.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝐴 𝐵) |
|
Theorem | fsumlessfi 11369* |
A shorter sum of nonnegative terms is no greater than a longer one.
(Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon,
12-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)
& ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
& ⊢ (𝜑 → 𝐶 ∈ Fin) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) |
|
Theorem | fsumge1 11370* |
A sum of nonnegative numbers is greater than or equal to any one of
its terms. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof
shortened by Mario Carneiro, 4-Jun-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)
& ⊢ (𝑘 = 𝑀 → 𝐵 = 𝐶)
& ⊢ (𝜑 → 𝑀 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ≤ Σ𝑘 ∈ 𝐴 𝐵) |
|
Theorem | fsum00 11371* |
A sum of nonnegative numbers is zero iff all terms are zero.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∀𝑘 ∈ 𝐴 𝐵 = 0)) |
|
Theorem | fsumle 11372* |
If all of the terms of finite sums compare, so do the sums.
(Contributed by NM, 11-Dec-2005.) (Proof shortened by Mario Carneiro,
24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐶) |
|
Theorem | fsumlt 11373* |
If every term in one finite sum is less than the corresponding term in
another, then the first sum is less than the second. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 < Σ𝑘 ∈ 𝐴 𝐶) |
|
Theorem | fsumabs 11374* |
Generalized triangle inequality: the absolute value of a finite sum is
less than or equal to the sum of absolute values. (Contributed by NM,
9-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (abs‘Σ𝑘 ∈ 𝐴 𝐵) ≤ Σ𝑘 ∈ 𝐴 (abs‘𝐵)) |
|
Theorem | telfsumo 11375* |
Sum of a telescoping series, using half-open intervals. (Contributed by
Mario Carneiro, 2-May-2016.)
|
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)
& ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)
& ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)
& ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸)) |
|
Theorem | telfsumo2 11376* |
Sum of a telescoping series. (Contributed by Mario Carneiro,
2-May-2016.)
|
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)
& ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)
& ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)
& ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐸)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐶 − 𝐵) = (𝐸 − 𝐷)) |
|
Theorem | telfsum 11377* |
Sum of a telescoping series. (Contributed by Scott Fenton,
24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)
& ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)
& ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)
& ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸)
& ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)(𝐵 − 𝐶) = (𝐷 − 𝐸)) |
|
Theorem | telfsum2 11378* |
Sum of a telescoping series. (Contributed by Mario Carneiro,
15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|
⊢ (𝑘 = 𝑗 → 𝐴 = 𝐵)
& ⊢ (𝑘 = (𝑗 + 1) → 𝐴 = 𝐶)
& ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷)
& ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸)
& ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)(𝐶 − 𝐵) = (𝐸 − 𝐷)) |
|
Theorem | fsumparts 11379* |
Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
|
⊢ (𝑘 = 𝑗 → (𝐴 = 𝐵 ∧ 𝑉 = 𝑊)) & ⊢ (𝑘 = (𝑗 + 1) → (𝐴 = 𝐶 ∧ 𝑉 = 𝑋)) & ⊢ (𝑘 = 𝑀 → (𝐴 = 𝐷 ∧ 𝑉 = 𝑌)) & ⊢ (𝑘 = 𝑁 → (𝐴 = 𝐸 ∧ 𝑉 = 𝑍)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑉 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀..^𝑁)(𝐵 · (𝑋 − 𝑊)) = (((𝐸 · 𝑍) − (𝐷 · 𝑌)) − Σ𝑗 ∈ (𝑀..^𝑁)((𝐶 − 𝐵) · 𝑋))) |
|
Theorem | fsumrelem 11380* |
Lemma for fsumre 11381, fsumim 11382, and fsumcj 11383. (Contributed by Mario
Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐹:ℂ⟶ℂ & ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵)) |
|
Theorem | fsumre 11381* |
The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℜ‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (ℜ‘𝐵)) |
|
Theorem | fsumim 11382* |
The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (ℑ‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (ℑ‘𝐵)) |
|
Theorem | fsumcj 11383* |
The complex conjugate of a sum. (Contributed by Paul Chapman,
9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (∗‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (∗‘𝐵)) |
|
Theorem | iserabs 11384* |
Generalized triangle inequality: the absolute value of an infinite sum
is less than or equal to the sum of absolute values. (Contributed by
Paul Chapman, 10-Sep-2007.) (Revised by Jim Kingdon, 14-Dec-2022.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)
& ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ 𝐵)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (abs‘𝐴) ≤ 𝐵) |
|
Theorem | cvgcmpub 11385* |
An upper bound for the limit of a real infinite series. This theorem
can also be used to compare two infinite series. (Contributed by Mario
Carneiro, 24-Mar-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)
& ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) |
|
Theorem | fsumiun 11386* |
Sum over a disjoint indexed union. (Contributed by Mario Carneiro,
1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶) |
|
Theorem | hashiun 11387* |
The cardinality of a disjoint indexed union. (Contributed by Mario
Carneiro, 24-Jan-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ𝑥 ∈ 𝐴 (♯‘𝐵)) |
|
Theorem | hash2iun 11388* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 (♯‘𝐶)) |
|
Theorem | hash2iun1dif1 11389* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ 𝐵 = (𝐴 ∖ {𝑥})
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (♯‘𝐶) = 1) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = ((♯‘𝐴) · ((♯‘𝐴) − 1))) |
|
Theorem | hashrabrex 11390* |
The number of elements in a class abstraction with a restricted
existential quantification. (Contributed by Alexander van der Vekens,
29-Jul-2018.)
|
⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → {𝑥 ∈ 𝑋 ∣ 𝜓} ∈ Fin) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ 𝜓}) ⇒ ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 𝜓}) = Σ𝑦 ∈ 𝑌 (♯‘{𝑥 ∈ 𝑋 ∣ 𝜓})) |
|
Theorem | hashuni 11391* |
The cardinality of a disjoint union. (Contributed by Mario Carneiro,
24-Jan-2015.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) ⇒ ⊢ (𝜑 → (♯‘∪ 𝐴)
= Σ𝑥 ∈ 𝐴 (♯‘𝑥)) |
|
4.8.3 The binomial theorem
|
|
Theorem | binomlem 11392* |
Lemma for binom 11393 (binomial theorem). Inductive step.
(Contributed by
NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜓 → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵)↑(𝑁 + 1)) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))) |
|
Theorem | binom 11393* |
The binomial theorem: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to
𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). Theorem
15-2.8 of [Gleason] p. 296. This part
of the proof sets up the
induction and does the base case, with the bulk of the work (the
induction step) in binomlem 11392. This is Metamath 100 proof #44.
(Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro,
24-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)))) |
|
Theorem | binom1p 11394* |
Special case of the binomial theorem for (1 + 𝐴)↑𝑁.
(Contributed by Paul Chapman, 10-May-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((1 +
𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) |
|
Theorem | binom11 11395* |
Special case of the binomial theorem for 2↑𝑁. (Contributed by
Mario Carneiro, 13-Mar-2014.)
|
⊢ (𝑁 ∈ ℕ0 →
(2↑𝑁) = Σ𝑘 ∈ (0...𝑁)(𝑁C𝑘)) |
|
Theorem | binom1dif 11396* |
A summation for the difference between ((𝐴 + 1)↑𝑁) and
(𝐴↑𝑁). (Contributed by Scott Fenton,
9-Apr-2014.) (Revised by
Mario Carneiro, 22-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) →
(((𝐴 + 1)↑𝑁) − (𝐴↑𝑁)) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘))) |
|
Theorem | bcxmaslem1 11397 |
Lemma for bcxmas 11398. (Contributed by Paul Chapman,
18-May-2007.)
|
⊢ (𝐴 = 𝐵 → ((𝑁 + 𝐴)C𝐴) = ((𝑁 + 𝐵)C𝐵)) |
|
Theorem | bcxmas 11398* |
Parallel summation (Christmas Stocking) theorem for Pascal's Triangle.
(Contributed by Paul Chapman, 18-May-2007.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (((𝑁 + 1) + 𝑀)C𝑀) = Σ𝑗 ∈ (0...𝑀)((𝑁 + 𝑗)C𝑗)) |
|
4.8.4 Infinite sums (cont.)
|
|
Theorem | isumshft 11399* |
Index shift of an infinite sum. (Contributed by Paul Chapman,
31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 =
(ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵) |
|
Theorem | isumsplit 11400* |
Split off the first 𝑁 terms of an infinite sum.
(Contributed by
Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 =
(ℤ≥‘𝑁)
& ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |