Home | Intuitionistic Logic Explorer Theorem List (p. 105 of 142) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cseq 10401 | Extend class notation with recursive sequence builder. |
class seq𝑀( + , 𝐹) | ||
Definition | df-seqfrec 10402* |
Define a general-purpose operation that builds a recursive sequence
(i.e., a function on an upper integer set such as ℕ or ℕ0)
whose value at an index is a function of its previous value and the
value of an input sequence at that index. This definition is
complicated, but fortunately it is not intended to be used directly.
Instead, the only purpose of this definition is to provide us with an
object that has the properties expressed by seqf 10417, seq3-1 10416 and
seq3p1 10418. Typically, those are the main theorems
that would be used in
practice.
The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation +, an input sequence 𝐹 with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence seq1( + , 𝐹) with values 1, 3/2, 7/4, 15/8,.., so that (seq1( + , 𝐹)‘1) = 1, (seq1( + , 𝐹)‘2) = 3/2, etc. In other words, seq𝑀( + , 𝐹) transforms a sequence 𝐹 into an infinite series. seq𝑀( + , 𝐹) ⇝ 2 means "the sum of F(n) from n = M to infinity is 2". Since limits are unique (climuni 11256), by climdm 11258 the "sum of F(n) from n = 1 to infinity" can be expressed as ( ⇝ ‘seq1( + , 𝐹)) (provided the sequence converges) and evaluates to 2 in this example. Internally, the frec function generates as its values a set of ordered pairs starting at 〈𝑀, (𝐹‘𝑀)〉, with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by NM, 18-Apr-2005.) (Revised by Jim Kingdon, 4-Nov-2022.) |
⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) | ||
Theorem | seqex 10403 | Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ seq𝑀( + , 𝐹) ∈ V | ||
Theorem | seqeq1 10404 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹) = seq𝑁( + , 𝐹)) | ||
Theorem | seqeq2 10405 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ ( + = 𝑄 → seq𝑀( + , 𝐹) = seq𝑀(𝑄, 𝐹)) | ||
Theorem | seqeq3 10406 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺)) | ||
Theorem | seqeq1d 10407 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹)) | ||
Theorem | seqeq2d 10408 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → seq𝑀(𝐴, 𝐹) = seq𝑀(𝐵, 𝐹)) | ||
Theorem | seqeq3d 10409 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) | ||
Theorem | seqeq123d 10410 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝑀 = 𝑁) & ⊢ (𝜑 → + = 𝑄) & ⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑁(𝑄, 𝐺)) | ||
Theorem | nfseq 10411 | Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝑀 & ⊢ Ⅎ𝑥 + & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥seq𝑀( + , 𝐹) | ||
Theorem | iseqovex 10412* | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝑆) | ||
Theorem | iseqvalcbv 10413* | Changing the bound variables in an expression which appears in some seq related proofs. (Contributed by Jim Kingdon, 28-Apr-2022.) |
⊢ frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑇 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑎 ∈ (ℤ≥‘𝑀), 𝑏 ∈ 𝑇 ↦ 〈(𝑎 + 1), (𝑎(𝑐 ∈ (ℤ≥‘𝑀), 𝑑 ∈ 𝑆 ↦ (𝑑 + (𝐹‘(𝑐 + 1))))𝑏)〉), 〈𝑀, (𝐹‘𝑀)〉) | ||
Theorem | seq3val 10414* | Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 10417, seq3-1 10416 and seq3p1 10418, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅) | ||
Theorem | seqvalcd 10415* | Value of the sequence builder function. Similar to seq3val 10414 but the classes 𝐷 (type of each term) and 𝐶 (type of the value we are accumulating) do not need to be the same. (Contributed by Jim Kingdon, 9-Jul-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) & ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅) | ||
Theorem | seq3-1 10416* | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | ||
Theorem | seqf 10417* | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝑆) | ||
Theorem | seq3p1 10418* | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 30-Apr-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1)))) | ||
Theorem | seqovcd 10419* | A closure law for the recursive sequence builder. This is a lemma for theorems such as seqf2 10420 and seq1cd 10421 and is unlikely to be needed once such theorems are proved. (Contributed by Jim Kingdon, 20-Jul-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶) | ||
Theorem | seqf2 10420* | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 7-Jul-2023.) |
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝐶) | ||
Theorem | seq1cd 10421* | Initial value of the recursive sequence builder. A version of seq3-1 10416 which provides two classes 𝐷 and 𝐶 for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 19-Jul-2023.) |
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | ||
Theorem | seqp1cd 10422* | Value of the sequence builder function at a successor. A version of seq3p1 10418 which provides two classes 𝐷 and 𝐶 for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 20-Jul-2023.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1)))) | ||
Theorem | seq3clss 10423* | Closure property of the recursive sequence builder. (Contributed by Jim Kingdon, 28-Sep-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝑇) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥 + 𝑦) ∈ 𝑇) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆) | ||
Theorem | seq3m1 10424* | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 3-Nov-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (𝐹‘𝑁))) | ||
Theorem | seq3fveq2 10425* | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)) | ||
Theorem | seq3feq2 10426* | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺)) | ||
Theorem | seq3fveq 10427* | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | seq3feq 10428* | Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐺‘𝑘)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺)) | ||
Theorem | seq3shft2 10429* | Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾))) | ||
Theorem | serf 10430* | An infinite series of complex terms is a function from ℕ to ℂ. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ) | ||
Theorem | serfre 10431* | An infinite series of real numbers is a function from ℕ to ℝ. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) | ||
Theorem | monoord 10432* | Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁)) | ||
Theorem | monoord2 10433* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) | ||
Theorem | ser3mono 10434* | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ≤ (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | seq3split 10435* | Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))) | ||
Theorem | seq3-1p 10436* | Removing the first term from a sequence. (Contributed by Jim Kingdon, 16-Aug-2021.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = ((𝐹‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))) | ||
Theorem | seq3caopr3 10437* | Lemma for seq3caopr2 10438. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by Jim Kingdon, 22-Apr-2023.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seq3caopr2 10438* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆))) → ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seq3caopr 10439* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 23-Apr-2023.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | iseqf1olemkle 10440* | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 21-Aug-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) ⇒ ⊢ (𝜑 → 𝐾 ≤ (◡𝐽‘𝐾)) | ||
Theorem | iseqf1olemklt 10441* | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 21-Aug-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) & ⊢ (𝜑 → 𝐾 ≠ (◡𝐽‘𝐾)) ⇒ ⊢ (𝜑 → 𝐾 < (◡𝐽‘𝐾)) | ||
Theorem | iseqf1olemqcl 10442 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → if(𝐴 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))), (𝐽‘𝐴)) ∈ (𝑀...𝑁)) | ||
Theorem | iseqf1olemqval 10443* | Lemma for seq3f1o 10460. Value of the function 𝑄. (Contributed by Jim Kingdon, 28-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝑀...𝑁)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) ⇒ ⊢ (𝜑 → (𝑄‘𝐴) = if(𝐴 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))), (𝐽‘𝐴))) | ||
Theorem | iseqf1olemnab 10444* | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → (𝑄‘𝐴) = (𝑄‘𝐵)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) ⇒ ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐾...(◡𝐽‘𝐾)) ∧ ¬ 𝐵 ∈ (𝐾...(◡𝐽‘𝐾)))) | ||
Theorem | iseqf1olemab 10445* | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → (𝑄‘𝐴) = (𝑄‘𝐵)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ (𝜑 → 𝐴 ∈ (𝐾...(◡𝐽‘𝐾))) & ⊢ (𝜑 → 𝐵 ∈ (𝐾...(◡𝐽‘𝐾))) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | iseqf1olemnanb 10446* | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → (𝑄‘𝐴) = (𝑄‘𝐵)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ (𝜑 → ¬ 𝐴 ∈ (𝐾...(◡𝐽‘𝐾))) & ⊢ (𝜑 → ¬ 𝐵 ∈ (𝐾...(◡𝐽‘𝐾))) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | iseqf1olemqf 10447* | Lemma for seq3f1o 10460. Domain and codomain of 𝑄. (Contributed by Jim Kingdon, 26-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) ⇒ ⊢ (𝜑 → 𝑄:(𝑀...𝑁)⟶(𝑀...𝑁)) | ||
Theorem | iseqf1olemmo 10448* | Lemma for seq3f1o 10460. Showing that 𝑄 is one-to-one. (Contributed by Jim Kingdon, 27-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ (𝜑 → 𝐴 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → (𝑄‘𝐴) = (𝑄‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | iseqf1olemqf1o 10449* | Lemma for seq3f1o 10460. 𝑄 is a permutation of (𝑀...𝑁). 𝑄 is formed from the constant portion of 𝐽, followed by the single element 𝐾 (at position 𝐾), followed by the rest of J (with the 𝐾 deleted and the elements before 𝐾 moved one position later to fill the gap). (Contributed by Jim Kingdon, 21-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) ⇒ ⊢ (𝜑 → 𝑄:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) | ||
Theorem | iseqf1olemqk 10450* | Lemma for seq3f1o 10460. 𝑄 is constant for one more position than 𝐽 is. (Contributed by Jim Kingdon, 21-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝐾)(𝑄‘𝑥) = 𝑥) | ||
Theorem | iseqf1olemjpcl 10451* | Lemma for seq3f1o 10460. A closure lemma involving 𝐽 and 𝑃. (Contributed by Jim Kingdon, 29-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) | ||
Theorem | iseqf1olemqpcl 10452* | Lemma for seq3f1o 10460. A closure lemma involving 𝑄 and 𝑃. (Contributed by Jim Kingdon, 29-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) | ||
Theorem | iseqf1olemfvp 10453* | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 30-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝑇:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ (𝜑 → (⦋𝑇 / 𝑓⦌𝑃‘𝐴) = (𝐺‘(𝑇‘𝐴))) | ||
Theorem | seq3f1olemqsumkj 10454* | Lemma for seq3f1o 10460. 𝑄 gives the same sum as 𝐽 in the range (𝐾...(◡𝐽‘𝐾)). (Contributed by Jim Kingdon, 29-Aug-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) & ⊢ (𝜑 → 𝐾 ≠ (◡𝐽‘𝐾)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾))) | ||
Theorem | seq3f1olemqsumk 10455* | Lemma for seq3f1o 10460. 𝑄 gives the same sum as 𝐽 in the range (𝐾...𝑁). (Contributed by Jim Kingdon, 22-Aug-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) & ⊢ (𝜑 → 𝐾 ≠ (◡𝐽‘𝐾)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)) | ||
Theorem | seq3f1olemqsum 10456* | Lemma for seq3f1o 10460. 𝑄 gives the same sum as 𝐽. (Contributed by Jim Kingdon, 21-Aug-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) & ⊢ (𝜑 → 𝐾 ≠ (◡𝐽‘𝐾)) & ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ (𝜑 → (seq𝑀( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝑀( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)) | ||
Theorem | seq3f1olemstep 10457* | Lemma for seq3f1o 10460. Given a permutation which is constant up to a point, supply a new one which is constant for one more position. (Contributed by Jim Kingdon, 19-Aug-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) & ⊢ (𝜑 → (seq𝑀( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝑀( + , 𝐿)‘𝑁)) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ ∀𝑥 ∈ (𝑀...𝐾)(𝑓‘𝑥) = 𝑥 ∧ (seq𝑀( + , 𝑃)‘𝑁) = (seq𝑀( + , 𝐿)‘𝑁))) | ||
Theorem | seq3f1olemp 10458* | Lemma for seq3f1o 10460. Existence of a constant permutation of (𝑀...𝑁) which leads to the same sum as the permutation 𝐹 itself. (Contributed by Jim Kingdon, 18-Aug-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ 𝐿 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀))) & ⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ ∀𝑥 ∈ (𝑀...𝑁)(𝑓‘𝑥) = 𝑥 ∧ (seq𝑀( + , 𝑃)‘𝑁) = (seq𝑀( + , 𝐿)‘𝑁))) | ||
Theorem | seq3f1oleml 10459* | Lemma for seq3f1o 10460. This is more or less the result, but stated in terms of 𝐹 and 𝐺 without 𝐻. 𝐿 and 𝐻 may differ in terms of what happens to terms after 𝑁. The terms after 𝑁 don't matter for the value at 𝑁 but we need some definition given the way our theorems concerning seq work. (Contributed by Jim Kingdon, 17-Aug-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ 𝐿 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝐹‘𝑥)), (𝐺‘𝑀))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐿)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | seq3f1o 10460* | Rearrange a sum via an arbitrary bijection on (𝑀...𝑁). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 3-Nov-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = (𝐺‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | ser3add 10461* | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 4-Oct-2022.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | ser3sub 10462* | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) − (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seq3id3 10463* | A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a + -idempotent sums (or "+'s") to that element. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Jim Kingdon, 8-Apr-2023.) |
⊢ (𝜑 → (𝑍 + 𝑍) = 𝑍) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = 𝑍) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) | ||
Theorem | seq3id 10464* | Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for +) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 8-Apr-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑥) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑥) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( + , 𝐹)) | ||
Theorem | seq3id2 10465* | The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for +) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 12-Nov-2022.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑥) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑥) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | seq3homo 10466* | Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 10-Oct-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)) | ||
Theorem | seq3z 10467* | If the operation + has an absorbing element 𝑍 (a.k.a. zero element), then any sequence containing a 𝑍 evaluates to 𝑍. (Contributed by Mario Carneiro, 27-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑍) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → (𝐹‘𝐾) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) | ||
Theorem | seqfeq3 10468* | Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑥𝑄𝑦)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀(𝑄, 𝐹)) | ||
Theorem | seq3distr 10469* | The distributive property for series. (Contributed by Jim Kingdon, 10-Oct-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑇𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | ser0 10470 | The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013.) (Revised by Mario Carneiro, 15-Dec-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( + , (𝑍 × {0}))‘𝑁) = 0) | ||
Theorem | ser0f 10471 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0})) = (𝑍 × {0})) | ||
Theorem | fser0const 10472* | Simplifying an expression which turns out just to be a constant zero sequence. (Contributed by Jim Kingdon, 16-Sep-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑛 ∈ 𝑍 ↦ if(𝑛 ≤ 𝑁, ((𝑍 × {0})‘𝑛), 0)) = (𝑍 × {0})) | ||
Theorem | ser3ge0 10473* | A finite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 8-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 0 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 0 ≤ (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | ser3le 10474* | Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Jim Kingdon, 23-Apr-2023.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ≤ (seq𝑀( + , 𝐺)‘𝑁)) | ||
Syntax | cexp 10475 | Extend class notation to include exponentiation of a complex number to an integer power. |
class ↑ | ||
Definition | df-exp 10476* |
Define exponentiation to nonnegative integer powers. For example,
(5↑2) = 25 (see ex-exp 13762).
This definition is not meant to be used directly; instead, exp0 10480 and expp1 10483 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0↑0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134 (see 0exp0e1 10481). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3↑-2) = (1 / 9) (ex-exp 13762). The case 𝑥 = 0, 𝑦 < 0 gives the value (1 / 0), so we will avoid this case in our theorems. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.) |
⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦))))) | ||
Theorem | exp3vallem 10477 | Lemma for exp3val 10478. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingdon, 7-Jun-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (seq1( · , (ℕ × {𝐴}))‘𝑁) # 0) | ||
Theorem | exp3val 10478 | Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}))‘-𝑁))))) | ||
Theorem | expnnval 10479 | Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ × {𝐴}))‘𝑁)) | ||
Theorem | exp0 10480 | Value of a complex number raised to the 0th power. Note that under our definition, 0↑0 = 1 (0exp0e1 10481) , following the convention used by Gleason. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) | ||
Theorem | 0exp0e1 10481 | The zeroth power of zero equals one. See comment of exp0 10480. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (0↑0) = 1 | ||
Theorem | exp1 10482 | Value of a complex number raised to the first power. (Contributed by NM, 20-Oct-2004.) (Revised by Mario Carneiro, 2-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) | ||
Theorem | expp1 10483 | Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2005.) (Revised by Mario Carneiro, 2-Jul-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
Theorem | expnegap0 10484 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | expineg2 10485 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) | ||
Theorem | expn1ap0 10486 | A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴↑-1) = (1 / 𝐴)) | ||
Theorem | expcllem 10487* | Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.) |
⊢ 𝐹 ⊆ ℂ & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹) | ||
Theorem | expcl2lemap 10488* | Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.) |
⊢ 𝐹 ⊆ ℂ & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 # 0) → (1 / 𝑥) ∈ 𝐹) ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ 𝐹) | ||
Theorem | nnexpcl 10489 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ) | ||
Theorem | nn0expcl 10490 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ0) | ||
Theorem | zexpcl 10491 | Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ) | ||
Theorem | qexpcl 10492 | Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | reexpcl 10493 | Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | expcl 10494 | Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) | ||
Theorem | rpexpcl 10495 | Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) | ||
Theorem | reexpclzap 10496 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | qexpclz 10497 | Closure of exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | m1expcl2 10498 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1, 1}) | ||
Theorem | m1expcl 10499 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℤ) | ||
Theorem | expclzaplem 10500* | Closure law for integer exponentiation. Lemma for expclzap 10501 and expap0i 10508. (Contributed by Jim Kingdon, 9-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ {𝑧 ∈ ℂ ∣ 𝑧 # 0}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |