P. 129 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
5.6.6  The infinite sequence builder "seq" - extension
Syntax	cseq 12801	Extend class notation with recursive sequence builder.
class seq𝑀( + , 𝐹)
Definition	df-seq 12802*	Define a general-purpose operation that builds a recursive sequence (i.e. a function on the positive integers ℕ or some other upper integer set) 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 12814 and seqp1 12816. 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 14283), by climdm 14285 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 12746 through om2uzf1oi 12752, originally proved by Raph Levien for use with df-exp 12861 and later generalized for arbitrary recursive sequences. Definition df-sum 14417 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 12803	Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ seq𝑀( + , 𝐹) ∈ V
Theorem	seqeq1 12804	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹) = seq𝑁( + , 𝐹))
Theorem	seqeq2 12805	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ ( + = 𝑄 → seq𝑀( + , 𝐹) = seq𝑀(𝑄, 𝐹))
Theorem	seqeq3 12806	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))
Theorem	seqeq1d 12807	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝐴( + , 𝐹) = seq𝐵( + , 𝐹))
Theorem	seqeq2d 12808	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝑀(𝐴, 𝐹) = seq𝑀(𝐵, 𝐹))
Theorem	seqeq3d 12809	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐴) = seq𝑀( + , 𝐵))
Theorem	seqeq123d 12810	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑁(𝑄, 𝐺))
Theorem	nfseq 12811	Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seq𝑀( + , 𝐹)
Theorem	seqval 12812*	Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ↾ ω)    ⇒   ⊢ seq𝑀( + , 𝐹) = ran 𝑅
Theorem	seqfn 12813	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 12814	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 12815	Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014.)
⊢ 𝑀 ∈ ℤ    &   ⊢ (𝜑 → (𝐹‘𝑀) = 𝐴)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = 𝐴)
Theorem	seqp1 12816	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 12817	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 30-Apr-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑁 ∈ 𝑍    &   ⊢ 𝐾 = (𝑁 + 1)    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐾) = 𝐵)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐴 + 𝐵))
Theorem	seqm1 12818	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑁) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (𝐹‘𝑁)))
Theorem	seqcl2 12819*	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 12820*	Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝐶)
Theorem	seqcl 12821*	Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ 𝑆)
Theorem	seqf 12822*	Range of the recursive sequence builder (special case of seqf2 12820). (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶𝑆)
Theorem	seqfveq2 12823*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝐾( + , 𝐺)‘𝑁))
Theorem	seqfeq2 12824*	Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐺‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺))
Theorem	seqfveq 12825*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
Theorem	seqfeq 12826*	Equality of sequences. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))
Theorem	seqshft2 12827*	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 12828	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 12829*	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 12830*	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 12831*	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 12832*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))
Theorem	sermono 12833*	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 12834*	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 12835*	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 12836*	Lemma for seqcaopr2 12837. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqcaopr2 12837*	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 12838*	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 12839*	Lemma for seqf1o 12842. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾)))
Theorem	seqf1olem1 12840*	Lemma for seqf1o 12842. (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 12841*	Lemma for seqf1o 12842. (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 12842*	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 12843*	The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	sersub 12844*	The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) − (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqid3 12845*	A sequence that consists entirely of zeroes (or whatever the identity 𝑍 is for operation +) sums to zero. (Contributed by Mario Carneiro, 15-Dec-2014.)
⊢ (𝜑 → (𝑍 + 𝑍) = 𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = 𝑍)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍)
Theorem	seqid 12846*	Discard the first few terms of a sequence that starts with all zeroes (or whatever the identity 𝑍 is for operation +). (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑥)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑥) = 𝑍)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( + , 𝐹))
Theorem	seqid2 12847*	The last few terms of a sequence that ends with all zeroes (or whatever the identity 𝑍 is for operation +) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑥)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾))    &   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑥) = 𝑍)    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁))
Theorem	seqhomo 12848*	Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁))
Theorem	seqz 12849*	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 12850*	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 12851*	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 12852*	The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦)))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺)‘𝑁)))
Theorem	ser0 12853	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 12854	A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0})) = (𝑍 × {0}))
Theorem	serge0 12855*	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 12856*	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 12857	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 12858*	Distribute function operation through a sequence. Note that 𝐺(𝑧) is an implicit function on 𝑧. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → (seq𝑀( ∘𝑓 + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁)))
Theorem	seqof2 12859*	Distribute function operation through a sequence. Maps-to notation version of seqof 12858. (Contributed by Mario Carneiro, 7-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (seq𝑀( ∘𝑓 + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁)))
5.6.7  Integer powers
Syntax	cexp 12860	Extend class notation to include exponentiation of a complex number to an integer power.
class ↑
Definition	df-exp 12861*	Define exponentiation to nonnegative integer powers. For example, (5↑2) = 25 (ex-exp 27307). This definition is not meant to be used directly; instead, exp0 12864 and expp1 12867 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 12865). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3↑-2) = (1 / 9) (ex-exp 27307). The case 𝑥 = 0, 𝑦 < 0 gives the value (1 / 0), so we will avoid this case in our theorems. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.)
⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦)))))
Theorem	expval 12862	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 12863	Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ × {𝐴}))‘𝑁))
Theorem	exp0 12864	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 12865	0↑0 = 1 (common case). 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 12866	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 12867	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 12868	Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁)))
Theorem	expneg2 12869	Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁)))
Theorem	expn1 12870	A number to the negative one power is the reciprocal. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴↑-1) = (1 / 𝐴))
Theorem	expcllem 12871*	Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.)
⊢ 𝐹 ⊆ ℂ    &   ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹)    &   ⊢ 1 ∈ 𝐹    ⇒   ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹)
Theorem	expcl2lem 12872*	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 12873	Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ)
Theorem	nn0expcl 12874	Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ0)
Theorem	zexpcl 12875	Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ)
Theorem	qexpcl 12876	Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ)
Theorem	reexpcl 12877	Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ)
Theorem	expcl 12878	Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ)
Theorem	rpexpcl 12879	Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+)
Theorem	reexpclz 12880	Closure of exponentiation of reals. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ)
Theorem	qexpclz 12881	Closure of exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℚ)
Theorem	m1expcl2 12882	Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1, 1})
Theorem	m1expcl 12883	Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℤ)
Theorem	expclzlem 12884	Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ (ℂ ∖ {0}))
Theorem	expclz 12885	Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ)
Theorem	nn0expcli 12886	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ (𝐴↑𝑁) ∈ ℕ0
Theorem	nn0sqcl 12887	The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (𝐴 ∈ ℕ0 → (𝐴↑2) ∈ ℕ0)
Theorem	expm1t 12888	Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = ((𝐴↑(𝑁 − 1)) · 𝐴))
Theorem	1exp 12889	Value of one raised to a nonnegative integer power. (Contributed by NM, 15-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (𝑁 ∈ ℤ → (1↑𝑁) = 1)
Theorem	expeq0 12890	Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0))
Theorem	expne0 12891	Positive integer exponentiation is nonzero iff its mantissa is nonzero. (Contributed by NM, 6-May-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) ≠ 0 ↔ 𝐴 ≠ 0))
Theorem	expne0i 12892	Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ≠ 0)
Theorem	expgt0 12893	Nonnegative integer exponentiation with a positive mantissa is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴) → 0 < (𝐴↑𝑁))
Theorem	expnegz 12894	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁)))
Theorem	0exp 12895	Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0)
Theorem	expge0 12896	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → 0 ≤ (𝐴↑𝑁))
Theorem	expge1 12897	Nonnegative integer exponentiation with a mantissa greater than or equal to 1 is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝐴) → 1 ≤ (𝐴↑𝑁))
Theorem	expgt1 12898	Positive integer exponentiation with a mantissa greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝐴) → 1 < (𝐴↑𝑁))
Theorem	mulexp 12899	Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁)))
Theorem	mulexpz 12900	Integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁)))