P. 141 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14001-14100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fzofi 14001	Half-open integer sets are finite. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝑀..^𝑁) ∈ Fin
Theorem	fsequb 14002*	The values of a finite real sequence have an upper bound. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) < 𝑥)
Theorem	fsequb2 14003*	The values of a finite real sequence have an upper bound. (Contributed by NM, 20-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹:(𝑀...𝑁)⟶ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥)
Theorem	fseqsupcl 14004	The values of a finite real sequence have a supremum. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐹:(𝑀...𝑁)⟶ℝ) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
Theorem	fseqsupubi 14005	The values of a finite real sequence are bounded by their supremum. (Contributed by NM, 20-Sep-2005.)
⊢ ((𝐾 ∈ (𝑀...𝑁) ∧ 𝐹:(𝑀...𝑁)⟶ℝ) → (𝐹‘𝐾) ≤ sup(ran 𝐹, ℝ, < ))
Theorem	nn0ennn 14006	The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.)
⊢ ℕ0 ≈ ℕ
Theorem	nnenom 14007	The set of positive integers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers). (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ ℕ ≈ ω
Theorem	nnct 14008	ℕ is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ ℕ ≼ ω
Theorem	uzindi 14009*	Indirect strong induction on the upper integers. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐿))    &   ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐿...𝑇) ∧ ∀𝑦(𝑆 ∈ (𝐿..^𝑅) → 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)    &   ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	axdc4uzlem 14010*	Lemma for axdc4uz 14011. (Contributed by Mario Carneiro, 8-Jan-2014.) (Revised by Mario Carneiro, 26-Dec-2014.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐺 = (rec((𝑦 ∈ V ↦ (𝑦 + 1)), 𝑀) ↾ ω)    &   ⊢ 𝐻 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ((𝐺‘𝑛)𝐹𝑥))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(𝑍 × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:𝑍⟶𝐴 ∧ (𝑔‘𝑀) = 𝐶 ∧ ∀𝑘 ∈ 𝑍 (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))))
Theorem	axdc4uz 14011*	A version of axdc4 10428 that works on an upper set of integers instead of ω. (Contributed by Mario Carneiro, 8-Jan-2014.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴 ∧ 𝐹:(𝑍 × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:𝑍⟶𝐴 ∧ (𝑔‘𝑀) = 𝐶 ∧ ∀𝑘 ∈ 𝑍 (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))))
Theorem	ssnn0fi 14012*	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 14013*	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 14014*	Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (∀𝑦 ∈ (𝑀...(𝑥 − 1))𝜓 → 𝜑))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜒)
Theorem	nnsinds 14015*	Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑁 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ (1...(𝑥 − 1))𝜓 → 𝜑))    ⇒   ⊢ (𝑁 ∈ ℕ → 𝜒)
Theorem	nn0sinds 14016*	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 14017*	Lemma for fsuppmapnn0fiub 14018 and fsuppmapnn0fiubex 14019. (Contributed by AV, 2-Oct-2019.)
⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 (𝑓 supp 𝑍)    &   ⊢ 𝑆 = sup(𝑈, ℝ, < )    ⇒   ⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → ((∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅) → 𝑆 ∈ ℕ0))
Theorem	fsuppmapnn0fiub 14018*	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 14019*	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 14020*	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 14021*	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 14022*	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 14023*	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 14024*	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 14025*	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 14026*	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 14027	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 14028	Extend class notation with recursive sequence builder.
class seq𝑀( + , 𝐹)
Definition	df-seq 14029*	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 14041 and seqp1 14043. 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 15593), by climdm 15595 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 13974 through om2uzf1oi 13980, originally proved by Raph Levien for use with df-exp 14089 and later generalized for arbitrary recursive sequences. Definition df-sum 15728 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 14030	Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ seq𝑀( + , 𝐹) ∈ V
Theorem	seqeq1 14031	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹) = seq𝑁( + , 𝐹))
Theorem	seqeq2 14032	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ ( + = 𝑄 → seq𝑀( + , 𝐹) = seq𝑀(𝑄, 𝐹))
Theorem	seqeq3 14033	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))
Theorem	seqeq1d 14034	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
Theorem	seqeq2d 14035	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝑀(𝐴, 𝐹) = seq𝑀(𝐵, 𝐹))
Theorem	seqeq3d 14036	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
Theorem	seqeq123d 14037	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑁(𝑄, 𝐺))
Theorem	nfseq 14038	Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seq𝑀( + , 𝐹)
Theorem	seqval 14039*	Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ↾ ω)    ⇒   ⊢ seq𝑀( + , 𝐹) = ran 𝑅
Theorem	seqfn 14040	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 14041	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 14042	Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014.)
⊢ 𝑀 ∈ ℤ    &   ⊢ (𝜑 → (𝐹‘𝑀) = 𝐴)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝐴)
Theorem	seqp1 14043	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 14044	Weak version of seqex 14030 that holds without ax-rep 5232. 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 14045	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	seqm1 14046	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑁) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (𝐹‘𝑁)))
Theorem	seqcl2 14047*	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 14048*	Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝐶)
Theorem	seqcl 14049*	Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆)
Theorem	seqf 14050*	Range of the recursive sequence builder (special case of seqf2 14048). (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝑆)
Theorem	seqfveq2 14051*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))
Theorem	seqfeq2 14052*	Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺))
Theorem	seqfveq 14053*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
Theorem	seqfeq 14054*	Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))
Theorem	seqshft2 14055*	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 14056	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 14057*	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 14058*	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 14059*	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 14060*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))
Theorem	sermono 14061*	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 14062*	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 14063*	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 14064*	Lemma for seqcaopr2 14065. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqcaopr2 14065*	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 14066*	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 14067*	Lemma for seqf1o 14070. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾)))
Theorem	seqf1olem1 14068*	Lemma for seqf1o 14070. (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 14069*	Lemma for seqf1o 14070. (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 14070*	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 14071*	The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	sersub 14072*	The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) − (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqid3 14073*	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 14074*	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 14075*	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 14076*	Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))
Theorem	seqz 14077*	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 14078*	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 14079*	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 14080*	The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦)))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺)‘𝑁)))
Theorem	ser0 14081	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 14082	A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0})) = (𝑍 × {0}))
Theorem	serge0 14083*	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 14084*	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 14085	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 14086*	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 14087*	Distribute function operation through a sequence. Maps-to notation version of seqof 14086. (Contributed by Mario Carneiro, 7-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)))
5.6.7  Integer powers
Syntax	cexp 14088	Extend class notation to include exponentiation of a complex number to an integer power.
class ↑
Definition	df-exp 14089*	Define exponentiation of complex numbers with integer exponents. For example, (5↑2) = 25 (ex-exp 30710). 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 14092 and expp1 14095 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 do not have superscripts. 10-Jun-2005: The definition was extended from positive exponents to nonnegative exponent, so that 0↑0 = 1, following standard convention, for instance Definition 10-4.1 of [Gleason] p. 134 (0exp0e1 14093). 4-Jun-2014: The definition was extended to integer exponents. For example, (-3↑-2) = (1 / 9) (ex-exp 30710). The case 𝑥 = 0, 𝑦 < 0 gives the "value" (1 / 0); relying on this should be avoided in applications. For a definition of exponentiation including complex exponents see df-cxp 26680 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 26790. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.)
⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦)))))
Theorem	expval 14090	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 14091	Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ × {𝐴}))‘𝑁))
Theorem	exp0 14092	Value of a complex number raised to the zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14093), following standard convention, for instance 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 14093	The zeroth power of zero equals one. See comment of exp0 14092. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0↑0) = 1
Theorem	exp1 14094	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 14095	Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. When 𝐴 is nonzero, this holds for all integers 𝑁, see expneg 14096. (Contributed by NM, 20-May-2005.) (Revised by Mario Carneiro, 2-Jul-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))
Theorem	expneg 14096	Value of a complex number raised to a nonpositive integer power. When 𝐴 = 0 and 𝑁 is nonzero, both sides have the "value" (1 / 0); relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁)))
Theorem	expneg2 14097	Value of a complex number raised to a nonpositive integer power. When 𝐴 = 0 and 𝑁 is nonzero, both sides have the "value" (1 / 0); relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁)))
Theorem	expn1 14098	A complex number raised to the negative one power is its reciprocal. When 𝐴 = 0, both sides have the "value" (1 / 0); relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴↑-1) = (1 / 𝐴))
Theorem	expcllem 14099*	Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.)
⊢ 𝐹 ⊆ ℂ    &   ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹)    &   ⊢ 1 ∈ 𝐹    ⇒   ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹)
Theorem	expcl2lem 14100*	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 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ 𝐹)