P. 138 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnct 13701	ℕ is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ ℕ ≼ ω
Theorem	uzindi 13702*	Indirect strong induction on the upper integers. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐿))    &   ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐿...𝑇) ∧ ∀𝑦(𝑆 ∈ (𝐿..^𝑅) → 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)    &   ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	axdc4uzlem 13703*	Lemma for axdc4uz 13704. (Contributed by Mario Carneiro, 8-Jan-2014.) (Revised by Mario Carneiro, 26-Dec-2014.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐺 = (rec((𝑦 ∈ V ↦ (𝑦 + 1)), 𝑀) ↾ ω)    &   ⊢ 𝐻 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ((𝐺‘𝑛)𝐹𝑥))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(𝑍 × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:𝑍⟶𝐴 ∧ (𝑔‘𝑀) = 𝐶 ∧ ∀𝑘 ∈ 𝑍 (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))))
Theorem	axdc4uz 13704*	A version of axdc4 10212 that works on an upper set of integers instead of ω. (Contributed by Mario Carneiro, 8-Jan-2014.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴 ∧ 𝐹:(𝑍 × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:𝑍⟶𝐴 ∧ (𝑔‘𝑀) = 𝐶 ∧ ∀𝑘 ∈ 𝑍 (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))))
Theorem	ssnn0fi 13705*	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 13706*	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 (𝑠 < 𝑥 → ¬ 𝜑))
5.6.4  Strong induction over upper sets of integers
Theorem	uzsinds 13707*	Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (∀𝑦 ∈ (𝑀...(𝑥 − 1))𝜓 → 𝜑))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜒)
Theorem	nnsinds 13708*	Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ (1...(𝑥 − 1))𝜓 → 𝜑))    ⇒   ⊢ (𝑁 ∈ ℕ → 𝜒)
Theorem	nn0sinds 13709*	Strong (or "total") induction principle over the nonnegative integers. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ ℕ0 → (∀𝑦 ∈ (0...(𝑥 − 1))𝜓 → 𝜑))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝜒)
5.6.5  Finitely supported functions over the nonnegative integers
Theorem	fsuppmapnn0fiublem 13710*	Lemma for fsuppmapnn0fiub 13711 and fsuppmapnn0fiubex 13712. (Contributed by AV, 2-Oct-2019.)
⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍)    &   ⊢ 𝑆 = sup(𝑈, ℝ, < )    ⇒   ⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → 𝑆 ∈ ℕ0))
Theorem	fsuppmapnn0fiub 13711*	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(𝑈, ℝ, < )    ⇒   ⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑆)))
Theorem	fsuppmapnn0fiubex 13712*	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.)
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚)))
Theorem	fsuppmapnn0fiub0 13713*	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.)
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍)))
Theorem	suppssfz 13714*	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.)
⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0))    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍))    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (0...𝑆))
Theorem	fsuppmapnn0ub 13715*	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.)
⊢ ((𝐹 ∈ (𝑅 ↑m ℕ0) ∧ 𝑍 ∈ 𝑉) → (𝐹 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝐹‘𝑥) = 𝑍)))
Theorem	fsuppmapnn0fz 13716*	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.)
⊢ ((𝐹 ∈ (𝑅 ↑m ℕ0) ∧ 𝑍 ∈ 𝑉) → (𝐹 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 (𝐹 supp 𝑍) ⊆ (0...𝑚)))
Theorem	mptnn0fsupp 13717*	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 13718*	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 13719*	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 13720	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))))
5.6.6  The infinite sequence builder "seq" - extension
Syntax	cseq 13721	Extend class notation with recursive sequence builder.
class seq𝑀( + , 𝐹)
Definition	df-seq 13722*	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 13734 and seqp1 13736. 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 15261), by climdm 15263 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 13667 through om2uzf1oi 13673, originally proved by Raph Levien for use with df-exp 13783 and later generalized for arbitrary recursive sequences. Definition df-sum 15398 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 13723	Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ seq𝑀( + , 𝐹) ∈ V
Theorem	seqeq1 13724	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹) = seq𝑁( + , 𝐹))
Theorem	seqeq2 13725	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ ( + = 𝑄 → seq𝑀( + , 𝐹) = seq𝑀(𝑄, 𝐹))
Theorem	seqeq3 13726	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))
Theorem	seqeq1d 13727	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
Theorem	seqeq2d 13728	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝑀(𝐴, 𝐹) = seq𝑀(𝐵, 𝐹))
Theorem	seqeq3d 13729	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
Theorem	seqeq123d 13730	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑁(𝑄, 𝐺))
Theorem	nfseq 13731	Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seq𝑀( + , 𝐹)
Theorem	seqval 13732*	Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ↾ ω)    ⇒   ⊢ seq𝑀( + , 𝐹) = ran 𝑅
Theorem	seqfn 13733	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 13734	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 13735	Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014.)
⊢ 𝑀 ∈ ℤ    &   ⊢ (𝜑 → (𝐹‘𝑀) = 𝐴)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝐴)
Theorem	seqp1 13736	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	seqexw 13737	Weak version of seqex 13723 that holds without ax-rep 5209. A sequence builder exists when its binary operation input exists and its starting index is an integer. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ + ∈ V    &   ⊢ 𝑀 ∈ ℤ    ⇒   ⊢ seq𝑀( + , 𝐹) ∈ V
Theorem	seqp1d 13738	Value of the sequence builder function at a successor, deduction form. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by AV, 3-May-2024.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ 𝐾 = (𝑁 + 1)    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐾) = 𝐵)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐴 + 𝐵))
Theorem	seqp1iOLD 13739	Obsolete version of seqp1d 13738 as of 3-May-2024. Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑁 ∈ 𝑍    &   ⊢ 𝐾 = (𝑁 + 1)    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐾) = 𝐵)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐴 + 𝐵))
Theorem	seqm1 13740	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑁) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (𝐹‘𝑁)))
Theorem	seqcl2 13741*	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 13742*	Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝐶)
Theorem	seqcl 13743*	Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆)
Theorem	seqf 13744*	Range of the recursive sequence builder (special case of seqf2 13742). (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝑆)
Theorem	seqfveq2 13745*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))
Theorem	seqfeq2 13746*	Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺))
Theorem	seqfveq 13747*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
Theorem	seqfeq 13748*	Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))
Theorem	seqshft2 13749*	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 13750	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 13751*	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 13752*	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 13753*	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 13754*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))
Theorem	sermono 13755*	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 13756*	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 13757*	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 13758*	Lemma for seqcaopr2 13759. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqcaopr2 13759*	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 13760*	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 13761*	Lemma for seqf1o 13764. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾)))
Theorem	seqf1olem1 13762*	Lemma for seqf1o 13764. (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 13763*	Lemma for seqf1o 13764. (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 13764*	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 13765*	The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	sersub 13766*	The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) − (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqid3 13767*	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 13768*	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 13769*	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 13770*	Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))
Theorem	seqz 13771*	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 13772*	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 13773*	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 13774*	The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦)))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺)‘𝑁)))
Theorem	ser0 13775	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 13776	A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0})) = (𝑍 × {0}))
Theorem	serge0 13777*	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 13778*	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 13779	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 13780*	Distribute function operation through a sequence. Note that 𝐺(𝑧) is an implicit function on 𝑧. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqof2 13781*	Distribute function operation through a sequence. Maps-to notation version of seqof 13780. (Contributed by Mario Carneiro, 7-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)))
5.6.7  Integer powers
Syntax	cexp 13782	Extend class notation to include exponentiation of a complex number to an integer power.
class ↑
Definition	df-exp 13783*	Define exponentiation to nonnegative integer powers. For example, (5↑2) = 25 (ex-exp 28814). 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 13786 and expp1 13789 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 13787). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3↑-2) = (1 / 9) (ex-exp 28814). 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 25713 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 25822. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.)
⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦)))))
Theorem	expval 13784	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 13785	Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ × {𝐴}))‘𝑁))
Theorem	exp0 13786	Value of a complex number raised to the 0th power. Note that under our definition, 0↑0 = 1 (0exp0e1 13787) , 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 13787	The zeroth power of zero equals one. See comment of exp0 13786. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0↑0) = 1
Theorem	exp1 13788	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 13789	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 13790	Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁)))
Theorem	expneg2 13791	Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁)))
Theorem	expn1 13792	A number to the negative one power is the reciprocal. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴↑-1) = (1 / 𝐴))
Theorem	expcllem 13793*	Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.)
⊢ 𝐹 ⊆ ℂ    &   ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹)    &   ⊢ 1 ∈ 𝐹    ⇒   ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹)
Theorem	expcl2lem 13794*	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 13795	Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ)
Theorem	nn0expcl 13796	Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ0)
Theorem	zexpcl 13797	Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ)
Theorem	qexpcl 13798	Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ)
Theorem	reexpcl 13799	Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ)
Theorem	expcl 13800	Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ)