Home Intuitionistic Logic ExplorerTheorem List (p. 89 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

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

Theoremfzosubel2 8801 Membership in a translated half-open integer range implies translated membership in the original range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
((A ((B + 𝐶)..^(B + 𝐷)) (B 𝐶 𝐷 ℤ)) → (AB) (𝐶..^𝐷))

Theoremfzosubel3 8802 Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015.)
((A (B..^(B + 𝐷)) 𝐷 ℤ) → (AB) (0..^𝐷))

Theoremeluzgtdifelfzo 8803 Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
((A B ℤ) → ((𝑁 (ℤA) B < A) → (𝑁A) (0..^(𝑁B))))

Theoremige2m2fzo 8804 Membership of an integer greater than 1 decreased by 2 in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
(𝑁 (ℤ‘2) → (𝑁 − 2) (0..^(𝑁 − 1)))

Theoremfzocatel 8805 Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018.)
(((A (0..^(B + 𝐶)) ¬ A (0..^B)) (B 𝐶 ℤ)) → (AB) (0..^𝐶))

Theoremubmelfzo 8806 If an integer in a 1 based finite set of sequential integers is subtracted from the upper bound of this finite set of sequential integers, the result is contained in a half-open range of nonnegative integers with the same upper bound. (Contributed by AV, 18-Mar-2018.) (Revised by AV, 30-Oct-2018.)
(𝐾 (1...𝑁) → (𝑁𝐾) (0..^𝑁))

Theoremelfzodifsumelfzo 8807 If an integer is in a half-open range of nonnegative integers with a difference as upper bound, the sum of the integer with the subtrahend of the difference is in the a half-open range of nonnegative integers containing the minuend of the difference. (Contributed by AV, 13-Nov-2018.)
((𝑀 (0...𝑁) 𝑁 (0...𝑃)) → (𝐼 (0..^(𝑁𝑀)) → (𝐼 + 𝑀) (0..^𝑃)))

Theoremelfzom1elp1fzo 8808 Membership of an integer incremented by one in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Proof shortened by AV, 5-Jan-2020.)
((𝑁 𝐼 (0..^(𝑁 − 1))) → (𝐼 + 1) (0..^𝑁))

Theoremelfzom1elfzo 8809 Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.)
((𝑁 𝐼 (0..^(𝑁 − 1))) → 𝐼 (0..^𝑁))

Theoremfzval3 8810 Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
(𝑁 ℤ → (𝑀...𝑁) = (𝑀..^(𝑁 + 1)))

Theoremfzosn 8811 Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
(A ℤ → (A..^(A + 1)) = {A})

Theoremelfzomin 8812 Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
(𝑍 ℤ → 𝑍 (𝑍..^(𝑍 + 1)))

Theoremzpnn0elfzo 8813 Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
((𝑍 𝑁 0) → (𝑍 + 𝑁) (𝑍..^((𝑍 + 𝑁) + 1)))

Theoremzpnn0elfzo1 8814 Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
((𝑍 𝑁 0) → (𝑍 + 𝑁) (𝑍..^(𝑍 + (𝑁 + 1))))

Theoremfzosplitsnm1 8815 Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
((A B (ℤ‘(A + 1))) → (A..^B) = ((A..^(B − 1)) ∪ {(B − 1)}))

Theoremelfzonlteqm1 8816 If an element of a half-open integer range is not less than the upper bound of the range decreased by 1, it must be equal to the upper bound of the range decreased by 1. (Contributed by AV, 3-Nov-2018.)
((A (0..^B) ¬ A < (B − 1)) → A = (B − 1))

Theoremfzonn0p1 8817 A nonnegative integer is element of the half-open range of nonnegative integers with the element increased by one as an upper bound. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
(𝑁 0𝑁 (0..^(𝑁 + 1)))

Theoremfzossfzop1 8818 A half-open range of nonnegative integers is a subset of a half-open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
(𝑁 0 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))

Theoremfzonn0p1p1 8819 If a nonnegative integer is element of a half-open range of nonnegative integers, increasing this integer by one results in an element of a half- open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
(𝐼 (0..^𝑁) → (𝐼 + 1) (0..^(𝑁 + 1)))

Theoremelfzom1p1elfzo 8820 Increasing an element of a half-open range of nonnegative integers by 1 results in an element of the half-open range of nonnegative integers with an upper bound increased by 1. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
((𝑁 𝑋 (0..^(𝑁 − 1))) → (𝑋 + 1) (0..^𝑁))

Theoremfzo0ssnn0 8821 Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.)
(0..^𝑁) ⊆ ℕ0

Theoremfzo01 8822 Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
(0..^1) = {0}

Theoremfzo12sn 8823 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}

Theoremfzo0to2pr 8824 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}

Theoremfzo0to3tp 8825 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}

Theoremfzo0to42pr 8826 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})

Theoremfzo0sn0fzo1 8827 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..^𝑁)))

Theoremfzoend 8828 The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.)
(A (A..^B) → (B − 1) (A..^B))

Theoremfzo0end 8829 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))

Theoremssfzo12 8830 Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
((𝐾 𝐿 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀𝐾 𝐿𝑁)))

Theoremssfzo12bi 8831 Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018.)
(((𝐾 𝐿 ℤ) (𝑀 𝑁 ℤ) 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ↔ (𝑀𝐾 𝐿𝑁)))

Theoremubmelm1fzo 8832 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..^𝑁))

Theoremfzofzp1 8833 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))

Theoremfzofzp1b 8834 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)))

Theoremelfzom1b 8835 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))))

Theoremelfzonelfzo 8836 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.)
(𝑁 ℤ → ((𝐾 (𝑀..^𝑅) ¬ 𝐾 (𝑀..^𝑁)) → 𝐾 (𝑁..^𝑅)))

Theoremelfzomelpfzo 8837 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.)
(((𝑀 𝑁 ℤ) (𝐾 𝐿 ℤ)) → (𝐾 ((𝑀𝐿)..^(𝑁𝐿)) ↔ (𝐾 + 𝐿) (𝑀..^𝑁)))

Theorempeano2fzor 8838 A Peano-postulate-like theorem for downward closure of a half-open integer range. (Contributed by Mario Carneiro, 1-Oct-2015.)
((𝐾 (ℤ𝑀) (𝐾 + 1) (𝑀..^𝑁)) → 𝐾 (𝑀..^𝑁))

Theoremfzosplitsn 8839 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}))

Theoremfzosplitprm1 8840 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}))

Theoremfzosplitsni 8841 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)))

Theoremfzisfzounsn 8842 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}))

Theoremfzostep1 8843 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) = 𝐶))

Theoremfzoshftral 8844* Shift the scanning order inside of a quantification over a half-open integer range, analogous to fzshftral 8720. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
((𝑀 𝑁 𝐾 ℤ) → (𝑗 (𝑀..^𝑁)φ𝑘 ((𝑀 + 𝐾)..^(𝑁 + 𝐾))[(𝑘𝐾) / 𝑗]φ))

Theoremfzind2 8845* 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 8109 using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016.)
(x = 𝑀 → (φψ))    &   (x = y → (φχ))    &   (x = (y + 1) → (φθ))    &   (x = 𝐾 → (φτ))    &   (𝑁 (ℤ𝑀) → ψ)    &   (y (𝑀..^𝑁) → (χθ))       (𝐾 (𝑀...𝑁) → τ)

Theoremfrec2uz0d 8846* 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)), 𝐶)       (φ → (𝐺‘∅) = 𝐶)

Theoremfrec2uzzd 8847* The value of 𝐺 (see frec2uz0d 8846) is an integer. (Contributed by Jim Kingdon, 16-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)    &   (φA 𝜔)       (φ → (𝐺A) ℤ)

Theoremfrec2uzsucd 8848* The value of 𝐺 (see frec2uz0d 8846) at a successor. (Contributed by Jim Kingdon, 16-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)    &   (φA 𝜔)       (φ → (𝐺‘suc A) = ((𝐺A) + 1))

Theoremfrec2uzuzd 8849* The value 𝐺 (see frec2uz0d 8846) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)    &   (φA 𝜔)       (φ → (𝐺A) (ℤ𝐶))

Theoremfrec2uzltd 8850* Less-than relation for 𝐺 (see frec2uz0d 8846). (Contributed by Jim Kingdon, 16-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)    &   (φA 𝜔)    &   (φB 𝜔)       (φ → (A B → (𝐺A) < (𝐺B)))

Theoremfrec2uzlt2d 8851* The mapping 𝐺 (see frec2uz0d 8846) preserves order. (Contributed by Jim Kingdon, 16-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)    &   (φA 𝜔)    &   (φB 𝜔)       (φ → (A B ↔ (𝐺A) < (𝐺B)))

Theoremfrec2uzrand 8852* Range of 𝐺 (see frec2uz0d 8846). (Contributed by Jim Kingdon, 17-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)       (φ → ran 𝐺 = (ℤ𝐶))

Theoremfrec2uzf1od 8853* 𝐺 (see frec2uz0d 8846) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)       (φ𝐺:𝜔–1-1-onto→(ℤ𝐶))

Theoremfrec2uzisod 8854* 𝐺 (see frec2uz0d 8846) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)       (φ𝐺 Isom E , < (𝜔, (ℤ𝐶)))

Theoremfrecuzrdgrrn 8855* 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⟩)       ((φ 𝐷 𝜔) → (𝑅𝐷) ((ℤ𝐶) × 𝑆))

Theoremfrec2uzrdg 8856* 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 8846 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))⟩)

Theoremfrecuzrdgrom 8857* 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 𝜔)

Theoremfrecuzrdglem 8858* 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 𝑅)

Theoremfrecuzrdgfn 8859* The recursive definition generator on upper integers is a function. See comment in frec2uz0d 8846 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 (ℤ𝐶))

Theoremfrecuzrdgcl 8860* Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8846 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) 𝑆)

Theoremfrecuzrdg0 8861* Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 8846 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)

Theoremfrecuzrdgsuc 8862* Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 8846 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)))

Theoremuzenom 8863 An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015.)
𝑍 = (ℤ𝑀)       (𝑀 ℤ → 𝑍 ≈ 𝜔)

Theoremfrecfzennn 8864 The cardinality of a finite set of sequential integers. (See frec2uz0d 8846 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.)
𝐺 = frec((x ℤ ↦ (x + 1)), 0)       (𝑁 0 → (1...𝑁) ≈ (𝐺𝑁))

Theoremfrecfzen2 8865 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) − 𝑀)))

Theoremfrechashgf1o 8866 𝐺 maps 𝜔 one-to-one onto 0. (Contributed by Jim Kingdon, 19-May-2020.)
𝐺 = frec((x ℤ ↦ (x + 1)), 0)       𝐺:𝜔–1-1-onto→ℕ0

Theoremfzfig 8867 A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.)
((𝑀 𝑁 ℤ) → (𝑀...𝑁) Fin)

Theoremfzfigd 8868 Deduction form of fzfig 8867. (Contributed by Jim Kingdon, 21-May-2020.)
(φ𝑀 ℤ)    &   (φ𝑁 ℤ)       (φ → (𝑀...𝑁) Fin)

Theoremfzofig 8869 Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.)
((𝑀 𝑁 ℤ) → (𝑀..^𝑁) Fin)

Theoremnn0ennn 8870 The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.)
0 ≈ ℕ

Theoremnnenom 8871 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"

Syntaxcseq 8872 Extend class notation with recursive sequence builder.
class seq𝑀( + , 𝐹, 𝑆)

Definitiondf-iseq 8873* 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 8882 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)))⟩), ⟨𝑀, (𝐹𝑀)⟩)

Theoremiseqeq1 8874 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝑀 = 𝑁 → seq𝑀( + , 𝐹, 𝑆) = seq𝑁( + , 𝐹, 𝑆))

Theoremiseqeq2 8875 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
( + = 𝑄 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀(𝑄, 𝐹, 𝑆))

Theoremiseqeq3 8876 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝐹 = 𝐺 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆))

Theoremiseqeq4 8877 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝑆 = 𝑇 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇))

Theoremnfiseq 8878 Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
x𝑀    &   x +    &   x𝐹    &   x𝑆       xseq𝑀( + , 𝐹, 𝑆)

Theoremiseqovex 8879* 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) 𝑆)

Theoremiseqval 8880* 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 𝑅)

Theoremiseqfn 8881* The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.)
(φ𝑀 ℤ)    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → seq𝑀( + , 𝐹, 𝑆) Fn (ℤ𝑀))

Theoremiseq1 8882* Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.)
(φ𝑀 ℤ)    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹𝑀))

Theoremiseqcl 8883* Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.)
(φ𝑁 (ℤ𝑀))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) 𝑆)

Theoremiseqp1 8884* 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))))

Theoremiseqfveq2 8885* Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
(φ𝐾 (ℤ𝑀))    &   (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺𝐾))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ x (ℤ𝐾)) → (𝐺x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)    &   (φ𝑁 (ℤ𝐾))    &   ((φ 𝑘 ((𝐾 + 1)...𝑁)) → (𝐹𝑘) = (𝐺𝑘))       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁))

Theoremiseqfeq2 8886* Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
(φ𝐾 (ℤ𝑀))    &   (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺𝐾))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ x (ℤ𝐾)) → (𝐺x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)    &   ((φ 𝑘 (ℤ‘(𝐾 + 1))) → (𝐹𝑘) = (𝐺𝑘))       (φ → (seq𝑀( + , 𝐹, 𝑆) ↾ (ℤ𝐾)) = seq𝐾( + , 𝐺, 𝑆))

Theoremiseqfveq 8887* 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

Syntaxcexp 8888 Extend class notation to include exponentiation of a complex number to an integer power.
class

Definitiondf-iexp 8889* Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 8893 and expp1 8896 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)))))

Theoremexpivallem 8890 Lemma for expival 8891. 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)

Theoremexpival 8891 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}), ℂ)‘-𝑁)))))

Theoremexpinnval 8892 Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.)
((A 𝑁 ℕ) → (A𝑁) = (seq1( · , (ℕ × {A}), ℂ)‘𝑁))

Theoremexp0 8893 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)

Theorem0exp0e1 8894 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

Theoremexp1 8895 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)

Theoremexpp1 8896 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))

Theoremexpnegap0 8897 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𝑁)))

Theoremexpineg2 8898 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↑-𝑁)))

Theoremexpn1ap0 8899 A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.)
((A A # 0) → (A↑-1) = (1 / A))

Theoremexpcllem 8900* Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.)
𝐹 ⊆ ℂ    &   ((x 𝐹 y 𝐹) → (x · y) 𝐹)    &   1 𝐹       ((A 𝐹 B 0) → (AB) 𝐹)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9427
 Copyright terms: Public domain < Previous  Next >