Theorem List for Intuitionistic Logic Explorer - 11301-11400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cvgratz 11301* |
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 11302* |
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 11303* |
Lemma for mertensabs 11306. 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 11304* |
Lemma for mertensabs 11306. (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 11305* |
Lemma for mertensabs 11306. (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 11306* |
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 11307* |
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 11308* |
The limit of an infinite product with an initial segment added.
(Contributed by Scott Fenton, 18-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) ⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) |
|
Theorem | clim2divap 11309* |
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 11310* |
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 11311 |
The value of the partial products in a one-valued infinite product.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( · , (𝑍 × {1}))‘𝑁) = 1) |
|
Theorem | prodf1f 11312 |
A one-valued infinite product is equal to the constant one function.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) = (𝑍 × {1})) |
|
Theorem | prodfclim1 11313 |
The constant one product converges to one. (Contributed by Scott
Fenton, 5-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) ⇝ 1) |
|
Theorem | prodfap0 11314* |
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 11315* |
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 11316* |
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 11317* |
A non-trivially converging infinite product converges. (Contributed by
Scott Fenton, 18-Dec-2017.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
⇒ ⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ ) |
|
Theorem | ntrivcvgap0 11318* |
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 11319 |
Extend class notation to include complex products.
|
class ∏𝑘 ∈ 𝐴 𝐵 |
|
Definition | df-proddc 11320* |
Define the product of a series with an index set of integers 𝐴.
This definition takes most of the aspects of df-sumdc 11123 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 11321 |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
⊢ Ⅎ𝑘𝐴
& ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | prodeq1 11322* |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | nfcprod1 11323* |
Bound-variable hypothesis builder for product. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵 |
|
Theorem | nfcprod 11324* |
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 11325* |
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 11326* |
Equality theorem for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | cbvprod 11327* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
& ⊢ Ⅎ𝑘𝐴
& ⊢ Ⅎ𝑗𝐴
& ⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvprodv 11328* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | cbvprodi 11329* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ Ⅎ𝑘𝐵
& ⊢ Ⅎ𝑗𝐶
& ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | prodeq1i 11330* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶 |
|
Theorem | prodeq2i 11331* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 |
|
Theorem | prodeq12i 11332* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷) ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷 |
|
Theorem | prodeq1d 11333* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
|
Theorem | prodeq2d 11334* |
Equality deduction for product. Note that unlike prodeq2dv 11335, 𝑘
may occur in 𝜑. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | prodeq2dv 11335* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | prodeq2sdv 11336* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) |
|
Theorem | 2cprodeq2dv 11337* |
Equality deduction for double product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodeq12dv 11338* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodeq12rdv 11339* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) |
|
Theorem | prodrbdclem 11340* |
Lemma for prodrbdc 11343. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 4-Apr-2024.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
⇒ ⊢ ((𝜑 ∧ 𝐴 ⊆
(ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾
(ℤ≥‘𝑁)) = seq𝑁( · , 𝐹)) |
|
Theorem | fproddccvg 11341* |
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 11342* |
Lemma for prodrbdc 11343. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID
𝑘 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) |
|
Theorem | prodrbdc 11343* |
Rebase the starting point of a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐴 ⊆
(ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴)
& ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID
𝑘 ∈ 𝐴) ⇒ ⊢ (𝜑 → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶)) |
|
Theorem | prodmodclem3 11344* |
Lemma for prodmodc 11347. (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 11345* |
Lemma for prodmodc 11347. (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 11346* |
Lemma for prodmodc 11347. (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 11347* |
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( · , 𝐺)‘𝑚)))) |
|
4.9 Elementary trigonometry
|
|
4.9.1 The exponential, sine, and cosine
functions
|
|
Syntax | ce 11348 |
Extend class notation to include the exponential function.
|
class exp |
|
Syntax | ceu 11349 |
Extend class notation to include Euler's constant e =
2.71828....
|
class e |
|
Syntax | csin 11350 |
Extend class notation to include the sine function.
|
class sin |
|
Syntax | ccos 11351 |
Extend class notation to include the cosine function.
|
class cos |
|
Syntax | ctan 11352 |
Extend class notation to include the tangent function.
|
class tan |
|
Syntax | cpi 11353 |
Extend class notation to include the constant pi, π
= 3.14159....
|
class π |
|
Definition | df-ef 11354* |
Define the exponential function. Its value at the complex number 𝐴
is (exp‘𝐴) and is called the "exponential
of 𝐴"; see
efval 11367. (Contributed by NM, 14-Mar-2005.)
|
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0
((𝑥↑𝑘) / (!‘𝑘))) |
|
Definition | df-e 11355 |
Define Euler's constant e = 2.71828.... (Contributed
by NM,
14-Mar-2005.)
|
⊢ e = (exp‘1) |
|
Definition | df-sin 11356 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i
· 𝑥)) −
(exp‘(-i · 𝑥))) / (2 · i))) |
|
Definition | df-cos 11357 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i
· 𝑥)) +
(exp‘(-i · 𝑥))) / 2)) |
|
Definition | df-tan 11358 |
Define the tangent function. We define it this way for cmpt 3989,
which
requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario
Carneiro, 14-Mar-2014.)
|
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦
((sin‘𝑥) /
(cos‘𝑥))) |
|
Definition | df-pi 11359 |
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 11360 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ) |
|
Theorem | reeftcl 11361 |
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 11362 |
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 11363* |
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) → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁))) |
|
Theorem | efcllemp 11364* |
Lemma for efcl 11370. The series that defines the exponential
function
converges. The ratio test cvgratgt0 11302 is used to show convergence.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → (2 ·
(abs‘𝐴)) < 𝐾)
⇒ ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ ) |
|
Theorem | efcllem 11365* |
Lemma for efcl 11370. The series that defines the exponential
function
converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝
) |
|
Theorem | ef0lem 11366* |
The series defining the exponential function converges in the (trivial)
case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 = 0 → seq0( + , 𝐹) ⇝ 1) |
|
Theorem | efval 11367* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘))) |
|
Theorem | esum 11368 |
Value of Euler's constant e = 2.71828.... (Contributed
by Steve
Rodriguez, 5-Mar-2006.)
|
⊢ e = Σ𝑘 ∈ ℕ0 (1 /
(!‘𝑘)) |
|
Theorem | eff 11369 |
Domain and codomain of the exponential function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
⊢ exp:ℂ⟶ℂ |
|
Theorem | efcl 11370 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈
ℂ) |
|
Theorem | efval2 11371* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘)) |
|
Theorem | efcvg 11372* |
The series that defines the exponential function converges to it.
(Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro,
28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ⇝ (exp‘𝐴)) |
|
Theorem | efcvgfsum 11373* |
Exponential function convergence in terms of a sequence of partial
finite sums. (Contributed by NM, 10-Jan-2006.) (Revised by Mario
Carneiro, 28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦
Σ𝑘 ∈ (0...𝑛)((𝐴↑𝑘) / (!‘𝑘))) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ (exp‘𝐴)) |
|
Theorem | reefcl 11374 |
The exponential function is real if its argument is real. (Contributed
by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈
ℝ) |
|
Theorem | reefcld 11375 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ) |
|
Theorem | ere 11376 |
Euler's constant e = 2.71828... is a real number.
(Contributed by
NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|
⊢ e ∈ ℝ |
|
Theorem | ege2le3 11377 |
Euler's constant e = 2.71828... is bounded by 2 and 3.
(Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 /
2)↑𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 /
(!‘𝑛))) ⇒ ⊢ (2 ≤ e ∧ e ≤
3) |
|
Theorem | ef0 11378 |
Value of the exponential function at 0. Equation 2 of [Gleason] p. 308.
(Contributed by Steve Rodriguez, 27-Jun-2006.) (Revised by Mario
Carneiro, 28-Apr-2014.)
|
⊢ (exp‘0) = 1 |
|
Theorem | efcj 11379 |
The exponential of a complex conjugate. Equation 3 of [Gleason] p. 308.
(Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro,
28-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ →
(exp‘(∗‘𝐴)) = (∗‘(exp‘𝐴))) |
|
Theorem | efaddlem 11380* |
Lemma for efadd 11381 (exponential function addition law).
(Contributed by
Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛))) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) |
|
Theorem | efadd 11381 |
Sum of exponents law for exponential function. (Contributed by NM,
10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) |
|
Theorem | efcan 11382 |
Cancellation law for exponential function. Equation 27 of [Rudin] p. 164.
(Contributed by NM, 13-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1) |
|
Theorem | efap0 11383 |
The exponential of a complex number is apart from zero. (Contributed by
Jim Kingdon, 12-Dec-2022.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) # 0) |
|
Theorem | efne0 11384 |
The exponential of a complex number is nonzero. Corollary 15-4.3 of
[Gleason] p. 309. The same result also
holds with not equal replaced by
apart, as seen at efap0 11383 (which will be more useful in most
contexts).
(Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ≠ 0) |
|
Theorem | efneg 11385 |
The exponential of the opposite is the inverse of the exponential.
(Contributed by Mario Carneiro, 10-May-2014.)
|
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴))) |
|
Theorem | eff2 11386 |
The exponential function maps the complex numbers to the nonzero complex
numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|
⊢ exp:ℂ⟶(ℂ ∖
{0}) |
|
Theorem | efsub 11387 |
Difference of exponents law for exponential function. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) |
|
Theorem | efexp 11388 |
The exponential of an integer power. Corollary 15-4.4 of [Gleason]
p. 309, restricted to integers. (Contributed by NM, 13-Jan-2006.)
(Revised by Mario Carneiro, 5-Jun-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (exp‘(𝑁 · 𝐴)) = ((exp‘𝐴)↑𝑁)) |
|
Theorem | efzval 11389 |
Value of the exponential function for integers. Special case of efval 11367.
Equation 30 of [Rudin] p. 164. (Contributed
by Steve Rodriguez,
15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁)) |
|
Theorem | efgt0 11390 |
The exponential of a real number is greater than 0. (Contributed by Paul
Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ (𝐴 ∈ ℝ → 0 <
(exp‘𝐴)) |
|
Theorem | rpefcl 11391 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈
ℝ+) |
|
Theorem | rpefcld 11392 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (exp‘𝐴) ∈
ℝ+) |
|
Theorem | eftlcvg 11393* |
The tail series of the exponential function are convergent.
(Contributed by Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) →
seq𝑀( + , 𝐹) ∈ dom ⇝
) |
|
Theorem | eftlcl 11394* |
Closure of the sum of an infinite tail of the series defining the
exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) →
Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
|
Theorem | reeftlcl 11395* |
Closure of the sum of an infinite tail of the series defining the
exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) →
Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℝ) |
|
Theorem | eftlub 11396* |
An upper bound on the absolute value of the infinite tail of the series
expansion of the exponential function on the closed unit disk.
(Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario
Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦
(((abs‘𝐴)↑𝑛) / (!‘𝑛))) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) ≤
1) ⇒ ⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |
|
Theorem | efsep 11397* |
Separate out the next term of the power series expansion of the
exponential function. The last hypothesis allows the separated terms to
be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007.)
(Revised by Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ 𝑀 ∈
ℕ0
& ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (exp‘𝐴) = (𝐵 + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘))) & ⊢ (𝜑 → (𝐵 + ((𝐴↑𝑀) / (!‘𝑀))) = 𝐷) ⇒ ⊢ (𝜑 → (exp‘𝐴) = (𝐷 + Σ𝑘 ∈ (ℤ≥‘𝑁)(𝐹‘𝑘))) |
|
Theorem | effsumlt 11398* |
The partial sums of the series expansion of the exponential function at
a positive real number are bounded by the value of the function.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈
ℕ0) ⇒ ⊢ (𝜑 → (seq0( + , 𝐹)‘𝑁) < (exp‘𝐴)) |
|
Theorem | eft0val 11399 |
The value of the first term of the series expansion of the exponential
function is 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by
Mario Carneiro, 29-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴↑0) / (!‘0)) =
1) |
|
Theorem | ef4p 11400* |
Separate out the first four terms of the infinite series expansion of
the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.)
(Revised by Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = ((((1 + 𝐴) + ((𝐴↑2) / 2)) + ((𝐴↑3) / 6)) + Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘))) |