![]() |
Metamath
Proof Explorer Theorem List (p. 132 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43650) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | axdc4uzlem 13101* | Lemma for axdc4uz 13102. (Contributed by Mario Carneiro, 8-Jan-2014.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 ∈ V & ⊢ 𝐺 = (rec((𝑦 ∈ V ↦ (𝑦 + 1)), 𝑀) ↾ ω) & ⊢ 𝐻 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ((𝐺‘𝑛)𝐹𝑥)) ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(𝑍 × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:𝑍⟶𝐴 ∧ (𝑔‘𝑀) = 𝐶 ∧ ∀𝑘 ∈ 𝑍 (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))) | ||
Theorem | axdc4uz 13102* | A version of axdc4 9613 that works on an upper set of integers instead of ω. (Contributed by Mario Carneiro, 8-Jan-2014.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴 ∧ 𝐹:(𝑍 × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:𝑍⟶𝐴 ∧ (𝑔‘𝑀) = 𝐶 ∧ ∀𝑘 ∈ 𝑍 (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))) | ||
Theorem | ssnn0fi 13103* | A subset of the nonnegative integers is finite if and only if there is a nonnegative integer so that all integers greater than this integer are not contained in the subset. (Contributed by AV, 3-Oct-2019.) |
⊢ (𝑆 ⊆ ℕ0 → (𝑆 ∈ Fin ↔ ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝑥 ∉ 𝑆))) | ||
Theorem | rabssnn0fi 13104* | A subset of the nonnegative integers defined by a restricted class abstraction is finite if there is a nonnegative integer so that for all integers greater than this integer the condition of the class abstraction is not fulfilled. (Contributed by AV, 3-Oct-2019.) |
⊢ ({𝑥 ∈ ℕ0 ∣ 𝜑} ∈ Fin ↔ ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ¬ 𝜑)) | ||
Theorem | uzsinds 13105* | Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (∀𝑦 ∈ (𝑀...(𝑥 − 1))𝜓 → 𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜒) | ||
Theorem | nnsinds 13106* | Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ (1...(𝑥 − 1))𝜓 → 𝜑)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝜒) | ||
Theorem | nn0sinds 13107* | Strong (or "total") induction principle over the nonnegative integers. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ℕ0 → (∀𝑦 ∈ (0...(𝑥 − 1))𝜓 → 𝜑)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝜒) | ||
Theorem | fsuppmapnn0fiublem 13108* | Lemma for fsuppmapnn0fiub 13109 and fsuppmapnn0fiubex 13110. (Contributed by AV, 2-Oct-2019.) |
⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) & ⊢ 𝑆 = sup(𝑈, ℝ, < ) ⇒ ⊢ ((𝑀 ⊆ (𝑅 ↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → 𝑆 ∈ ℕ0)) | ||
Theorem | fsuppmapnn0fiub 13109* | If all functions of a finite set of functions over the nonnegative integers are finitely supported, then the support of all these functions is contained in a finite set of sequential integers starting at 0 and ending with the supremum of the union of the support of these functions. (Contributed by AV, 2-Oct-2019.) (Proof shortened by JJ, 2-Aug-2021.) |
⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍) & ⊢ 𝑆 = sup(𝑈, ℝ, < ) ⇒ ⊢ ((𝑀 ⊆ (𝑅 ↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑆))) | ||
Theorem | fsuppmapnn0fiubex 13110* | If all functions of a finite set of functions over the nonnegative integers are finitely supported, then the support of all these functions is contained in a finite set of sequential integers starting at 0. (Contributed by AV, 2-Oct-2019.) |
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚))) | ||
Theorem | fsuppmapnn0fiub0 13111* | If all functions of a finite set of functions over the nonnegative integers are finitely supported, then all these functions are zero for all integers greater than a fixed integer. (Contributed by AV, 3-Oct-2019.) |
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | ||
Theorem | suppssfz 13112* | Condition for a function over the nonnegative integers to have a support contained in a finite set of sequential integers. (Contributed by AV, 9-Oct-2019.) |
⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑𝑚 ℕ0)) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍)) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (0...𝑆)) | ||
Theorem | fsuppmapnn0ub 13113* | If a function over the nonnegative integers is finitely supported, then there is an upper bound for the arguments resulting in nonzero values. (Contributed by AV, 6-Oct-2019.) |
⊢ ((𝐹 ∈ (𝑅 ↑𝑚 ℕ0) ∧ 𝑍 ∈ 𝑉) → (𝐹 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝐹‘𝑥) = 𝑍))) | ||
Theorem | fsuppmapnn0fz 13114* | If a function over the nonnegative integers is finitely supported, then there is an upper bound for a finite set of sequential integers containing the support of the function. (Contributed by AV, 30-Sep-2019.) (Proof shortened by AV, 6-Oct-2019.) |
⊢ ((𝐹 ∈ (𝑅 ↑𝑚 ℕ0) ∧ 𝑍 ∈ 𝑉) → (𝐹 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 (𝐹 supp 𝑍) ⊆ (0...𝑚))) | ||
Theorem | mptnn0fsupp 13115* | A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 23-Dec-2019.) |
⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐶 = 0 )) ⇒ ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐶) finSupp 0 ) | ||
Theorem | mptnn0fsuppd 13116* | A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 2-Dec-2019.) (Revised by AV, 23-Dec-2019.) |
⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ 𝐵) & ⊢ (𝑘 = 𝑥 → 𝐶 = 𝐷) & ⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → 𝐷 = 0 )) ⇒ ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐶) finSupp 0 ) | ||
Theorem | mptnn0fsuppr 13117* | A finitely supported mapping from the nonnegative integers fulfills certain conditions. (Contributed by AV, 3-Nov-2019.) (Revised by AV, 23-Dec-2019.) |
⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐶) finSupp 0 ) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐶 = 0 )) | ||
Theorem | f13idfv 13118 | A one-to-one function with the domain { 0, 1 ,2 } in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ 𝐴 = (0...2) ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘0) ≠ (𝐹‘1) ∧ (𝐹‘0) ≠ (𝐹‘2) ∧ (𝐹‘1) ≠ (𝐹‘2)))) | ||
Syntax | cseq 13119 | Extend class notation with recursive sequence builder. |
class seq𝑀( + , 𝐹) | ||
Definition | df-seq 13120* |
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 seq1 13132
and seqp1 13134.
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 14691), by climdm 14693 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 rec 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 rec is exactly the sequence we want, and we just extract the range (restricted to omega) and throw away the domain. This definition has its roots in a series of theorems from om2uz0i 13065 through om2uzf1oi 13071, originally proved by Raph Levien for use with df-exp 13179 and later generalized for arbitrary recursive sequences. Definition df-sum 14825 extracts the summation values from partial (finite) and complete (infinite) series. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 4-Sep-2013.) |
⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) | ||
Theorem | seqex 13121 | Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ seq𝑀( + , 𝐹) ∈ V | ||
Theorem | seqeq1 13122 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹) = seq𝑁( + , 𝐹)) | ||
Theorem | seqeq2 13123 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ ( + = 𝑄 → seq𝑀( + , 𝐹) = seq𝑀(𝑄, 𝐹)) | ||
Theorem | seqeq3 13124 | Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺)) | ||
Theorem | seqeq1d 13125 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹)) | ||
Theorem | seqeq2d 13126 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → seq𝑀(𝐴, 𝐹) = seq𝑀(𝐵, 𝐹)) | ||
Theorem | seqeq3d 13127 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵)) | ||
Theorem | seqeq123d 13128 | Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.) |
⊢ (𝜑 → 𝑀 = 𝑁) & ⊢ (𝜑 → + = 𝑄) & ⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑁(𝑄, 𝐺)) | ||
Theorem | nfseq 13129 | Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝑀 & ⊢ Ⅎ𝑥 + & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥seq𝑀( + , 𝐹) | ||
Theorem | seqval 13130* | Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω) ⇒ ⊢ seq𝑀( + , 𝐹) = ran 𝑅 | ||
Theorem | seqfn 13131 | The sequence builder function is a function. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝑀 ∈ ℤ → seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀)) | ||
Theorem | seq1 13132 | Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | ||
Theorem | seq1i 13133 | Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝑀 ∈ ℤ & ⊢ (𝜑 → (𝐹‘𝑀) = 𝐴) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝐴) | ||
Theorem | seqp1 13134 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1)))) | ||
Theorem | seqp1i 13135 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 ∈ 𝑍 & ⊢ 𝐾 = (𝑁 + 1) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝐴) & ⊢ (𝜑 → (𝐹‘𝐾) = 𝐵) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐴 + 𝐵)) | ||
Theorem | seqm1 13136 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑁) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (𝐹‘𝑁))) | ||
Theorem | seqcl2 13137* | Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑀 + 1)...𝑁)) → (𝐹‘𝑥) ∈ 𝐷) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝐶) | ||
Theorem | seqf2 13138* | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝐶) | ||
Theorem | seqcl 13139* | Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆) | ||
Theorem | seqf 13140* | Range of the recursive sequence builder (special case of seqf2 13138). (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝑆) | ||
Theorem | seqfveq2 13141* | Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁)) | ||
Theorem | seqfeq2 13142* | Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺)) | ||
Theorem | seqfveq 13143* | Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | seqfeq 13144* | Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺)) | ||
Theorem | seqshft2 13145* | Shifting the index set of a sequence. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺)‘(𝑁 + 𝐾))) | ||
Theorem | seqres 13146 | Restricting its characteristic function to (ℤ≥‘𝑀) does not affect the seq function. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝐹 ↾ (ℤ≥‘𝑀))) = seq𝑀( + , 𝐹)) | ||
Theorem | serf 13147* | 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 13148* | 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 13149* | 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 13150* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) | ||
Theorem | sermono 13151* | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 30-Jun-2013.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ≤ (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | seqsplit 13152* | Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))) | ||
Theorem | seq1p 13153* | Removing the first term from a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = ((𝐹‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))) | ||
Theorem | seqcaopr3 13154* | Lemma for seqcaopr2 13155. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqcaopr2 13155* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆))) → ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqcaopr 13156* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 30-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqf1olem2a 13157* | Lemma for seqf1o 13160. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐴) ⇒ ⊢ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾))) | ||
Theorem | seqf1olem1 13158* | Lemma for seqf1o 13160. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) & ⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝐶) & ⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) & ⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) ⇒ ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) | ||
Theorem | seqf1olem2 13159* | Lemma for seqf1o 13160. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) & ⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝐶) & ⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) & ⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) & ⊢ (𝜑 → ∀𝑔∀𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁))) ⇒ ⊢ (𝜑 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1))) | ||
Theorem | seqf1o 13160* | Rearrange a sum via an arbitrary bijection on (𝑀...𝑁). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = (𝐺‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | seradd 13161* | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | sersub 13162* | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) − (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqid3 13163* | 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.) |
⊢ (𝜑 → (𝑍 + 𝑍) = 𝑍) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) | ||
Theorem | seqid 13164* | 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 Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑥) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( + , 𝐹)) | ||
Theorem | seqid2 13165* | 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 Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑥) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | seqhomo 13166* | Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)) | ||
Theorem | seqz 13167* | 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.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑍) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (𝐹‘𝐾) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) | ||
Theorem | seqfeq4 13168* | Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑥𝑄𝑦)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀(𝑄, 𝐹)‘𝑁)) | ||
Theorem | seqfeq3 13169* | 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 | seqdistr 13170* | The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | ser0 13171 | 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 13172 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0})) = (𝑍 × {0})) | ||
Theorem | serge0 13173* | 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 | serle 13174* | Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ≤ (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | ser1const 13175 | Value of the partial series sum of a constant function. (Contributed by NM, 8-Aug-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (seq1( + , (ℕ × {𝐴}))‘𝑁) = (𝑁 · 𝐴)) | ||
Theorem | seqof 13176* | Distribute function operation through a sequence. Note that 𝐺(𝑧) is an implicit function on 𝑧. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))) ⇒ ⊢ (𝜑 → (seq𝑀( ∘𝑓 + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqof2 13177* | Distribute function operation through a sequence. Maps-to notation version of seqof 13176. (Contributed by Mario Carneiro, 7-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊) ⇒ ⊢ (𝜑 → (seq𝑀( ∘𝑓 + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) | ||
Syntax | cexp 13178 | Extend class notation to include exponentiation of a complex number to an integer power. |
class ↑ | ||
Definition | df-exp 13179* |
Define exponentiation to nonnegative integer powers. For example,
(5↑2) = 25 (ex-exp 27882). Terminology: In general,
"exponentiation" is the operation of raising a
"base" 𝑥 to the power
of the "exponent" 𝑦, resulting in the "power"
(𝑥↑𝑦), also
called "x to the power of y". In this case, "integer
exponentiation" is
the operation of raising a complex "base" 𝑥 to the
power of an
integer 𝑦, resulting in the "integer
power" (𝑥↑𝑦).
This definition is not meant to be used directly; instead, exp0 13182 and expp1 13185 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 (0exp0e1 13183). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3↑-2) = (1 / 9) (ex-exp 27882). The case 𝑥 = 0, 𝑦 < 0 gives the value (1 / 0), so we will avoid this case in our theorems. For a definition of exponentiation including complex exponents see df-cxp 24741 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 24850. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.) |
⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦))))) | ||
Theorem | expval 13180 | Value of exponentiation to integer powers. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}))‘-𝑁))))) | ||
Theorem | expnnval 13181 | Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ × {𝐴}))‘𝑁)) | ||
Theorem | exp0 13182 | Value of a complex number raised to the 0th power. Note that under our definition, 0↑0 = 1, 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 13183 | 0↑0 = 1. This is our convention. It follows the convention used by Gleason; see Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (0↑0) = 1 | ||
Theorem | exp1 13184 | 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 13185 | 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 | expneg 13186 | Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | expneg2 13187 | Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) | ||
Theorem | expn1 13188 | A number to the negative one power is the reciprocal. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑-1) = (1 / 𝐴)) | ||
Theorem | expcllem 13189* | Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.) |
⊢ 𝐹 ⊆ ℂ & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹) | ||
Theorem | expcl2lem 13190* | Lemma for proving integer exponentiation closure laws. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝐹 ⊆ ℂ & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐹) ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ 𝐹) | ||
Theorem | nnexpcl 13191 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ) | ||
Theorem | nn0expcl 13192 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ0) | ||
Theorem | zexpcl 13193 | Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ) | ||
Theorem | qexpcl 13194 | Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | reexpcl 13195 | Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | expcl 13196 | Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) | ||
Theorem | rpexpcl 13197 | Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) | ||
Theorem | reexpclz 13198 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | qexpclz 13199 | Closure of exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | m1expcl2 13200 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1, 1}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |