Theorem List for Intuitionistic Logic Explorer - 11301-11400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | trireciplem 11301 |
Lemma for trirecip 11302. 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 11302 |
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 11303* |
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 11304* |
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 11305* |
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 11306* |
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 11307* |
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 11308* |
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 11309* |
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 11310 |
Less-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 # 𝐵) |
|
Theorem | absgtap 11311 |
Greater-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 < (abs‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 # 𝐵) |
|
Theorem | geolim 11312* |
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 11313* |
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 11314* |
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 11315* |
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 11316* |
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 11317* |
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 11318* |
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 11319* |
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 11320* |
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 11321* |
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... 11322 |
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 11323 |
Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... =
1. Uses geoisum1 11320. This is a representation of .111... in
binary with
an infinite number of 1's. Theorem 0.999... 11322 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 11324 |
Lemma for cvgratnn 11332. 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 11325* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon, 15-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ)
⇒ ⊢ (𝜑 → (abs‘(𝐹‘𝑁)) ≤ ((abs‘(𝐹‘1)) · (𝐴↑(𝑁 − 1)))) |
|
Theorem | cvgratnnlemmn 11326* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
15-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → (abs‘(𝐹‘𝑁)) ≤ ((abs‘(𝐹‘𝑀)) · (𝐴↑(𝑁 − 𝑀)))) |
|
Theorem | cvgratnnlemseq 11327* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) |
|
Theorem | cvgratnnlemabsle 11328* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) ≤ ((abs‘(𝐹‘𝑀)) · Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)))) |
|
Theorem | cvgratnnlemsumlt 11329* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
23-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)) < (𝐴 / (1 − 𝐴))) |
|
Theorem | cvgratnnlemfm 11330* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon, 23-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ)
⇒ ⊢ (𝜑 → (abs‘(𝐹‘𝑀)) < ((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀)) |
|
Theorem | cvgratnnlemrate 11331* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon, 21-Nov-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) < (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) · (𝐴 / (1 − 𝐴))) / 𝑀)) |
|
Theorem | cvgratnn 11332* |
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 11333 and cvgratgt0 11334, the decision to
index starting at one is not merely cosmetic, as proving convergence
using climcvg1n 11151 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 11333* |
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 11334* |
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 11335* |
Lemma for mertensabs 11338. 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 11336* |
Lemma for mertensabs 11338. (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 11337* |
Lemma for mertensabs 11338. (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 11338* |
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 11339* |
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 11340* |
The limit of an infinite product with an initial segment added.
(Contributed by Scott Fenton, 18-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) |
|
Theorem | clim2divap 11341* |
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 11342* |
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 11343 |
The value of the partial products in a one-valued infinite product.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( · , (𝑍 × {1}))‘𝑁) = 1) |
|
Theorem | prodf1f 11344 |
A one-valued infinite product is equal to the constant one function.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) = (𝑍 × {1})) |
|
Theorem | prodfclim1 11345 |
The constant one product converges to one. (Contributed by Scott
Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) ⇝ 1) |
|
Theorem | prodfap0 11346* |
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 11347* |
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 11348* |
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 11349* |
A non-trivially converging infinite product converges. (Contributed by
Scott Fenton, 18-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
|
Theorem | ntrivcvgap0 11350* |
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 11351 |
Extend class notation to include complex products.
|
class ∏𝑘 ∈ 𝐴 𝐵 |
|
Definition | df-proddc 11352* |
Define the product of a series with an index set of integers 𝐴.
This definition takes most of the aspects of df-sumdc 11155 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 11353 |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
⊢ Ⅎ𝑘𝐴
& ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | prodeq1 11354* |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | nfcprod1 11355* |
Bound-variable hypothesis builder for product. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵 |
|
Theorem | nfcprod 11356* |
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 11357* |
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 11358* |
Equality theorem for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | cbvprod 11359* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
& ⊢ Ⅎ𝑘𝐴
& ⊢ Ⅎ𝑗𝐴
& ⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvprodv 11360* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvprodi 11361* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶
& ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | prodeq1i 11362* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶 |
|
Theorem | prodeq2i 11363* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | prodeq12i 11364* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷 |
|
Theorem | prodeq1d 11365* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | prodeq2d 11366* |
Equality deduction for product. Note that unlike prodeq2dv 11367, 𝑘
may occur in 𝜑. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | prodeq2dv 11367* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | prodeq2sdv 11368* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | 2cprodeq2dv 11369* |
Equality deduction for double product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodeq12dv 11370* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodeq12rdv 11371* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodrbdclem 11372* |
Lemma for prodrbdc 11375. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 4-Apr-2024.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ ((𝜑 ∧ 𝐴 ⊆
(ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾
(ℤ≥‘𝑁)) = seq𝑁( · , 𝐹)) |
|
Theorem | fproddccvg 11373* |
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 11374* |
Lemma for prodrbdc 11375. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID
𝑘 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) |
|
Theorem | prodrbdc 11375* |
Rebase the starting point of a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID
𝑘 ∈ 𝐴) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) |
|
Theorem | prodmodclem3 11376* |
Lemma for prodmodc 11379. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) & ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1)) & ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) & ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)
& ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) ⇒ ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑀) = (seq1( · , 𝐻)‘𝑁)) |
|
Theorem | prodmodclem2a 11377* |
Lemma for prodmodc 11379. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) & ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
& ⊢ (𝜑 → 𝐾 Isom < , <
((1...(♯‘𝐴)),
𝐴)) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁)) |
|
Theorem | prodmodclem2 11378* |
Lemma for prodmodc 11379. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 13-Apr-2024.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) ⇒ ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧)) |
|
Theorem | prodmodc 11379* |
A product has at most one limit. (Contributed by Scott Fenton,
4-Dec-2017.) (Modified by Jim Kingdon, 14-Apr-2024.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) ⇒ ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)))) |
|
Theorem | zproddc 11380* |
Series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
& ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
& ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹))) |
|
Theorem | iprodap 11381* |
Series product with an upper integer index set (i.e. an infinite
product.) (Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹))) |
|
Theorem | zprodap0 11382* |
Nonzero series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 6-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑋 # 0) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)
& ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 𝑋) |
|
Theorem | iprodap0 11383* |
Nonzero series product with an upper integer index set (i.e. an
infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑋 # 0) & ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 𝐵 = 𝑋) |
|
4.8.10.4 Finite products
|
|
Theorem | fprodseq 11384* |
The value of a product over a nonempty finite set. (Contributed by
Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
|
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
& ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)) |
|
4.9 Elementary trigonometry
|
|
4.9.1 The exponential, sine, and cosine
functions
|
|
Syntax | ce 11385 |
Extend class notation to include the exponential function.
|
class exp |
|
Syntax | ceu 11386 |
Extend class notation to include Euler's constant e =
2.71828....
|
class e |
|
Syntax | csin 11387 |
Extend class notation to include the sine function.
|
class sin |
|
Syntax | ccos 11388 |
Extend class notation to include the cosine function.
|
class cos |
|
Syntax | ctan 11389 |
Extend class notation to include the tangent function.
|
class tan |
|
Syntax | cpi 11390 |
Extend class notation to include the constant pi, π
= 3.14159....
|
class π |
|
Definition | df-ef 11391* |
Define the exponential function. Its value at the complex number 𝐴
is (exp‘𝐴) and is called the "exponential
of 𝐴"; see
efval 11404. (Contributed by NM, 14-Mar-2005.)
|
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0
((𝑥↑𝑘) / (!‘𝑘))) |
|
Definition | df-e 11392 |
Define Euler's constant e = 2.71828.... (Contributed
by NM,
14-Mar-2005.)
|
⊢ e = (exp‘1) |
|
Definition | df-sin 11393 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i
· 𝑥)) −
(exp‘(-i · 𝑥))) / (2 · i))) |
|
Definition | df-cos 11394 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i
· 𝑥)) +
(exp‘(-i · 𝑥))) / 2)) |
|
Definition | df-tan 11395 |
Define the tangent function. We define it this way for cmpt 3997,
which
requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario
Carneiro, 14-Mar-2014.)
|
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) /
(cos‘𝑥))) |
|
Definition | df-pi 11396 |
Define the constant pi, π = 3.14159..., which is the
smallest
positive number whose sine is zero. Definition of π in [Gleason]
p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV,
14-Sep-2020.)
|
⊢ π = inf((ℝ+ ∩ (◡sin “ {0})), ℝ, <
) |
|
Theorem | eftcl 11397 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ) |
|
Theorem | reeftcl 11398 |
The terms of the series expansion of the exponential function at a real
number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℝ) |
|
Theorem | eftabs 11399 |
The absolute value of a term in the series expansion of the exponential
function. (Contributed by Paul Chapman, 23-Nov-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) →
(abs‘((𝐴↑𝐾) / (!‘𝐾))) = (((abs‘𝐴)↑𝐾) / (!‘𝐾))) |
|
Theorem | eftvalcn 11400* |
The value of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁))) |