Theorem List for Intuitionistic Logic Explorer - 11401-11500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fsumcj 11401* |
The complex conjugate of a sum. (Contributed by Paul Chapman,
9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (∗‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (∗‘𝐵)) |
|
Theorem | iserabs 11402* |
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 11403* |
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 11404* |
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 11405* |
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 11406* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 (♯‘𝐶)) |
|
Theorem | hash2iun1dif1 11407* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ 𝐵 = (𝐴 ∖ {𝑥})
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Disj 𝑦 ∈ 𝐵 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (♯‘𝐶) = 1) ⇒ ⊢ (𝜑 → (♯‘∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶) = ((♯‘𝐴) · ((♯‘𝐴) − 1))) |
|
Theorem | hashrabrex 11408* |
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 11409* |
The cardinality of a disjoint union. (Contributed by Mario Carneiro,
24-Jan-2015.)
|
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) ⇒ ⊢ (𝜑 → (♯‘∪ 𝐴)
= Σ𝑥 ∈ 𝐴 (♯‘𝑥)) |
|
4.8.3 The binomial theorem
|
|
Theorem | binomlem 11410* |
Lemma for binom 11411 (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 11411* |
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 11410. 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 11412* |
Special case of the binomial theorem for (1 + 𝐴)↑𝑁.
(Contributed by Paul Chapman, 10-May-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((1 +
𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) |
|
Theorem | binom11 11413* |
Special case of the binomial theorem for 2↑𝑁. (Contributed by
Mario Carneiro, 13-Mar-2014.)
|
⊢ (𝑁 ∈ ℕ0 →
(2↑𝑁) = Σ𝑘 ∈ (0...𝑁)(𝑁C𝑘)) |
|
Theorem | binom1dif 11414* |
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 11415 |
Lemma for bcxmas 11416. (Contributed by Paul Chapman,
18-May-2007.)
|
⊢ (𝐴 = 𝐵 → ((𝑁 + 𝐴)C𝐴) = ((𝑁 + 𝐵)C𝐵)) |
|
Theorem | bcxmas 11416* |
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 11417* |
Index shift of an infinite sum. (Contributed by Paul Chapman,
31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 =
(ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝑗 = (𝐾 + 𝑘) → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝑊 𝐴 = Σ𝑘 ∈ 𝑍 𝐵) |
|
Theorem | isumsplit 11418* |
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))𝐴 + Σ𝑘 ∈ 𝑊 𝐴)) |
|
Theorem | isum1p 11419* |
The infinite sum of a converging infinite series equals the first term
plus the infinite sum of the rest of it. (Contributed by NM,
2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = ((𝐹‘𝑀) + Σ𝑘 ∈ (ℤ≥‘(𝑀 + 1))𝐴)) |
|
Theorem | isumnn0nn 11420* |
Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed
by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ (𝑘 = 0 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐴 = (𝐵 + Σ𝑘 ∈ ℕ 𝐴)) |
|
Theorem | isumrpcl 11421* |
The infinite sum of positive reals is positive. (Contributed by Paul
Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 =
(ℤ≥‘𝑁)
& ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐴 ∈
ℝ+) |
|
Theorem | isumle 11422* |
Comparison of two infinite sums. (Contributed by Paul Chapman,
13-Nov-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ≤ Σ𝑘 ∈ 𝑍 𝐵) |
|
Theorem | isumlessdc 11423* |
A finite sum of nonnegative numbers is less than or equal to its limit.
(Contributed by Mario Carneiro, 24-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)
& ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 DECID 𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐵)
& ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝑍 𝐵) |
|
4.8.5 Miscellaneous converging and diverging
sequences
|
|
Theorem | divcnv 11424* |
The sequence of reciprocals of positive integers, multiplied by the
factor 𝐴, converges to zero. (Contributed by
NM, 6-Feb-2008.)
(Revised by Jim Kingdon, 22-Oct-2022.)
|
⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℕ ↦ (𝐴 / 𝑛)) ⇝ 0) |
|
4.8.6 Arithmetic series
|
|
Theorem | arisum 11425* |
Arithmetic series sum of the first 𝑁 positive integers. This is
Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006.) (Proof
shortened by Mario Carneiro, 22-May-2014.)
|
⊢ (𝑁 ∈ ℕ0 →
Σ𝑘 ∈ (1...𝑁)𝑘 = (((𝑁↑2) + 𝑁) / 2)) |
|
Theorem | arisum2 11426* |
Arithmetic series sum of the first 𝑁 nonnegative integers.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV,
2-Aug-2021.)
|
⊢ (𝑁 ∈ ℕ0 →
Σ𝑘 ∈
(0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
|
Theorem | trireciplem 11427 |
Lemma for trirecip 11428. Show that the sum converges. (Contributed
by
Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro,
22-May-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))) ⇒ ⊢ seq1( + , 𝐹) ⇝ 1 |
|
Theorem | trirecip 11428 |
The sum of the reciprocals of the triangle numbers converge to two.
This is Metamath 100 proof #42. (Contributed by Scott Fenton,
23-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|
⊢ Σ𝑘 ∈ ℕ (2 / (𝑘 · (𝑘 + 1))) = 2 |
|
4.8.7 Geometric series
|
|
Theorem | expcnvap0 11429* |
A sequence of powers of a complex number 𝐴 with absolute value
smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.)
(Revised by Jim Kingdon, 23-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) |
|
Theorem | expcnvre 11430* |
A sequence of powers of a nonnegative real number less than one
converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) |
|
Theorem | expcnv 11431* |
A sequence of powers of a complex number 𝐴 with absolute value
smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.)
(Revised by Jim Kingdon, 28-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) <
1) ⇒ ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) |
|
Theorem | explecnv 11432* |
A sequence of terms converges to zero when it is less than powers of a
number 𝐴 whose absolute value is smaller than
1. (Contributed by
NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘(𝐹‘𝑘)) ≤ (𝐴↑𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 0) |
|
Theorem | geosergap 11433* |
The value of the finite geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1) +...
+ 𝐴↑(𝑁 − 1). (Contributed by Mario
Carneiro, 2-May-2016.)
(Revised by Jim Kingdon, 24-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 1) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) = (((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴))) |
|
Theorem | geoserap 11434* |
The value of the finite geometric series 1 + 𝐴↑1 + 𝐴↑2 +...
+ 𝐴↑(𝑁 − 1). This is Metamath 100
proof #66. (Contributed by
NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 1) & ⊢ (𝜑 → 𝑁 ∈
ℕ0) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴))) |
|
Theorem | pwm1geoserap1 11435* |
The n-th power of a number decreased by 1 expressed by the finite
geometric series 1 + 𝐴↑1 + 𝐴↑2 +... + 𝐴↑(𝑁 − 1).
(Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon,
24-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 # 1) ⇒ ⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) |
|
Theorem | absltap 11436 |
Less-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 # 𝐵) |
|
Theorem | absgtap 11437 |
Greater-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 < (abs‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 # 𝐵) |
|
Theorem | geolim 11438* |
The partial sums in the infinite series 1 + 𝐴↑1 + 𝐴↑2...
converge to (1 / (1 − 𝐴)). (Contributed by NM,
15-May-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐴↑𝑘)) ⇒ ⊢ (𝜑 → seq0( + , 𝐹) ⇝ (1 / (1 − 𝐴))) |
|
Theorem | geolim2 11439* |
The partial sums in the geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1)...
converge to ((𝐴↑𝑀) / (1 − 𝐴)). (Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) < 1) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐴↑𝑘)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ ((𝐴↑𝑀) / (1 − 𝐴))) |
|
Theorem | georeclim 11440* |
The limit of a geometric series of reciprocals. (Contributed by Paul
Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 1 < (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = ((1 / 𝐴)↑𝑘)) ⇒ ⊢ (𝜑 → seq0( + , 𝐹) ⇝ (𝐴 / (𝐴 − 1))) |
|
Theorem | geo2sum 11441* |
The value of the finite geometric series 2↑-1 + 2↑-2
+...
+ 2↑-𝑁, multiplied by a constant.
(Contributed by Mario
Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)(𝐴 / (2↑𝑘)) = (𝐴 − (𝐴 / (2↑𝑁)))) |
|
Theorem | geo2sum2 11442* |
The value of the finite geometric series 1 + 2 + 4 + 8
+...
+ 2↑(𝑁 − 1). (Contributed by Mario
Carneiro, 7-Sep-2016.)
|
⊢ (𝑁 ∈ ℕ0 →
Σ𝑘 ∈ (0..^𝑁)(2↑𝑘) = ((2↑𝑁) − 1)) |
|
Theorem | geo2lim 11443* |
The value of the infinite geometric series
2↑-1 + 2↑-2 +... , multiplied by a
constant. (Contributed
by Mario Carneiro, 15-Jun-2014.)
|
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) ⇒ ⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ⇝ 𝐴) |
|
Theorem | geoisum 11444* |
The infinite sum of 1 + 𝐴↑1 + 𝐴↑2... is (1 /
(1 − 𝐴)).
(Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ0
(𝐴↑𝑘) = (1 / (1 − 𝐴))) |
|
Theorem | geoisumr 11445* |
The infinite sum of reciprocals
1 + (1 / 𝐴)↑1 + (1 / 𝐴)↑2... is 𝐴 / (𝐴 − 1).
(Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 1 <
(abs‘𝐴)) →
Σ𝑘 ∈
ℕ0 ((1 / 𝐴)↑𝑘) = (𝐴 / (𝐴 − 1))) |
|
Theorem | geoisum1 11446* |
The infinite sum of 𝐴↑1 + 𝐴↑2... is (𝐴 / (1 − 𝐴)).
(Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ (𝐴↑𝑘) = (𝐴 / (1 − 𝐴))) |
|
Theorem | geoisum1c 11447* |
The infinite sum of 𝐴 · (𝑅↑1) + 𝐴 · (𝑅↑2)... is
(𝐴
· 𝑅) / (1 −
𝑅). (Contributed by
NM, 2-Nov-2007.) (Revised
by Mario Carneiro, 26-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (abs‘𝑅) < 1) → Σ𝑘 ∈ ℕ (𝐴 · (𝑅↑𝑘)) = ((𝐴 · 𝑅) / (1 − 𝑅))) |
|
Theorem | 0.999... 11448 |
The recurring decimal 0.999..., which is defined as the infinite sum 0.9 +
0.09 + 0.009 + ... i.e. 9 / 10↑1 + 9 / 10↑2 + 9
/ 10↑3
+ ..., is exactly equal to 1. (Contributed by NM,
2-Nov-2007.)
(Revised by AV, 8-Sep-2021.)
|
⊢ Σ𝑘 ∈ ℕ (9 / (;10↑𝑘)) = 1 |
|
Theorem | geoihalfsum 11449 |
Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... =
1. Uses geoisum1 11446. This is a representation of .111... in
binary with
an infinite number of 1's. Theorem 0.999... 11448 proves a similar claim for
.999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.)
(Proof shortened by AV, 9-Jul-2022.)
|
⊢ Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 |
|
4.8.8 Ratio test for infinite series
convergence
|
|
Theorem | cvgratnnlembern 11450 |
Lemma for cvgratnn 11458. Upper bound for a geometric progression of
positive ratio less than one. (Contributed by Jim Kingdon,
24-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ (𝜑 → 𝑀 ∈ ℕ)
⇒ ⊢ (𝜑 → (𝐴↑𝑀) < ((1 / ((1 / 𝐴) − 1)) / 𝑀)) |
|
Theorem | cvgratnnlemnexp 11451* |
Lemma for cvgratnn 11458. (Contributed by Jim Kingdon, 15-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ)
⇒ ⊢ (𝜑 → (abs‘(𝐹‘𝑁)) ≤ ((abs‘(𝐹‘1)) · (𝐴↑(𝑁 − 1)))) |
|
Theorem | cvgratnnlemmn 11452* |
Lemma for cvgratnn 11458. (Contributed by Jim Kingdon,
15-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → (abs‘(𝐹‘𝑁)) ≤ ((abs‘(𝐹‘𝑀)) · (𝐴↑(𝑁 − 𝑀)))) |
|
Theorem | cvgratnnlemseq 11453* |
Lemma for cvgratnn 11458. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) |
|
Theorem | cvgratnnlemabsle 11454* |
Lemma for cvgratnn 11458. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) ≤ ((abs‘(𝐹‘𝑀)) · Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)))) |
|
Theorem | cvgratnnlemsumlt 11455* |
Lemma for cvgratnn 11458. (Contributed by Jim Kingdon,
23-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)) < (𝐴 / (1 − 𝐴))) |
|
Theorem | cvgratnnlemfm 11456* |
Lemma for cvgratnn 11458. (Contributed by Jim Kingdon, 23-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ)
⇒ ⊢ (𝜑 → (abs‘(𝐹‘𝑀)) < ((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀)) |
|
Theorem | cvgratnnlemrate 11457* |
Lemma for cvgratnn 11458. (Contributed by Jim Kingdon, 21-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) < (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) · (𝐴 / (1 − 𝐴))) / 𝑀)) |
|
Theorem | cvgratnn 11458* |
Ratio test for convergence of a complex infinite series. If the ratio
𝐴 of the absolute values of successive
terms in an infinite
sequence 𝐹 is less than 1 for all terms, then
the infinite sum of
the terms of 𝐹 converges to a complex number.
Although this
theorem is similar to cvgratz 11459 and cvgratgt0 11460, the decision to
index starting at one is not merely cosmetic, as proving convergence
using climcvg1n 11277 is sensitive to how a sequence is indexed.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
12-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) ⇒ ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ ) |
|
Theorem | cvgratz 11459* |
Ratio test for convergence of a complex infinite series. If the ratio
𝐴 of the absolute values of successive
terms in an infinite sequence
𝐹 is less than 1 for all terms, then
the infinite sum of the terms
of 𝐹 converges to a complex number.
(Contributed by NM,
26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
|
Theorem | cvgratgt0 11460* |
Ratio test for convergence of a complex infinite series. If the ratio
𝐴 of the absolute values of successive
terms in an infinite sequence
𝐹 is less than 1 for all terms beyond
some index 𝐵, then the
infinite sum of the terms of 𝐹 converges to a complex number.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
11-Nov-2022.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 =
(ℤ≥‘𝑁)
& ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
|
4.8.9 Mertens' theorem
|
|
Theorem | mertenslemub 11461* |
Lemma for mertensabs 11464. An upper bound for 𝑇. (Contributed by
Jim Kingdon, 3-Dec-2022.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝
)
& ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑆 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} & ⊢ (𝜑 → 𝑋 ∈ 𝑇)
& ⊢ (𝜑 → 𝑆 ∈ ℕ)
⇒ ⊢ (𝜑 → 𝑋 ≤ Σ𝑛 ∈ (0...(𝑆 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
|
Theorem | mertenslemi1 11462* |
Lemma for mertensabs 11464. (Contributed by Mario Carneiro,
29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) & ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
)
& ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} & ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) & ⊢ (𝜑 → 𝑃 ∈ ℝ) & ⊢ (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1))))) & ⊢ (𝜑 → 0 ≤ 𝑃)
& ⊢ (𝜑 → ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑃) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
|
Theorem | mertenslem2 11463* |
Lemma for mertensabs 11464. (Contributed by Mario Carneiro,
28-Apr-2014.)
|
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) & ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
)
& ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} & ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
|
Theorem | mertensabs 11464* |
Mertens' theorem. If 𝐴(𝑗) is an absolutely convergent series
and
𝐵(𝑘) is convergent, then
(Σ𝑗 ∈ ℕ0𝐴(𝑗) · Σ𝑘 ∈ ℕ0𝐵(𝑘)) =
Σ𝑘 ∈ ℕ0Σ𝑗 ∈ (0...𝑘)(𝐴(𝑗) · 𝐵(𝑘 − 𝑗)) (and
this latter series is convergent). This latter sum is commonly known as
the Cauchy product of the sequences. The proof follows the outline at
http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem.
(Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
& ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) & ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) & ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
)
& ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ ) & ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝
) ⇒ ⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0
𝐵)) |
|
4.8.10 Finite and infinite
products
|
|
4.8.10.1 Product sequences
|
|
Theorem | prodf 11465* |
An infinite product of complex terms is a function from an upper set of
integers to ℂ. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ) |
|
Theorem | clim2prod 11466* |
The limit of an infinite product with an initial segment added.
(Contributed by Scott Fenton, 18-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) |
|
Theorem | clim2divap 11467* |
The limit of an infinite product with an initial segment removed.
(Contributed by Scott Fenton, 20-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝐴)
& ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0) ⇒ ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ (𝐴 / (seq𝑀( · , 𝐹)‘𝑁))) |
|
Theorem | prod3fmul 11468* |
The product of two infinite products. (Contributed by Scott Fenton,
18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , 𝐺)‘𝑁))) |
|
Theorem | prodf1 11469 |
The value of the partial products in a one-valued infinite product.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( · , (𝑍 × {1}))‘𝑁) = 1) |
|
Theorem | prodf1f 11470 |
A one-valued infinite product is equal to the constant one function.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) = (𝑍 × {1})) |
|
Theorem | prodfclim1 11471 |
The constant one product converges to one. (Contributed by Scott
Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) ⇝ 1) |
|
Theorem | prodfap0 11472* |
The product of finitely many terms apart from zero is apart from zero.
(Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon,
23-Mar-2024.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) # 0) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0) |
|
Theorem | prodfrecap 11473* |
The reciprocal of a finite product. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) # 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (1 / (𝐹‘𝑘))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁))) |
|
Theorem | prodfdivap 11474* |
The quotient of two products. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) # 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁))) |
|
4.8.10.2 Non-trivial convergence
|
|
Theorem | ntrivcvgap 11475* |
A non-trivially converging infinite product converges. (Contributed by
Scott Fenton, 18-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
|
Theorem | ntrivcvgap0 11476* |
A product that converges to a value apart from zero converges
non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)
& ⊢ (𝜑 → 𝑋 # 0) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦)) |
|
4.8.10.3 Complex products
|
|
Syntax | cprod 11477 |
Extend class notation to include complex products.
|
class ∏𝑘 ∈ 𝐴 𝐵 |
|
Definition | df-proddc 11478* |
Define the product of a series with an index set of integers 𝐴.
This definition takes most of the aspects of df-sumdc 11281 and adapts them
for multiplication instead of addition. However, we insist that in the
infinite case, there is a nonzero tail of the sequence. This ensures
that the convergence criteria match those of infinite sums.
(Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon,
21-Mar-2024.)
|
⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) |
|
Theorem | prodeq1f 11479 |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
⊢ Ⅎ𝑘𝐴
& ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | prodeq1 11480* |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | nfcprod1 11481* |
Bound-variable hypothesis builder for product. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵 |
|
Theorem | nfcprod 11482* |
Bound-variable hypothesis builder for product: if 𝑥 is (effectively)
not free in 𝐴 and 𝐵, it is not free in ∏𝑘 ∈
𝐴𝐵.
(Contributed by Scott Fenton, 1-Dec-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥∏𝑘 ∈ 𝐴 𝐵 |
|
Theorem | prodeq2w 11483* |
Equality theorem for product, when the class expressions 𝐵 and 𝐶
are equal everywhere. Proved using only Extensionality. (Contributed
by Scott Fenton, 4-Dec-2017.)
|
⊢ (∀𝑘 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | prodeq2 11484* |
Equality theorem for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | cbvprod 11485* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
& ⊢ Ⅎ𝑘𝐴
& ⊢ Ⅎ𝑗𝐴
& ⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvprodv 11486* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvprodi 11487* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶
& ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | prodeq1i 11488* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶 |
|
Theorem | prodeq2i 11489* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | prodeq12i 11490* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷 |
|
Theorem | prodeq1d 11491* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | prodeq2d 11492* |
Equality deduction for product. Note that unlike prodeq2dv 11493, 𝑘
may occur in 𝜑. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | prodeq2dv 11493* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | prodeq2sdv 11494* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | 2cprodeq2dv 11495* |
Equality deduction for double product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodeq12dv 11496* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodeq12rdv 11497* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodrbdclem 11498* |
Lemma for prodrbdc 11501. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 4-Apr-2024.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ ((𝜑 ∧ 𝐴 ⊆
(ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾
(ℤ≥‘𝑁)) = seq𝑁( · , 𝐹)) |
|
Theorem | fproddccvg 11499* |
The sequence of partial products of a finite product converges to
the whole product. (Contributed by Scott Fenton, 4-Dec-2017.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘𝑁)) |
|
Theorem | prodrbdclem2 11500* |
Lemma for prodrbdc 11501. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID
𝑘 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) |