Theorem List for Intuitionistic Logic Explorer - 11101-11200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | climmpt 11101* |
Exhibit a function 𝐺 with the same convergence properties
as the
not-quite-function 𝐹. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴)) |
|
Theorem | 2clim 11102* |
If two sequences converge to each other, they converge to the same
limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario
Carneiro, 31-Jan-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐺 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑥)
& ⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → 𝐺 ⇝ 𝐴) |
|
Theorem | climshftlemg 11103 |
A shifted function converges if the original function converges.
(Contributed by Mario Carneiro, 5-Nov-2013.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ 𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴)) |
|
Theorem | climres 11104 |
A function restricted to upper integers converges iff the original
function converges. (Contributed by Mario Carneiro, 13-Jul-2013.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → ((𝐹 ↾
(ℤ≥‘𝑀)) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴)) |
|
Theorem | climshft 11105 |
A shifted function converges iff the original function converges.
(Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro,
31-Jan-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → ((𝐹 shift 𝑀) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴)) |
|
Theorem | serclim0 11106 |
The zero series converges to zero. (Contributed by Paul Chapman,
9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|
⊢ (𝑀 ∈ ℤ → seq𝑀( + , ((ℤ≥‘𝑀) × {0})) ⇝
0) |
|
Theorem | climshft2 11107* |
A shifted function converges iff the original function converges.
(Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario
Carneiro, 6-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑊)
& ⊢ (𝜑 → 𝐺 ∈ 𝑋)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 𝐾)) = (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴)) |
|
Theorem | climabs0 11108* |
Convergence to zero of the absolute value is equivalent to convergence
to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro,
31-Jan-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ 𝐺 ⇝ 0)) |
|
Theorem | climcn1 11109* |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐻 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐵 ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐹‘𝐴)) |
|
Theorem | climcn2 11110* |
Image of a limit under a continuous map, two-arg version. (Contributed
by Mario Carneiro, 31-Jan-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐷)
& ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐶 ∧ 𝑣 ∈ 𝐷)) → (𝑢𝐹𝑣) ∈ ℂ) & ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐻 ⇝ 𝐵)
& ⊢ (𝜑 → 𝐾 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐶)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) ∈ 𝐷)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾‘𝑘) = ((𝐺‘𝑘)𝐹(𝐻‘𝑘))) ⇒ ⊢ (𝜑 → 𝐾 ⇝ (𝐴𝐹𝐵)) |
|
Theorem | addcn2 11111* |
Complex number addition is a continuous function. Part of Proposition
14-4.16 of [Gleason] p. 243. (We write
out the definition directly
because df-cn and df-cncf are not yet available to us. See addcncntop 12760
for the abbreviated version.) (Contributed by Mario Carneiro,
31-Jan-2014.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) →
∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
|
Theorem | subcn2 11112* |
Complex number subtraction is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by Mario
Carneiro, 31-Jan-2014.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) →
∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴)) |
|
Theorem | mulcn2 11113* |
Complex number multiplication is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by Mario
Carneiro, 31-Jan-2014.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) →
∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴)) |
|
Theorem | reccn2ap 11114* |
The reciprocal function is continuous. The class 𝑇 is just for
convenience in writing the proof and typically would be passed in as an
instance of eqid 2140. (Contributed by Mario Carneiro,
9-Feb-2014.)
Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.)
|
⊢ 𝑇 = (inf({1, ((abs‘𝐴) · 𝐵)}, ℝ, < ) ·
((abs‘𝐴) /
2)) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝐵 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 0} ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵)) |
|
Theorem | cn1lem 11115* |
A sufficient condition for a function to be continuous. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
⊢ 𝐹:ℂ⟶ℂ & ⊢ ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) →
(abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) ≤ (abs‘(𝑧 − 𝐴))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐴))) < 𝑥)) |
|
Theorem | abscn2 11116* |
The absolute value function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((abs‘𝑧) − (abs‘𝐴))) < 𝑥)) |
|
Theorem | cjcn2 11117* |
The complex conjugate function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((∗‘𝑧) − (∗‘𝐴))) < 𝑥)) |
|
Theorem | recn2 11118* |
The real part function is continuous. (Contributed by Mario Carneiro,
9-Feb-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℜ‘𝑧) − (ℜ‘𝐴))) < 𝑥)) |
|
Theorem | imcn2 11119* |
The imaginary part function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((ℑ‘𝑧) − (ℑ‘𝐴))) < 𝑥)) |
|
Theorem | climcn1lem 11120* |
The limit of a continuous function, theorem form. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ 𝐻:ℂ⟶ℂ & ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ ∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℂ ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((𝐻‘𝑧) − (𝐻‘𝐴))) < 𝑥))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐻‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (𝐻‘𝐴)) |
|
Theorem | climabs 11121* |
Limit of the absolute value of a sequence. Proposition 12-2.4(c) of
[Gleason] p. 172. (Contributed by NM,
7-Jun-2006.) (Revised by Mario
Carneiro, 9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (abs‘𝐴)) |
|
Theorem | climcj 11122* |
Limit of the complex conjugate of a sequence. Proposition 12-2.4(c)
of [Gleason] p. 172. (Contributed by
NM, 7-Jun-2006.) (Revised by
Mario Carneiro, 9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (∗‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (∗‘𝐴)) |
|
Theorem | climre 11123* |
Limit of the real part of a sequence. Proposition 12-2.4(c) of
[Gleason] p. 172. (Contributed by NM,
7-Jun-2006.) (Revised by Mario
Carneiro, 9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (ℜ‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (ℜ‘𝐴)) |
|
Theorem | climim 11124* |
Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of
[Gleason] p. 172. (Contributed by NM,
7-Jun-2006.) (Revised by Mario
Carneiro, 9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (ℑ‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (ℑ‘𝐴)) |
|
Theorem | climrecl 11125* |
The limit of a convergent real sequence is real. Corollary 12-2.5 of
[Gleason] p. 172. (Contributed by NM,
10-Sep-2005.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | climge0 11126* |
A nonnegative sequence converges to a nonnegative number. (Contributed
by NM, 11-Sep-2005.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) |
|
Theorem | climadd 11127* |
Limit of the sum of two converging sequences. Proposition 12-2.1(a)
of [Gleason] p. 168. (Contributed
by NM, 24-Sep-2005.) (Proof
shortened by Mario Carneiro, 31-Jan-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐻 ∈ 𝑋)
& ⊢ (𝜑 → 𝐺 ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 + 𝐵)) |
|
Theorem | climmul 11128* |
Limit of the product of two converging sequences. Proposition
12-2.1(c) of [Gleason] p. 168.
(Contributed by NM, 27-Dec-2005.)
(Proof shortened by Mario Carneiro, 1-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐻 ∈ 𝑋)
& ⊢ (𝜑 → 𝐺 ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 · 𝐵)) |
|
Theorem | climsub 11129* |
Limit of the difference of two converging sequences. Proposition
12-2.1(b) of [Gleason] p. 168.
(Contributed by NM, 4-Aug-2007.)
(Proof shortened by Mario Carneiro, 1-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐻 ∈ 𝑋)
& ⊢ (𝜑 → 𝐺 ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐴 − 𝐵)) |
|
Theorem | climaddc1 11130* |
Limit of a constant 𝐶 added to each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
3-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = ((𝐹‘𝑘) + 𝐶)) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (𝐴 + 𝐶)) |
|
Theorem | climaddc2 11131* |
Limit of a constant 𝐶 added to each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
3-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 + (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (𝐶 + 𝐴)) |
|
Theorem | climmulc2 11132* |
Limit of a sequence multiplied by a constant 𝐶. Corollary
12-2.2 of [Gleason] p. 171.
(Contributed by NM, 24-Sep-2005.)
(Revised by Mario Carneiro, 3-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 · (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (𝐶 · 𝐴)) |
|
Theorem | climsubc1 11133* |
Limit of a constant 𝐶 subtracted from each term of a
sequence.
(Contributed by Mario Carneiro, 9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = ((𝐹‘𝑘) − 𝐶)) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (𝐴 − 𝐶)) |
|
Theorem | climsubc2 11134* |
Limit of a constant 𝐶 minus each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 − (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐺 ⇝ (𝐶 − 𝐴)) |
|
Theorem | climle 11135* |
Comparison of the limits of two sequences. (Contributed by Paul
Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | climsqz 11136* |
Convergence of a sequence sandwiched between another converging
sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by
Mario Carneiro, 3-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐺 ⇝ 𝐴) |
|
Theorem | climsqz2 11137* |
Convergence of a sequence sandwiched between another converging
sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised
by Mario Carneiro, 3-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ≤ (𝐹‘𝑘))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → 𝐺 ⇝ 𝐴) |
|
Theorem | clim2ser 11138* |
The limit of an infinite series with an initial segment removed.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 1-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹) ⇝ (𝐴 − (seq𝑀( + , 𝐹)‘𝑁))) |
|
Theorem | clim2ser2 11139* |
The limit of an infinite series with an initial segment added.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 1-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( + , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (𝐴 + (seq𝑀( + , 𝐹)‘𝑁))) |
|
Theorem | iserex 11140* |
An infinite series converges, if and only if the series does with
initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.)
(Revised by Mario Carneiro, 27-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ )) |
|
Theorem | isermulc2 11141* |
Multiplication of an infinite series by a constant. (Contributed by
Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐶 · (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ (𝐶 · 𝐴)) |
|
Theorem | climlec2 11142* |
Comparison of a constant to the limit of a sequence. (Contributed by
NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | iserle 11143* |
Comparison of the limits of two infinite series. (Contributed by Paul
Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)
& ⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | iserge0 11144* |
The limit of an infinite series of nonnegative reals is nonnegative.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 3-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) |
|
Theorem | climub 11145* |
The limit of a monotonic sequence is an upper bound. (Contributed by
NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ≤ 𝐴) |
|
Theorem | climserle 11146* |
The partial sums of a converging infinite series with nonnegative
terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.)
(Revised by Mario Carneiro, 9-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ≤ 𝐴) |
|
Theorem | iser3shft 11147* |
Index shift of the limit of an infinite series. (Contributed by Mario
Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.)
|
⊢ (𝜑 → 𝐹 ∈ 𝑉)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ seq(𝑀 + 𝑁)( + , (𝐹 shift 𝑁)) ⇝ 𝐴)) |
|
Theorem | climcau 11148* |
A converging sequence of complex numbers is a Cauchy sequence. The
converse would require excluded middle or a different definition of
Cauchy sequence (for example, fixing a rate of convergence as in
climcvg1n 11151). Theorem 12-5.3 of [Gleason] p. 180 (necessity part).
(Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) |
|
Theorem | climrecvg1n 11149* |
A Cauchy sequence of real numbers converges, existence version. The
rate of convergence is fixed: all terms after the nth term must be
within 𝐶 / 𝑛 of the nth term, where 𝐶 is a
constant multiplier.
(Contributed by Jim Kingdon, 23-Aug-2021.)
|
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛)) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) |
|
Theorem | climcvg1nlem 11150* |
Lemma for climcvg1n 11151. We construct sequences of the real and
imaginary parts of each term of 𝐹, show those converge, and use
that to show that 𝐹 converges. (Contributed by Jim
Kingdon,
24-Aug-2021.)
|
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛))
& ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ (ℜ‘(𝐹‘𝑥))) & ⊢ 𝐻 = (𝑥 ∈ ℕ ↦
(ℑ‘(𝐹‘𝑥))) & ⊢ 𝐽 = (𝑥 ∈ ℕ ↦ (i · (𝐻‘𝑥))) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) |
|
Theorem | climcvg1n 11151* |
A Cauchy sequence of complex numbers converges, existence version.
The rate of convergence is fixed: all terms after the nth term must be
within 𝐶 / 𝑛 of the nth term, where 𝐶 is a
constant
multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
|
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛)) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) |
|
Theorem | climcaucn 11152* |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 11148 but adds the part that (𝐹‘𝑘) is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
|
Theorem | serf0 11153* |
If an infinite series converges, its underlying sequence converges to
zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro,
16-Feb-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉)
& ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) |
|
4.8.2 Finite and infinite sums
|
|
Syntax | csu 11154 |
Extend class notation to include finite summations. (An underscore was
added to the ASCII token in order to facilitate set.mm text searches,
since "sum" is a commonly used word in comments.)
|
class Σ𝑘 ∈ 𝐴 𝐵 |
|
Definition | df-sumdc 11155* |
Define the sum of a series with an index set of integers 𝐴. 𝑘
is normally a free variable in 𝐵, i.e. 𝐵 can be thought of as
𝐵(𝑘). This definition is the result of a
collection of
discussions over the most general definition for a sum that does not
need the index set to have a specified ordering. This definition is in
two parts, one for finite sums and one for subsets of the upper
integers. When summing over a subset of the upper integers, we extend
the index set to the upper integers by adding zero outside the domain,
and then sum the set in order, setting the result to the limit of the
partial sums, if it exists. This means that conditionally convergent
sums can be evaluated meaningfully. For finite sums, we are explicitly
order-independent, by picking any bijection to a 1-based finite sequence
and summing in the induced order. In both cases we have an if
expression so that we only need 𝐵 to be defined where 𝑘 ∈ 𝐴.
In the infinite case, we also require that the indexing set be a
decidable subset of an upperset of integers (that is, membership of
integers in it is decidable). These two methods of summation produce
the same result on their common region of definition (i.e. finite sets
of integers). Examples: Σ𝑘 ∈ {1, 2, 4} 𝑘 means
1 + 2 + 4 = 7, and Σ𝑘 ∈ ℕ (1 / (2↑𝑘))
= 1 means
1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 11323). (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
|
⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) |
|
Theorem | sumeq1 11156 |
Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jun-2019.)
|
⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
|
Theorem | nfsum1 11157 |
Bound-variable hypothesis builder for sum. (Contributed by NM,
11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘Σ𝑘 ∈ 𝐴 𝐵 |
|
Theorem | nfsum 11158 |
Bound-variable hypothesis builder for sum: if 𝑥 is (effectively) not
free in 𝐴 and 𝐵, it is not free in Σ𝑘 ∈
𝐴𝐵.
(Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro,
13-Jun-2019.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥Σ𝑘 ∈ 𝐴 𝐵 |
|
Theorem | sumdc 11159* |
Decidability of a subset of upper integers. (Contributed by Jim
Kingdon, 1-Jan-2022.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → ∀𝑥 ∈
(ℤ≥‘𝑀)DECID 𝑥 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → DECID 𝑁 ∈ 𝐴) |
|
Theorem | sumeq2 11160* |
Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jul-2013.)
|
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) |
|
Theorem | cbvsum 11161 |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jun-2019.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
& ⊢ Ⅎ𝑘𝐴
& ⊢ Ⅎ𝑗𝐴
& ⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvsumv 11162* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvsumi 11163* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|
⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶
& ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 |
|
Theorem | sumeq1i 11164* |
Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶 |
|
Theorem | sumeq2i 11165* |
Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 |
|
Theorem | sumeq12i 11166* |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷 |
|
Theorem | sumeq1d 11167* |
Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
|
Theorem | sumeq2d 11168* |
Equality deduction for sum. Note that unlike sumeq2dv 11169, 𝑘 may
occur in 𝜑. (Contributed by NM, 1-Nov-2005.)
|
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) |
|
Theorem | sumeq2dv 11169* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) |
|
Theorem | sumeq2ad 11170* |
Equality deduction for sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) |
|
Theorem | sumeq2sdv 11171* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶) |
|
Theorem | 2sumeq2dv 11172* |
Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐷) |
|
Theorem | sumeq12dv 11173* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) |
|
Theorem | sumeq12rdv 11174* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) |
|
Theorem | sumfct 11175* |
A lemma to facilitate conversions from the function form to the
class-variable form of a sum. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.)
|
⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → Σ𝑗 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = Σ𝑘 ∈ 𝐴 𝐵) |
|
Theorem | fz1f1o 11176* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
|
Theorem | nnf1o 11177 |
Lemma for sum and product theorems. (Contributed by Jim Kingdon,
15-Aug-2022.)
|
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) & ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
& ⊢ (𝜑 → 𝐺:(1...𝑁)–1-1-onto→𝐴) ⇒ ⊢ (𝜑 → 𝑁 = 𝑀) |
|
Theorem | sumrbdclem 11178* |
Lemma for sumrbdc 11180. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ ((𝜑 ∧ 𝐴 ⊆
(ℤ≥‘𝑁)) → (seq𝑀( + , 𝐹) ↾
(ℤ≥‘𝑁)) = seq𝑁( + , 𝐹)) |
|
Theorem | fsum3cvg 11179* |
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, 12-Nov-2022.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘𝑁)) |
|
Theorem | sumrbdc 11180* |
Rebase the starting point of a sum. (Contributed by Mario Carneiro,
14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID
𝑘 ∈ 𝐴) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐶 ↔ seq𝑁( + , 𝐹) ⇝ 𝐶)) |
|
Theorem | summodclem3 11181* |
Lemma for summodc 11184. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) & ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)
& ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
& ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0)) ⇒ ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |
|
Theorem | summodclem2a 11182* |
Lemma for summodc 11184. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
& ⊢ (𝜑 → 𝐾 Isom < , <
((1...(♯‘𝐴)),
𝐴)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁)) |
|
Theorem | summodclem2 11183* |
Lemma for summodc 11184. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) ⇒ ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦)) |
|
Theorem | summodc 11184* |
A sum has at most one limit. (Contributed by Mario Carneiro,
3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) ⇒ ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)))) |
|
Theorem | zsumdc 11185* |
Series sum with index set a subset of the upper integers.
(Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim
Kingdon, 8-Apr-2023.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 DECID 𝑥 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹))) |
|
Theorem | isum 11186* |
Series sum with an upper integer index set (i.e. an infinite series).
(Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario
Carneiro, 7-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹))) |
|
Theorem | fsumgcl 11187* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
& ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ) |
|
Theorem | fsum3 11188* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
& ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)) |
|
Theorem | sum0 11189 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|
⊢ Σ𝑘 ∈ ∅ 𝐴 = 0 |
|
Theorem | isumz 11190* |
Any sum of zero over a summable set is zero. (Contributed by Mario
Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∨ 𝐴 ∈ Fin) → Σ𝑘 ∈ 𝐴 0 = 0) |
|
Theorem | fsumf1o 11191* |
Re-index a finite sum using a bijection. (Contributed by Mario
Carneiro, 20-Apr-2014.)
|
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
& ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)
& ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |
|
Theorem | isumss 11192* |
Change the index set to a subset in an upper integer sum.
(Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim
Kingdon, 21-Sep-2022.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) & ⊢ (𝜑 → ∀𝑗 ∈
(ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → ∀𝑗 ∈
(ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
|
Theorem | fisumss 11193* |
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 11194* |
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 11195* |
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 11196* |
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 11197* |
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 11198* |
A finite sum expressed in terms of a partial sum of an infinite series.
The recursive definition follows as fsum1 11213 and fsump1 11221, which should
make our notation clear and from which, along with closure fsumcl 11201, 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 11199* |
- 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 11200* |
- 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 ∈ 𝑆) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |