HomeHome Metamath Proof Explorer
Theorem List (p. 318 of 449)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-28622)
  Hilbert Space Explorer  Hilbert Space Explorer
(28623-30145)
  Users' Mathboxes  Users' Mathboxes
(30146-44834)
 

Theorem List for Metamath Proof Explorer - 31701-31800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsgnsub 31701 Subtraction of a number of opposite sign. (Contributed by Thierry Arnoux, 2-Oct-2018.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → (sgn‘(𝐴𝐵)) = (sgn‘𝐴))
 
Theoremsgnnbi 31702 Negative signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
(𝐴 ∈ ℝ* → ((sgn‘𝐴) = -1 ↔ 𝐴 < 0))
 
Theoremsgnpbi 31703 Positive signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
(𝐴 ∈ ℝ* → ((sgn‘𝐴) = 1 ↔ 0 < 𝐴))
 
Theoremsgn0bi 31704 Zero signum. (Contributed by Thierry Arnoux, 10-Oct-2018.)
(𝐴 ∈ ℝ* → ((sgn‘𝐴) = 0 ↔ 𝐴 = 0))
 
Theoremsgnsgn 31705 Signum is idempotent. (Contributed by Thierry Arnoux, 2-Oct-2018.)
(𝐴 ∈ ℝ* → (sgn‘(sgn‘𝐴)) = (sgn‘𝐴))
 
Theoremsgnmulsgn 31706 If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) < 0 ↔ ((sgn‘𝐴) · (sgn‘𝐵)) < 0))
 
Theoremsgnmulsgp 31707 If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐴 · 𝐵) ↔ 0 < ((sgn‘𝐴) · (sgn‘𝐵))))
 
Theoremfzssfzo 31708 Condition for an integer interval to be a subset of a half-open integer interval. (Contributed by Thierry Arnoux, 8-Oct-2018.)
(𝐾 ∈ (𝑀..^𝑁) → (𝑀...𝐾) ⊆ (𝑀..^𝑁))
 
Theoremgsumncl 31709* Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.)
𝐾 = (Base‘𝑀)    &   (𝜑𝑀 ∈ Mnd)    &   (𝜑𝑃 ∈ (ℤ𝑁))    &   ((𝜑𝑘 ∈ (𝑁...𝑃)) → 𝐵𝐾)       (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) ∈ 𝐾)
 
Theoremgsumnunsn 31710* Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.)
𝐾 = (Base‘𝑀)    &   (𝜑𝑀 ∈ Mnd)    &   (𝜑𝑃 ∈ (ℤ𝑁))    &   ((𝜑𝑘 ∈ (𝑁...𝑃)) → 𝐵𝐾)    &    + = (+g𝑀)    &   (𝜑𝐶𝐾)    &   ((𝜑𝑘 = (𝑃 + 1)) → 𝐵 = 𝐶)       (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)) = ((𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) + 𝐶))
 
20.3.23.1  Operations on words
 
Theoremccatmulgnn0dir 31711 Concatenation of words follow the rule mulgnn0dir 18195 (although applying mulgnn0dir 18195 would require 𝑆 to be a set). In this case 𝐴 is ⟨“𝐾”⟩ to the power 𝑀 in the free monoid. (Contributed by Thierry Arnoux, 5-Oct-2018.)
𝐴 = ((0..^𝑀) × {𝐾})    &   𝐵 = ((0..^𝑁) × {𝐾})    &   𝐶 = ((0..^(𝑀 + 𝑁)) × {𝐾})    &   (𝜑𝐾𝑆)    &   (𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝐴 ++ 𝐵) = 𝐶)
 
Theoremofcccat 31712 Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 5-Oct-2018.)
(𝜑𝐹 ∈ Word 𝑆)    &   (𝜑𝐺 ∈ Word 𝑆)    &   (𝜑𝐾𝑇)       (𝜑 → ((𝐹 ++ 𝐺) ∘f/c 𝑅𝐾) = ((𝐹f/c 𝑅𝐾) ++ (𝐺f/c 𝑅𝐾)))
 
Theoremofcs1 31713 Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
((𝐴𝑆𝐵𝑇) → (⟨“𝐴”⟩ ∘f/c 𝑅𝐵) = ⟨“(𝐴𝑅𝐵)”⟩)
 
Theoremofcs2 31714 Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 9-Oct-2018.)
((𝐴𝑆𝐵𝑆𝐶𝑇) → (⟨“𝐴𝐵”⟩ ∘f/c 𝑅𝐶) = ⟨“(𝐴𝑅𝐶)(𝐵𝑅𝐶)”⟩)
 
20.3.24  Polynomials with real coefficients - misc additions
 
Theoremplymul02 31715 Product of a polynomial with the zero polynomial. (Contributed by Thierry Arnoux, 26-Sep-2018.)
(𝐹 ∈ (Poly‘𝑆) → (0𝑝f · 𝐹) = 0𝑝)
 
Theoremplymulx0 31716* Coefficients of a polynomial multiplied by Xp. (Contributed by Thierry Arnoux, 25-Sep-2018.)
(𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘(𝐹f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))
 
Theoremplymulx 31717* Coefficients of a polynomial multiplied by Xp. (Contributed by Thierry Arnoux, 25-Sep-2018.)
(𝐹 ∈ (Poly‘ℝ) → (coeff‘(𝐹f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))
 
Theoremplyrecld 31718 Closure of a polynomial with real coefficients. (Contributed by Thierry Arnoux, 18-Sep-2018.)
(𝜑𝐹 ∈ (Poly‘ℝ))    &   (𝜑𝑋 ∈ ℝ)       (𝜑 → (𝐹𝑋) ∈ ℝ)
 
Theoremsignsplypnf 31719* The quotient of a polynomial 𝐹 by a monic monomial of same degree 𝐺 converges to the highest coefficient of 𝐹. (Contributed by Thierry Arnoux, 18-Sep-2018.)
𝐷 = (deg‘𝐹)    &   𝐶 = (coeff‘𝐹)    &   𝐵 = (𝐶𝐷)    &   𝐺 = (𝑥 ∈ ℝ+ ↦ (𝑥𝐷))       (𝐹 ∈ (Poly‘ℝ) → (𝐹f / 𝐺) ⇝𝑟 𝐵)
 
Theoremsignsply0 31720* Lemma for the rule of signs, based on Bolzano's intermediate value theorem for polynomials : If the lowest and highest coefficient 𝐴 and 𝐵 are of opposite signs, the polynomial admits a positive root. (Contributed by Thierry Arnoux, 19-Sep-2018.)
𝐷 = (deg‘𝐹)    &   𝐶 = (coeff‘𝐹)    &   𝐵 = (𝐶𝐷)    &   𝐴 = (𝐶‘0)    &   (𝜑𝐹 ∈ (Poly‘ℝ))    &   (𝜑𝐹 ≠ 0𝑝)    &   (𝜑 → (𝐴 · 𝐵) < 0)       (𝜑 → ∃𝑧 ∈ ℝ+ (𝐹𝑧) = 0)
 
20.3.25  Descartes's rule of signs
 
20.3.25.1  Sign changes in a word over real numbers
 
Theoremsignspval 31721* The value of the skipping 0 sign operation. (Contributed by Thierry Arnoux, 9-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))       ((𝑋 ∈ {-1, 0, 1} ∧ 𝑌 ∈ {-1, 0, 1}) → (𝑋 𝑌) = if(𝑌 = 0, 𝑋, 𝑌))
 
Theoremsignsw0glem 31722* Neutral element property of . (Contributed by Thierry Arnoux, 9-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))       𝑢 ∈ {-1, 0, 1} ((0 𝑢) = 𝑢 ∧ (𝑢 0) = 𝑢)
 
Theoremsignswbase 31723 The base of 𝑊 is the triplet reprensenting the possible signs. (Contributed by Thierry Arnoux, 9-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}       {-1, 0, 1} = (Base‘𝑊)
 
Theoremsignswplusg 31724* The operation of 𝑊. (Contributed by Thierry Arnoux, 9-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}        = (+g𝑊)
 
Theoremsignsw0g 31725* The neutral element of 𝑊. (Contributed by Thierry Arnoux, 9-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}       0 = (0g𝑊)
 
Theoremsignswmnd 31726* 𝑊 is a monoid structure on {-1, 0, 1} which operation retains the right side, but skips zeroes. This will be used for skipping zeroes when counting sign changes. (Contributed by Thierry Arnoux, 9-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}       𝑊 ∈ Mnd
 
Theoremsignswrid 31727* The zero-skipping operation propagages nonzeros. (Contributed by Thierry Arnoux, 11-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}       (𝑋 ∈ {-1, 0, 1} → (𝑋 0) = 𝑋)
 
Theoremsignswlid 31728* The zero-skipping operation keeps nonzeros. (Contributed by Thierry Arnoux, 12-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}       (((𝑋 ∈ {-1, 0, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 ≠ 0) → (𝑋 𝑌) = 𝑌)
 
Theoremsignswn0 31729* The zero-skipping operation propagages nonzeros. (Contributed by Thierry Arnoux, 11-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}       (((𝑋 ∈ {-1, 0, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑋 ≠ 0) → (𝑋 𝑌) ≠ 0)
 
Theoremsignswch 31730* The zero-skipping operation changes value when the operands change signs. (Contributed by Thierry Arnoux, 9-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}       ((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) → ((𝑋 𝑌) ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0))
 
20.3.25.2  Counting sign changes in a word over real numbers
 
Theoremsignslema 31731 Computational part of signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018.)
(𝜑𝐸 ∈ ℕ0)    &   (𝜑𝐹 ∈ ℕ0)    &   (𝜑𝐺 ∈ ℕ0)    &   (𝜑𝐻 ∈ ℕ0)    &   (𝜑 → (𝐸 < 𝐺 ∧ ¬ 2 ∥ (𝐺𝐸)))    &   (𝜑 → ((𝐻𝐺) − (𝐹𝐸)) ∈ {0, 2})       (𝜑 → (𝐹 < 𝐻 ∧ ¬ 2 ∥ (𝐻𝐹)))
 
Theoremsignstfv 31732* Value of the zero-skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (𝐹 ∈ Word ℝ → (𝑇𝐹) = (𝑛 ∈ (0..^(♯‘𝐹)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝐹𝑖))))))
 
Theoremsignstfval 31733* Value of the zero-skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇𝐹)‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹𝑖)))))
 
Theoremsignstcl 31734* Closure of the zero skipping sign word. (Contributed by Thierry Arnoux, 9-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇𝐹)‘𝑁) ∈ {-1, 0, 1})
 
Theoremsignstf 31735* The zero skipping sign word is a word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (𝐹 ∈ Word ℝ → (𝑇𝐹) ∈ Word ℝ)
 
Theoremsignstlen 31736* Length of the zero skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (𝐹 ∈ Word ℝ → (♯‘(𝑇𝐹)) = (♯‘𝐹))
 
Theoremsignstf0 31737* Sign of a single letter word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (𝐾 ∈ ℝ → (𝑇‘⟨“𝐾”⟩) = ⟨“(sgn‘𝐾)”⟩)
 
Theoremsignstfvn 31738* Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) = (((𝑇𝐹)‘((♯‘𝐹) − 1)) (sgn‘𝐾)))
 
Theoremsignsvtn0 31739* If the last letter is nonzero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-Oct-2018.) (Proof shortened by AV, 3-Nov-2022.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   𝑁 = (♯‘𝐹)       ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
 
Theoremsignstfvp 31740* Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑁) = ((𝑇𝐹)‘𝑁))
 
Theoremsignstfvneq0 31741* In case the first letter is not zero, the zero skipping sign is never zero. (Contributed by Thierry Arnoux, 10-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇𝐹)‘𝑁) ≠ 0)
 
Theoremsignstfvcl 31742* Closure of the zero skipping sign in case the first letter is not zero. (Contributed by Thierry Arnoux, 10-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇𝐹)‘𝑁) ∈ {-1, 1})
 
Theoremsignstfvc 31743* Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 11-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       ((𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇𝐹)‘𝑁))
 
Theoremsignstres 31744* Restriction of a zero skipping sign to a subword. (Contributed by Thierry Arnoux, 11-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0...(♯‘𝐹))) → ((𝑇𝐹) ↾ (0..^𝑁)) = (𝑇‘(𝐹 ↾ (0..^𝑁))))
 
Theoremsignstfveq0a 31745* Lemma for signstfveq0 31746. (Contributed by Thierry Arnoux, 11-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   𝑁 = (♯‘𝐹)       (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈ (ℤ‘2))
 
Theoremsignstfveq0 31746* In case the last letter is zero, the zero skipping sign is the same as the previous letter. (Contributed by Thierry Arnoux, 11-Oct-2018.) (Proof shortened by AV, 4-Nov-2022.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   𝑁 = (♯‘𝐹)       (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇𝐹)‘(𝑁 − 1)) = ((𝑇𝐹)‘(𝑁 − 2)))
 
Theoremsignsvvfval 31747* The value of 𝑉, which represents the number of times the sign changes in a word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (𝐹 ∈ Word ℝ → (𝑉𝐹) = Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
 
Theoremsignsvvf 31748* 𝑉 is a function. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       𝑉:Word ℝ⟶ℕ0
 
Theoremsignsvf0 31749* There is no change of sign in the empty word. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (𝑉‘∅) = 0
 
Theoremsignsvf1 31750* In a single-letter word, which represents a constant polynomial, there is no change of sign. (Contributed by Thierry Arnoux, 8-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (𝐾 ∈ ℝ → (𝑉‘⟨“𝐾”⟩) = 0)
 
Theoremsignsvfn 31751* Number of changes in a word compared to a shorter word. (Contributed by Thierry Arnoux, 12-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = ((𝑉𝐹) + if((((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1, 0)))
 
Theoremsignsvtp 31752* Adding a letter of the same sign as the highest coefficient does not change the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   (𝜑𝐸 ∈ (Word ℝ ∖ {∅}))    &   (𝜑 → (𝐸‘0) ≠ 0)    &   (𝜑𝐹 = (𝐸 ++ ⟨“𝐴”⟩))    &   (𝜑𝐴 ∈ ℝ)    &   𝑁 = (♯‘𝐸)    &   𝐵 = ((𝑇𝐸)‘(𝑁 − 1))       ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝑉𝐹) = (𝑉𝐸))
 
Theoremsignsvtn 31753* Adding a letter of a different sign as the highest coefficient changes the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   (𝜑𝐸 ∈ (Word ℝ ∖ {∅}))    &   (𝜑 → (𝐸‘0) ≠ 0)    &   (𝜑𝐹 = (𝐸 ++ ⟨“𝐴”⟩))    &   (𝜑𝐴 ∈ ℝ)    &   𝑁 = (♯‘𝐸)    &   𝐵 = ((𝑇𝐸)‘(𝑁 − 1))       ((𝜑 ∧ (𝐴 · 𝐵) < 0) → ((𝑉𝐹) − (𝑉𝐸)) = 1)
 
Theoremsignsvfpn 31754* Adding a letter of the same sign as the highest coefficient does not change the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   (𝜑𝐸 ∈ (Word ℝ ∖ {∅}))    &   (𝜑 → (𝐸‘0) ≠ 0)    &   (𝜑𝐹 = (𝐸 ++ ⟨“𝐴”⟩))    &   (𝜑𝐴 ∈ ℝ)    &   𝑁 = (♯‘𝐸)    &   𝐵 = (𝐸‘(𝑁 − 1))       ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (𝑉𝐹) = (𝑉𝐸))
 
Theoremsignsvfnn 31755* Adding a letter of a different sign as the highest coefficient changes the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   (𝜑𝐸 ∈ (Word ℝ ∖ {∅}))    &   (𝜑 → (𝐸‘0) ≠ 0)    &   (𝜑𝐹 = (𝐸 ++ ⟨“𝐴”⟩))    &   (𝜑𝐴 ∈ ℝ)    &   𝑁 = (♯‘𝐸)    &   𝐵 = (𝐸‘(𝑁 − 1))       ((𝜑 ∧ (𝐵 · 𝐴) < 0) → ((𝑉𝐹) − (𝑉𝐸)) = 1)
 
Theoremsignlem0 31756* Adding a zero as the highest coefficient does not change the parity of the sign changes. (Contributed by Thierry Arnoux, 12-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))       ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) → (𝑉‘(𝐹 ++ ⟨“0”⟩)) = (𝑉𝐹))
 
Theoremsignshf 31757* 𝐻, corresponding to the word 𝐹 multiplied by (𝑥𝐶), as a function. (Contributed by Thierry Arnoux, 29-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   𝐻 = ((⟨“0”⟩ ++ 𝐹) ∘f − ((𝐹 ++ ⟨“0”⟩) ∘f/c · 𝐶))       ((𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+) → 𝐻:(0..^((♯‘𝐹) + 1))⟶ℝ)
 
Theoremsignshwrd 31758* 𝐻, corresponding to the word 𝐹 multiplied by (𝑥𝐶), is a word. (Contributed by Thierry Arnoux, 29-Sep-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   𝐻 = ((⟨“0”⟩ ++ 𝐹) ∘f − ((𝐹 ++ ⟨“0”⟩) ∘f/c · 𝐶))       ((𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+) → 𝐻 ∈ Word ℝ)
 
Theoremsignshlen 31759* Length of 𝐻, corresponding to the word 𝐹 multiplied by (𝑥𝐶). (Contributed by Thierry Arnoux, 14-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   𝐻 = ((⟨“0”⟩ ++ 𝐹) ∘f − ((𝐹 ++ ⟨“0”⟩) ∘f/c · 𝐶))       ((𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+) → (♯‘𝐻) = ((♯‘𝐹) + 1))
 
Theoremsignshnz 31760* 𝐻 is not the empty word. (Contributed by Thierry Arnoux, 14-Oct-2018.)
= (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))    &   𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}    &   𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))    &   𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))    &   𝐻 = ((⟨“0”⟩ ++ 𝐹) ∘f − ((𝐹 ++ ⟨“0”⟩) ∘f/c · 𝐶))       ((𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+) → 𝐻 ≠ ∅)
 
20.3.26  Number Theory
 
Theoremefcld 31761 Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (exp‘𝐴) ∈ ℂ)
 
Theoremiblidicc 31762* The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
 
Theoremrpsqrtcn 31763 Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.)
(√ ↾ ℝ+) ∈ (ℝ+cn→ℝ+)
 
Theoremdivsqrtid 31764 A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.)
(𝐴 ∈ ℝ+ → (𝐴 / (√‘𝐴)) = (√‘𝐴))
 
Theoremcxpcncf1 31765* The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn 25253. (Contributed by Thierry Arnoux, 20-Dec-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐷 ⊆ (ℂ ∖ (-∞(,]0)))       (𝜑 → (𝑥𝐷 ↦ (𝑥𝑐𝐴)) ∈ (𝐷cn→ℂ))
 
Theoremefmul2picn 31766* Multiplying by (i · (2 · π)) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.)
(𝜑 → (𝑥𝐴𝐵) ∈ (𝐴cn→ℂ))       (𝜑 → (𝑥𝐴 ↦ (exp‘((i · (2 · π)) · 𝐵))) ∈ (𝐴cn→ℂ))
 
Theoremfct2relem 31767 Lemma for ftc2re 31768. (Contributed by Thierry Arnoux, 20-Dec-2021.)
𝐸 = (𝐶(,)𝐷)    &   (𝜑𝐴𝐸)    &   (𝜑𝐵𝐸)       (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸)
 
Theoremftc2re 31768* The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.)
𝐸 = (𝐶(,)𝐷)    &   (𝜑𝐴𝐸)    &   (𝜑𝐵𝐸)    &   (𝜑𝐴𝐵)    &   (𝜑𝐹:𝐸⟶ℂ)    &   (𝜑 → (ℝ D 𝐹) ∈ (𝐸cn→ℂ))       (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹𝐵) − (𝐹𝐴)))
 
Theoremfdvposlt 31769* Functions with a positive derivative, i.e. monotonously growing functions, preserve strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
𝐸 = (𝐶(,)𝐷)    &   (𝜑𝐴𝐸)    &   (𝜑𝐵𝐸)    &   (𝜑𝐹:𝐸⟶ℝ)    &   (𝜑 → (ℝ D 𝐹) ∈ (𝐸cn→ℝ))    &   (𝜑𝐴 < 𝐵)    &   ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 < ((ℝ D 𝐹)‘𝑥))       (𝜑 → (𝐹𝐴) < (𝐹𝐵))
 
Theoremfdvneggt 31770* Functions with a negative derivative, i.e. monotonously decreasing functions, inverse strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
𝐸 = (𝐶(,)𝐷)    &   (𝜑𝐴𝐸)    &   (𝜑𝐵𝐸)    &   (𝜑𝐹:𝐸⟶ℝ)    &   (𝜑 → (ℝ D 𝐹) ∈ (𝐸cn→ℝ))    &   (𝜑𝐴 < 𝐵)    &   ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) < 0)       (𝜑 → (𝐹𝐵) < (𝐹𝐴))
 
Theoremfdvposle 31771* Functions with a nonnegative derivative, i.e. monotonously growing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
𝐸 = (𝐶(,)𝐷)    &   (𝜑𝐴𝐸)    &   (𝜑𝐵𝐸)    &   (𝜑𝐹:𝐸⟶ℝ)    &   (𝜑 → (ℝ D 𝐹) ∈ (𝐸cn→ℝ))    &   (𝜑𝐴𝐵)    &   ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ ((ℝ D 𝐹)‘𝑥))       (𝜑 → (𝐹𝐴) ≤ (𝐹𝐵))
 
Theoremfdvnegge 31772* Functions with a nonpositive derivative, i.e., decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
𝐸 = (𝐶(,)𝐷)    &   (𝜑𝐴𝐸)    &   (𝜑𝐵𝐸)    &   (𝜑𝐹:𝐸⟶ℝ)    &   (𝜑 → (ℝ D 𝐹) ∈ (𝐸cn→ℝ))    &   (𝜑𝐴𝐵)    &   ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0)       (𝜑 → (𝐹𝐵) ≤ (𝐹𝐴))
 
Theoremprodfzo03 31773* A product of three factors, indexed starting with zero. (Contributed by Thierry Arnoux, 14-Dec-2021.)
(𝑘 = 0 → 𝐷 = 𝐴)    &   (𝑘 = 1 → 𝐷 = 𝐵)    &   (𝑘 = 2 → 𝐷 = 𝐶)    &   ((𝜑𝑘 ∈ (0..^3)) → 𝐷 ∈ ℂ)       (𝜑 → ∏𝑘 ∈ (0..^3)𝐷 = (𝐴 · (𝐵 · 𝐶)))
 
Theoremactfunsnf1o 31774* The action 𝐹 of extending function from 𝐵 to 𝐶 with new values at point 𝐼 is a bijection. (Contributed by Thierry Arnoux, 9-Dec-2021.)
((𝜑𝑘𝐶) → 𝐴 ⊆ (𝐶m 𝐵))    &   (𝜑𝐶 ∈ V)    &   (𝜑𝐼𝑉)    &   (𝜑 → ¬ 𝐼𝐵)    &   𝐹 = (𝑥𝐴 ↦ (𝑥 ∪ {⟨𝐼, 𝑘⟩}))       ((𝜑𝑘𝐶) → 𝐹:𝐴1-1-onto→ran 𝐹)
 
Theoremactfunsnrndisj 31775* The action 𝐹 of extending function from 𝐵 to 𝐶 with new values at point 𝐼 yields different functions. (Contributed by Thierry Arnoux, 9-Dec-2021.)
((𝜑𝑘𝐶) → 𝐴 ⊆ (𝐶m 𝐵))    &   (𝜑𝐶 ∈ V)    &   (𝜑𝐼𝑉)    &   (𝜑 → ¬ 𝐼𝐵)    &   𝐹 = (𝑥𝐴 ↦ (𝑥 ∪ {⟨𝐼, 𝑘⟩}))       (𝜑Disj 𝑘𝐶 ran 𝐹)
 
Theoremitgexpif 31776* The basis for the circle method in the form of trigonometric sums. Proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 2-Dec-2021.)
(𝑁 ∈ ℤ → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, 1, 0))
 
Theoremfsum2dsub 31777* Lemma for breprexp 31803- Re-index a double sum, using difference of the initial indices. (Contributed by Thierry Arnoux, 7-Dec-2021.)
(𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝑖 = (𝑘𝑗) → 𝐴 = 𝐵)    &   ((𝜑𝑖 ∈ (ℤ‘-𝑗) ∧ 𝑗 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)    &   (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) → 𝐵 = 0)    &   (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0..^𝑗)) → 𝐵 = 0)       (𝜑 → Σ𝑖 ∈ (0...𝑀𝑗 ∈ (1...𝑁)𝐴 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑗 ∈ (1...𝑁)𝐵)
 
20.3.26.1  Representations of a number as sums of integers
 
Syntaxcrepr 31778 Representations of a number as a sum of nonnegative integers.
class repr
 
Definitiondf-repr 31779* The representations of a nonnegative 𝑚 as the sum of 𝑠 nonnegative integers from a set 𝑏. Cf. Definition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 1-Dec-2021.)
repr = (𝑠 ∈ ℕ0 ↦ (𝑏 ∈ 𝒫 ℕ, 𝑚 ∈ ℤ ↦ {𝑐 ∈ (𝑏m (0..^𝑠)) ∣ Σ𝑎 ∈ (0..^𝑠)(𝑐𝑎) = 𝑚}))
 
Theoremreprval 31780* Value of the representations of 𝑀 as the sum of 𝑆 nonnegative integers in a given set 𝐴 (Contributed by Thierry Arnoux, 1-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)       (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = 𝑀})
 
Theoremrepr0 31781 There is exactly one representation with no elements (an empty sum), only for 𝑀 = 0. (Contributed by Thierry Arnoux, 2-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)       (𝜑 → (𝐴(repr‘0)𝑀) = if(𝑀 = 0, {∅}, ∅))
 
Theoremreprf 31782 Members of the representation of 𝑀 as the sum of 𝑆 nonnegative integers from set 𝐴 as functions. (Contributed by Thierry Arnoux, 5-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐶 ∈ (𝐴(repr‘𝑆)𝑀))       (𝜑𝐶:(0..^𝑆)⟶𝐴)
 
Theoremreprsum 31783* Sums of values of the members of the representation of 𝑀 equal 𝑀. (Contributed by Thierry Arnoux, 5-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐶 ∈ (𝐴(repr‘𝑆)𝑀))       (𝜑 → Σ𝑎 ∈ (0..^𝑆)(𝐶𝑎) = 𝑀)
 
Theoremreprle 31784 Upper bound to the terms in the representations of 𝑀 as the sum of 𝑆 nonnegative integers from set 𝐴. (Contributed by Thierry Arnoux, 27-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐶 ∈ (𝐴(repr‘𝑆)𝑀))    &   (𝜑𝑋 ∈ (0..^𝑆))       (𝜑 → (𝐶𝑋) ≤ 𝑀)
 
Theoremreprsuc 31785* Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))       (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = 𝑏𝐴 ran 𝐹)
 
Theoremreprfi 31786 Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐴 ∈ Fin)       (𝜑 → (𝐴(repr‘𝑆)𝑀) ∈ Fin)
 
Theoremreprss 31787 Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐵𝐴)       (𝜑 → (𝐵(repr‘𝑆)𝑀) ⊆ (𝐴(repr‘𝑆)𝑀))
 
Theoremreprinrn 31788* Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)       (𝜑 → (𝑐 ∈ ((𝐴𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐𝐵)))
 
Theoremreprlt 31789 There are no representations of 𝑀 with more than 𝑀 terms. Remark of [Nathanson] p. 123 (Contributed by Thierry Arnoux, 7-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝑀 < 𝑆)       (𝜑 → (𝐴(repr‘𝑆)𝑀) = ∅)
 
Theoremhashreprin 31790* Express a sum of representations over an intersection using a product of the indicator function (Contributed by Thierry Arnoux, 11-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐵 ∈ Fin)    &   (𝜑𝐵 ⊆ ℕ)       (𝜑 → (♯‘((𝐴𝐵)(repr‘𝑆)𝑀)) = Σ𝑐 ∈ (𝐵(repr‘𝑆)𝑀)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐𝑎)))
 
Theoremreprgt 31791 There are no representations of more than (𝑆 · 𝑁) with only 𝑆 terms bounded by 𝑁. Remark of [Nathanson] p. 123 (Contributed by Thierry Arnoux, 7-Dec-2021.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐴 ⊆ (1...𝑁))    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑 → (𝑆 · 𝑁) < 𝑀)       (𝜑 → (𝐴(repr‘𝑆)𝑀) = ∅)
 
Theoremreprinfz1 31792 For the representation of 𝑁, it is sufficient to consider nonnegative integers up to 𝑁. Remark of [Nathanson] p. 123 (Contributed by Thierry Arnoux, 13-Dec-2021.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐴 ⊆ ℕ)       (𝜑 → (𝐴(repr‘𝑆)𝑁) = ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁))
 
Theoremreprfi2 31793 Corollary of reprinfz1 31792. (Contributed by Thierry Arnoux, 15-Dec-2021.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝐴 ⊆ ℕ)       (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin)
 
Theoremreprfz1 31794 Corollary of reprinfz1 31792. (Contributed by Thierry Arnoux, 14-Dec-2021.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑆 ∈ ℕ0)       (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁))
 
Theoremhashrepr 31795* Develop the number of representations of an integer 𝑀 as a sum of nonnegative integers in set 𝐴. (Contributed by Thierry Arnoux, 14-Dec-2021.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑆 ∈ ℕ0)       (𝜑 → (♯‘(𝐴(repr‘𝑆)𝑀)) = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑀)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐𝑎)))
 
Theoremreprpmtf1o 31796* Transposing 0 and 𝑋 maps representations with a condition on the first index to transpositions with the same condition on the index 𝑋. (Contributed by Thierry Arnoux, 27-Dec-2021.)
(𝜑𝑆 ∈ ℕ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝐴 ⊆ ℕ)    &   (𝜑𝑋 ∈ (0..^𝑆))    &   𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}    &   𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑋) ∈ 𝐵}    &   𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0}))    &   𝐹 = (𝑐𝑃 ↦ (𝑐𝑇))       (𝜑𝐹:𝑃1-1-onto𝑂)
 
Theoremreprdifc 31797* Express the representations as a sum of integers in a difference of sets using conditions on each of the indices. (Contributed by Thierry Arnoux, 27-Dec-2021.)
𝐶 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐𝑥) ∈ 𝐵}    &   (𝜑𝐴 ⊆ ℕ)    &   (𝜑𝐵 ⊆ ℕ)    &   (𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑆 ∈ ℕ0)       (𝜑 → ((𝐴(repr‘𝑆)𝑀) ∖ (𝐵(repr‘𝑆)𝑀)) = 𝑥 ∈ (0..^𝑆)𝐶)
 
Theoremchpvalz 31798* Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.)
(𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛))
 
Theoremchtvalz 31799* Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)
(𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
 
Theorembreprexplema 31800* Lemma for breprexp 31803 (induction step for weighted sums over representations) (Contributed by Thierry Arnoux, 7-Dec-2021.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑆 ∈ ℕ0)    &   (𝜑𝑀 ∈ ℕ0)    &   (𝜑𝑀 ≤ ((𝑆 + 1) · 𝑁))    &   (((𝜑𝑥 ∈ (0..^(𝑆 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿𝑥)‘𝑦) ∈ ℂ)       (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)))
    < Previous  Next >

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-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202 20101-20200 203 20201-20300 204 20301-20400 205 20401-20500 206 20501-20600 207 20601-20700 208 20701-20800 209 20801-20900 210 20901-21000 211 21001-21100 212 21101-21200 213 21201-21300 214 21301-21400 215 21401-21500 216 21501-21600 217 21601-21700 218 21701-21800 219 21801-21900 220 21901-22000 221 22001-22100 222 22101-22200 223 22201-22300 224 22301-22400 225 22401-22500 226 22501-22600 227 22601-22700 228 22701-22800 229 22801-22900 230 22901-23000 231 23001-23100 232 23101-23200 233 23201-23300 234 23301-23400 235 23401-23500 236 23501-23600 237 23601-23700 238 23701-23800 239 23801-23900 240 23901-24000 241 24001-24100 242 24101-24200 243 24201-24300 244 24301-24400 245 24401-24500 246 24501-24600 247 24601-24700 248 24701-24800 249 24801-24900 250 24901-25000 251 25001-25100 252 25101-25200 253 25201-25300 254 25301-25400 255 25401-25500 256 25501-25600 257 25601-25700 258 25701-25800 259 25801-25900 260 25901-26000 261 26001-26100 262 26101-26200 263 26201-26300 264 26301-26400 265 26401-26500 266 26501-26600 267 26601-26700 268 26701-26800 269 26801-26900 270 26901-27000 271 27001-27100 272 27101-27200 273 27201-27300 274 27301-27400 275 27401-27500 276 27501-27600 277 27601-27700 278 27701-27800 279 27801-27900 280 27901-28000 281 28001-28100 282 28101-28200 283 28201-28300 284 28301-28400 285 28401-28500 286 28501-28600 287 28601-28700 288 28701-28800 289 28801-28900 290 28901-29000 291 29001-29100 292 29101-29200 293 29201-29300 294 29301-29400 295 29401-29500 296 29501-29600 297 29601-29700 298 29701-29800 299 29801-29900 300 29901-30000 301 30001-30100 302 30101-30200 303 30201-30300 304 30301-30400 305 30401-30500 306 30501-30600 307 30601-30700 308 30701-30800 309 30801-30900 310 30901-31000 311 31001-31100 312 31101-31200 313 31201-31300 314 31301-31400 315 31401-31500 316 31501-31600 317 31601-31700 318 31701-31800 319 31801-31900 320 31901-32000 321 32001-32100 322 32101-32200 323 32201-32300 324 32301-32400 325 32401-32500 326 32501-32600 327 32601-32700 328 32701-32800 329 32801-32900 330 32901-33000 331 33001-33100 332 33101-33200 333 33201-33300 334 33301-33400 335 33401-33500 336 33501-33600 337 33601-33700 338 33701-33800 339 33801-33900 340 33901-34000 341 34001-34100 342 34101-34200 343 34201-34300 344 34301-34400 345 34401-34500 346 34501-34600 347 34601-34700 348 34701-34800 349 34801-34900 350 34901-35000 351 35001-35100 352 35101-35200 353 35201-35300 354 35301-35400 355 35401-35500 356 35501-35600 357 35601-35700 358 35701-35800 359 35801-35900 360 35901-36000 361 36001-36100 362 36101-36200 363 36201-36300 364 36301-36400 365 36401-36500 366 36501-36600 367 36601-36700 368 36701-36800 369 36801-36900 370 36901-37000 371 37001-37100 372 37101-37200 373 37201-37300 374 37301-37400 375 37401-37500 376 37501-37600 377 37601-37700 378 37701-37800 379 37801-37900 380 37901-38000 381 38001-38100 382 38101-38200 383 38201-38300 384 38301-38400 385 38401-38500 386 38501-38600 387 38601-38700 388 38701-38800 389 38801-38900 390 38901-39000 391 39001-39100 392 39101-39200 393 39201-39300 394 39301-39400 395 39401-39500 396 39501-39600 397 39601-39700 398 39701-39800 399 39801-39900 400 39901-40000 401 40001-40100 402 40101-40200 403 40201-40300 404 40301-40400 405 40401-40500 406 40501-40600 407 40601-40700 408 40701-40800 409 40801-40900 410 40901-41000 411 41001-41100 412 41101-41200 413 41201-41300 414 41301-41400 415 41401-41500 416 41501-41600 417 41601-41700 418 41701-41800 419 41801-41900 420 41901-42000 421 42001-42100 422 42101-42200 423 42201-42300 424 42301-42400 425 42401-42500 426 42501-42600 427 42601-42700 428 42701-42800 429 42801-42900 430 42901-43000 431 43001-43100 432 43101-43200 433 43201-43300 434 43301-43400 435 43401-43500 436 43501-43600 437 43601-43700 438 43701-43800 439 43801-43900 440 43901-44000 441 44001-44100 442 44101-44200 443 44201-44300 444 44301-44400 445 44401-44500 446 44501-44600 447 44601-44700 448 44701-44800 449 44801-44834
  Copyright terms: Public domain < Previous  Next >