P. 89 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8801-8900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fzo0ssnn0 8801	Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ (0..^𝑁) ⊆ ℕ0
Theorem	fzo01 8802	Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (0..^1) = {0}
Theorem	fzo12sn 8803	A 1-based half-open integer interval up to, but not including, 2 is a singleton. (Contributed by Alexander van der Vekens, 31-Jan-2018.)
⊢ (1..^2) = {1}
Theorem	fzo0to2pr 8804	A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (0..^2) = {0, 1}
Theorem	fzo0to3tp 8805	A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
⊢ (0..^3) = {0, 1, 2}
Theorem	fzo0to42pr 8806	A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
⊢ (0..^4) = ({0, 1} ∪ {2, 3})
Theorem	fzo0sn0fzo1 8807	A half-open range of nonnegative integers is the union of the singleton set containing 0 and a half-open range of positive integers. (Contributed by Alexander van der Vekens, 18-May-2018.)
⊢ (𝑁 ∈ ℕ → (0..^𝑁) = ({0} ∪ (1..^𝑁)))
Theorem	fzoend 8808	The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (A ∈ (A..^B) → (B − 1) ∈ (A..^B))
Theorem	fzo0end 8809	The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
⊢ (B ∈ ℕ → (B − 1) ∈ (0..^B))
Theorem	ssfzo12 8810	Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))
Theorem	ssfzo12bi 8811	Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018.)
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))
Theorem	ubmelm1fzo 8812	The result of subtracting 1 and an integer of a half-open range of nonnegative integers from the upper bound of this range is contained in this range. (Contributed by AV, 23-Mar-2018.) (Revised by AV, 30-Oct-2018.)
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁))
Theorem	fzofzp1 8813	If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ (𝐶 ∈ (A..^B) → (𝐶 + 1) ∈ (A...B))
Theorem	fzofzp1b 8814	If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ (𝐶 ∈ (ℤ≥‘A) → (𝐶 ∈ (A..^B) ↔ (𝐶 + 1) ∈ (A...B)))
Theorem	elfzom1b 8815	An integer is a member of a 1-based finite set of sequential integers iff its predecessor is a member of the corresponding 0-based set. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (1..^𝑁) ↔ (𝐾 − 1) ∈ (0..^(𝑁 − 1))))
Theorem	elfzonelfzo 8816	If an element of a half-open integer range is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
⊢ (𝑁 ∈ ℤ → ((𝐾 ∈ (𝑀..^𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) → 𝐾 ∈ (𝑁..^𝑅)))
Theorem	elfzomelpfzo 8817	An integer increased by another integer is an element of a half-open integer range if and only if the integer is contained in the half-open integer range with bounds decreased by the other integer. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐾 ∈ ((𝑀 − 𝐿)..^(𝑁 − 𝐿)) ↔ (𝐾 + 𝐿) ∈ (𝑀..^𝑁)))
Theorem	peano2fzor 8818	A Peano-postulate-like theorem for downward closure of a half-open integer range. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀..^𝑁)) → 𝐾 ∈ (𝑀..^𝑁))
Theorem	fzosplitsn 8819	Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ (B ∈ (ℤ≥‘A) → (A..^(B + 1)) = ((A..^B) ∪ {B}))
Theorem	fzosplitprm1 8820	Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ ∧ A < B) → (A..^(B + 1)) = ((A..^(B − 1)) ∪ {(B − 1), B}))
Theorem	fzosplitsni 8821	Membership in a half-open range extended by a singleton. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ (B ∈ (ℤ≥‘A) → (𝐶 ∈ (A..^(B + 1)) ↔ (𝐶 ∈ (A..^B) ∨ 𝐶 = B)))
Theorem	fzisfzounsn 8822	A finite interval of integers as union of a half-open integer range and a singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
⊢ (B ∈ (ℤ≥‘A) → (A...B) = ((A..^B) ∪ {B}))
Theorem	fzostep1 8823	Two possibilities for a number one greater than a number in a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ (A ∈ (B..^𝐶) → ((A + 1) ∈ (B..^𝐶) ∨ (A + 1) = 𝐶))
Theorem	fzoshftral 8824*	Shift the scanning order inside of a quantification over a half-open integer range, analogous to fzshftral 8700. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀..^𝑁)φ ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)..^(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]φ))
Theorem	fzind2 8825*	Induction on the integers from 𝑀 to 𝑁 inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Version of fzind 8089 using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016.)
⊢ (x = 𝑀 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = 𝐾 → (φ ↔ τ))    &   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ψ)    &   ⊢ (y ∈ (𝑀..^𝑁) → (χ → θ))    ⇒   ⊢ (𝐾 ∈ (𝑀...𝑁) → τ)
3.5.7  Miscellaneous theorems about integers
Theorem	frec2uz0d 8826*	The mapping 𝐺 is a one-to-one mapping from 𝜔 onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number 𝐶 (normally 0 for the upper integers ℕ0 or 1 for the upper integers ℕ), 1 maps to 𝐶 + 1, etc. This theorem shows the value of 𝐺 at ordinal natural number zero. (Contributed by Jim Kingdon, 16-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    ⇒   ⊢ (φ → (𝐺‘∅) = 𝐶)
Theorem	frec2uzzd 8827*	The value of 𝐺 (see frec2uz0d 8826) is an integer. (Contributed by Jim Kingdon, 16-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → A ∈ 𝜔)    ⇒   ⊢ (φ → (𝐺‘A) ∈ ℤ)
Theorem	frec2uzsucd 8828*	The value of 𝐺 (see frec2uz0d 8826) at a successor. (Contributed by Jim Kingdon, 16-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → A ∈ 𝜔)    ⇒   ⊢ (φ → (𝐺‘suc A) = ((𝐺‘A) + 1))
Theorem	frec2uzuzd 8829*	The value 𝐺 (see frec2uz0d 8826) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → A ∈ 𝜔)    ⇒   ⊢ (φ → (𝐺‘A) ∈ (ℤ≥‘𝐶))
Theorem	frec2uzltd 8830*	Less-than relation for 𝐺 (see frec2uz0d 8826). (Contributed by Jim Kingdon, 16-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → A ∈ 𝜔)    &   ⊢ (φ → B ∈ 𝜔)    ⇒   ⊢ (φ → (A ∈ B → (𝐺‘A) < (𝐺‘B)))
Theorem	frec2uzlt2d 8831*	The mapping 𝐺 (see frec2uz0d 8826) preserves order. (Contributed by Jim Kingdon, 16-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → A ∈ 𝜔)    &   ⊢ (φ → B ∈ 𝜔)    ⇒   ⊢ (φ → (A ∈ B ↔ (𝐺‘A) < (𝐺‘B)))
Theorem	frec2uzrand 8832*	Range of 𝐺 (see frec2uz0d 8826). (Contributed by Jim Kingdon, 17-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    ⇒   ⊢ (φ → ran 𝐺 = (ℤ≥‘𝐶))
Theorem	frec2uzf1od 8833*	𝐺 (see frec2uz0d 8826) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    ⇒   ⊢ (φ → 𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶))
Theorem	frec2uzisod 8834*	𝐺 (see frec2uz0d 8826) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    ⇒   ⊢ (φ → 𝐺 Isom E , < (𝜔, (ℤ≥‘𝐶)))
Theorem	frecuzrdgrrn 8835*	The function 𝑅 (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of 𝑆. (Contributed by Jim Kingdon, 27-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    ⇒   ⊢ ((φ ∧ 𝐷 ∈ 𝜔) → (𝑅‘𝐷) ∈ ((ℤ≥‘𝐶) × 𝑆))
Theorem	frec2uzrdg 8836*	A helper lemma for the value of a recursive definition generator on upper integers (typically either ℕ or ℕ0) with characteristic function 𝐹(x, y) and initial value A. This lemma shows that evaluating 𝑅 at an element of 𝜔 gives an ordered pair whose first element is the index (translated from 𝜔 to (ℤ≥‘𝐶)). See comment in frec2uz0d 8826 which describes 𝐺 and the index translation. (Contributed by Jim Kingdon, 24-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    &   ⊢ (φ → B ∈ 𝜔)    ⇒   ⊢ (φ → (𝑅‘B) = ⟨(𝐺‘B), (2nd ‘(𝑅‘B))⟩)
Theorem	frecuzrdgrom 8837*	The function 𝑅 (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 26-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    ⇒   ⊢ (φ → 𝑅 Fn 𝜔)
Theorem	frecuzrdglem 8838*	A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    &   ⊢ (φ → B ∈ (ℤ≥‘𝐶))    ⇒   ⊢ (φ → ⟨B, (2nd ‘(𝑅‘(◡𝐺‘B)))⟩ ∈ ran 𝑅)
Theorem	frecuzrdgfn 8839*	The recursive definition generator on upper integers is a function. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 26-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    &   ⊢ (φ → 𝑇 = ran 𝑅)    ⇒   ⊢ (φ → 𝑇 Fn (ℤ≥‘𝐶))
Theorem	frecuzrdgcl 8840*	Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 31-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    &   ⊢ (φ → 𝑇 = ran 𝑅)    ⇒   ⊢ ((φ ∧ B ∈ (ℤ≥‘𝐶)) → (𝑇‘B) ∈ 𝑆)
Theorem	frecuzrdg0 8841*	Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 27-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    &   ⊢ (φ → 𝑇 = ran 𝑅)    ⇒   ⊢ (φ → (𝑇‘𝐶) = A)
Theorem	frecuzrdgsuc 8842*	Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 8826 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 28-May-2020.)
⊢ (φ → 𝐶 ∈ ℤ)    &   ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → A ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)    &   ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    &   ⊢ (φ → 𝑇 = ran 𝑅)    ⇒   ⊢ ((φ ∧ B ∈ (ℤ≥‘𝐶)) → (𝑇‘(B + 1)) = (B𝐹(𝑇‘B)))
Theorem	uzenom 8843	An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → 𝑍 ≈ 𝜔)
Theorem	frecfzennn 8844	The cardinality of a finite set of sequential integers. (See frec2uz0d 8826 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.)
⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) ≈ (◡𝐺‘𝑁))
Theorem	frecfzen2 8845	The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.)
⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡𝐺‘((𝑁 + 1) − 𝑀)))
Theorem	frechashgf1o 8846	𝐺 maps 𝜔 one-to-one onto ℕ0. (Contributed by Jim Kingdon, 19-May-2020.)
⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0)    ⇒   ⊢ 𝐺:𝜔–1-1-onto→ℕ0
Theorem	fzfig 8847	A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ Fin)
Theorem	fzfigd 8848	Deduction form of fzfig 8847. (Contributed by Jim Kingdon, 21-May-2020.)
⊢ (φ → 𝑀 ∈ ℤ)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (𝑀...𝑁) ∈ Fin)
Theorem	fzofig 8849	Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin)
Theorem	nn0ennn 8850	The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.)
⊢ ℕ0 ≈ ℕ
Theorem	nnenom 8851	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.)
⊢ ℕ ≈ 𝜔
3.5.8  The infinite sequence builder "seq"
Syntax	cseq 8852	Extend class notation with recursive sequence builder.
class seq𝑀( + , 𝐹, 𝑆)
Definition	df-iseq 8853*	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 iseq1 8862 and at successors. 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. Internally, the frec function generates as its values a set of ordered pairs starting at ⟨𝑀, (𝐹‘𝑀)⟩, with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by Jim Kingdon, 29-May-2020.)
⊢ seq𝑀( + , 𝐹, 𝑆) = ran frec((x ∈ (ℤ≥‘𝑀), y ∈ 𝑆 ↦ ⟨(x + 1), (y + (𝐹‘(x + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
Theorem	iseqeq1 8854	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹, 𝑆) = seq𝑁( + , 𝐹, 𝑆))
Theorem	iseqeq2 8855	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
⊢ ( + = 𝑄 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀(𝑄, 𝐹, 𝑆))
Theorem	iseqeq3 8856	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆))
Theorem	iseqeq4 8857	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
⊢ (𝑆 = 𝑇 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇))
Theorem	nfiseq 8858	Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
⊢ Ⅎx𝑀    &   ⊢ Ⅎx +    &   ⊢ Ⅎx𝐹    &   ⊢ Ⅎx𝑆    ⇒   ⊢ Ⅎxseq𝑀( + , 𝐹, 𝑆)
Theorem	iseqovex 8859*	Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.)
⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    ⇒   ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝑀) ∧ y ∈ 𝑆)) → (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y) ∈ 𝑆)
Theorem	iseqval 8860*	Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.)
⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝑀), y ∈ 𝑆 ↦ ⟨(x + 1), (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y)⟩), ⟨𝑀, (𝐹‘𝑀)⟩)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    ⇒   ⊢ (φ → seq𝑀( + , 𝐹, 𝑆) = ran 𝑅)
Theorem	iseqfn 8861*	The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.)
⊢ (φ → 𝑀 ∈ ℤ)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    ⇒   ⊢ (φ → seq𝑀( + , 𝐹, 𝑆) Fn (ℤ≥‘𝑀))
Theorem	iseq1 8862*	Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.)
⊢ (φ → 𝑀 ∈ ℤ)    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    ⇒   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀))
Theorem	iseqcl 8863*	Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.)
⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    ⇒   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) ∈ 𝑆)
Theorem	iseqp1 8864*	Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.)
⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    ⇒   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1))))
Theorem	iseqfveq2 8865*	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
⊢ (φ → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺‘𝐾))    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    &   ⊢ (φ → 𝑁 ∈ (ℤ≥‘𝐾))    &   ⊢ ((φ ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁))
Theorem	iseqfeq2 8866*	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
⊢ (φ → 𝐾 ∈ (ℤ≥‘𝑀))    &   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺‘𝐾))    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝐾)) → (𝐺‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    &   ⊢ ((φ ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆) ↾ (ℤ≥‘𝐾)) = seq𝐾( + , 𝐺, 𝑆))
Theorem	iseqfveq 8867*	Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.)
⊢ (φ → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((φ ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘𝑘))    &   ⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐺‘x) ∈ 𝑆)    &   ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)    ⇒   ⊢ (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝑀( + , 𝐺, 𝑆)‘𝑁))
3.5.9  Integer powers
Syntax	cexp 8868	Extend class notation to include exponentiation of a complex number to an integer power.
class ↑
Definition	df-iexp 8869*	Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 8873 and expp1 8876 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. 4-Jun-2014: The definition was extended to include negative integer exponents. The case x = 0, y < 0 gives the value (1 / 0), so we will avoid this case in our theorems. (Contributed by Jim Kingodon, 7-Jun-2020.)
⊢ ↑ = (x ∈ ℂ, y ∈ ℤ ↦ if(y = 0, 1, if(0 < y, (seq1( · , (ℕ × {x}), ℂ)‘y), (1 / (seq1( · , (ℕ × {x}), ℂ)‘-y)))))
Theorem	expivallem 8870	Lemma for expival 8871. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingodon, 7-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℕ) → (seq1( · , (ℕ × {A}), ℂ)‘𝑁) # 0)
Theorem	expival 8871	Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (A # 0 ∨ 0 ≤ 𝑁)) → (A↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {A}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {A}), ℂ)‘-𝑁)))))
Theorem	expinnval 8872	Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → (A↑𝑁) = (seq1( · , (ℕ × {A}), ℂ)‘𝑁))
Theorem	exp0 8873	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.)
⊢ (A ∈ ℂ → (A↑0) = 1)
Theorem	0exp0e1 8874	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 8875	Value of a complex number raised to the first power. (Contributed by NM, 20-Oct-2004.) (Revised by Mario Carneiro, 2-Jul-2013.)
⊢ (A ∈ ℂ → (A↑1) = A)
Theorem	expp1 8876	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.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (A↑(𝑁 + 1)) = ((A↑𝑁) · A))
Theorem	expnegap0 8877	Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℕ0) → (A↑-𝑁) = (1 / (A↑𝑁)))
Theorem	expineg2 8878	Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)) → (A↑𝑁) = (1 / (A↑-𝑁)))
Theorem	expn1ap0 8879	A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0) → (A↑-1) = (1 / A))
Theorem	expcllem 8880*	Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.)
⊢ 𝐹 ⊆ ℂ    &   ⊢ ((x ∈ 𝐹 ∧ y ∈ 𝐹) → (x · y) ∈ 𝐹)    &   ⊢ 1 ∈ 𝐹    ⇒   ⊢ ((A ∈ 𝐹 ∧ B ∈ ℕ0) → (A↑B) ∈ 𝐹)
Theorem	expcl2lemap 8881*	Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.)
⊢ 𝐹 ⊆ ℂ    &   ⊢ ((x ∈ 𝐹 ∧ y ∈ 𝐹) → (x · y) ∈ 𝐹)    &   ⊢ 1 ∈ 𝐹    &   ⊢ ((x ∈ 𝐹 ∧ x # 0) → (1 / x) ∈ 𝐹)    ⇒   ⊢ ((A ∈ 𝐹 ∧ A # 0 ∧ B ∈ ℤ) → (A↑B) ∈ 𝐹)
Theorem	nnexpcl 8882	Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.)
⊢ ((A ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈ ℕ)
Theorem	nn0expcl 8883	Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.)
⊢ ((A ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈ ℕ0)
Theorem	zexpcl 8884	Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.)
⊢ ((A ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈ ℤ)
Theorem	qexpcl 8885	Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.)
⊢ ((A ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈ ℚ)
Theorem	reexpcl 8886	Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈ ℝ)
Theorem	expcl 8887	Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ∈ ℂ)
Theorem	rpexpcl 8888	Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.)
⊢ ((A ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℝ+)
Theorem	reexpclzap 8889	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ ((A ∈ ℝ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℝ)
Theorem	qexpclz 8890	Closure of exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((A ∈ ℚ ∧ A ≠ 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℚ)
Theorem	m1expcl2 8891	Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1, 1})
Theorem	m1expcl 8892	Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℤ)
Theorem	expclzaplem 8893*	Closure law for integer exponentiation. Lemma for expclzap 8894 and expap0i 8901. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ {z ∈ ℂ ∣ z # 0})
Theorem	expclzap 8894	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) ∈ ℂ)
Theorem	nn0expcli 8895	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ (A↑𝑁) ∈ ℕ0
Theorem	nn0sqcl 8896	The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (A ∈ ℕ0 → (A↑2) ∈ ℕ0)
Theorem	expm1t 8897	Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → (A↑𝑁) = ((A↑(𝑁 − 1)) · A))
Theorem	1exp 8898	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	expap0 8899	Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 8900 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((A↑𝑁) # 0 ↔ A # 0))
Theorem	expeq0 8900	Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((A↑𝑁) = 0 ↔ A = 0))