Home | 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
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sgnmulrp2 31701 | Multiplication by a positive number does not affect signum. (Contributed by Thierry Arnoux, 2-Oct-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (sgn‘(𝐴 · 𝐵)) = (sgn‘𝐴)) | ||
Theorem | sgnsub 31702 | Subtraction of a number of opposite sign. (Contributed by Thierry Arnoux, 2-Oct-2018.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → (sgn‘(𝐴 − 𝐵)) = (sgn‘𝐴)) | ||
Theorem | sgnnbi 31703 | Negative signum. (Contributed by Thierry Arnoux, 2-Oct-2018.) |
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = -1 ↔ 𝐴 < 0)) | ||
Theorem | sgnpbi 31704 | Positive signum. (Contributed by Thierry Arnoux, 2-Oct-2018.) |
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = 1 ↔ 0 < 𝐴)) | ||
Theorem | sgn0bi 31705 | Zero signum. (Contributed by Thierry Arnoux, 10-Oct-2018.) |
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | sgnsgn 31706 | Signum is idempotent. (Contributed by Thierry Arnoux, 2-Oct-2018.) |
⊢ (𝐴 ∈ ℝ* → (sgn‘(sgn‘𝐴)) = (sgn‘𝐴)) | ||
Theorem | sgnmulsgn 31707 | If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) < 0 ↔ ((sgn‘𝐴) · (sgn‘𝐵)) < 0)) | ||
Theorem | sgnmulsgp 31708 | If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐴 · 𝐵) ↔ 0 < ((sgn‘𝐴) · (sgn‘𝐵)))) | ||
Theorem | fzssfzo 31709 | Condition for an integer interval to be a subset of a half-open integer interval. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑀...𝐾) ⊆ (𝑀..^𝑁)) | ||
Theorem | gsumncl 31710* | Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
⊢ 𝐾 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑁...𝑃)) → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) ∈ 𝐾) | ||
Theorem | gsumnunsn 31711* | Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
⊢ 𝐾 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑁)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑁...𝑃)) → 𝐵 ∈ 𝐾) & ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑘 = (𝑃 + 1)) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)) = ((𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) + 𝐶)) | ||
Theorem | ccatmulgnn0dir 31712 | Concatenation of words follow the rule mulgnn0dir 18197 (although applying mulgnn0dir 18197 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) ⇒ ⊢ (𝜑 → (𝐴 ++ 𝐵) = 𝐶) | ||
Theorem | ofcccat 31713 | Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 5-Oct-2018.) |
⊢ (𝜑 → 𝐹 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐾 ∈ 𝑇) ⇒ ⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘f/c 𝑅𝐾) = ((𝐹 ∘f/c 𝑅𝐾) ++ (𝐺 ∘f/c 𝑅𝐾))) | ||
Theorem | ofcs1 31714 | Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (〈“𝐴”〉 ∘f/c 𝑅𝐵) = 〈“(𝐴𝑅𝐵)”〉) | ||
Theorem | ofcs2 31715 | Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 9-Oct-2018.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (〈“𝐴𝐵”〉 ∘f/c 𝑅𝐶) = 〈“(𝐴𝑅𝐶)(𝐵𝑅𝐶)”〉) | ||
Theorem | plymul02 31716 | Product of a polynomial with the zero polynomial. (Contributed by Thierry Arnoux, 26-Sep-2018.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → (0𝑝 ∘f · 𝐹) = 0𝑝) | ||
Theorem | plymulx0 31717* | 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))))) | ||
Theorem | plymulx 31718* | Coefficients of a polynomial multiplied by Xp. (Contributed by Thierry Arnoux, 25-Sep-2018.) |
⊢ (𝐹 ∈ (Poly‘ℝ) → (coeff‘(𝐹 ∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) | ||
Theorem | plyrecld 31719 | Closure of a polynomial with real coefficients. (Contributed by Thierry Arnoux, 18-Sep-2018.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘ℝ)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ∈ ℝ) | ||
Theorem | signsplypnf 31720* | 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 / 𝐺) ⇝𝑟 𝐵) | ||
Theorem | signsply0 31721* | 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) | ||
Theorem | signspval 31722* | 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, 𝑋, 𝑌)) | ||
Theorem | signsw0glem 31723* | Neutral element property of ⨣. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏)) ⇒ ⊢ ∀𝑢 ∈ {-1, 0, 1} ((0 ⨣ 𝑢) = 𝑢 ∧ (𝑢 ⨣ 0) = 𝑢) | ||
Theorem | signswbase 31724 | 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‘𝑊) | ||
Theorem | signswplusg 31725* | 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‘𝑊) | ||
Theorem | signsw0g 31726* | 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‘𝑊) | ||
Theorem | signswmnd 31727* | 𝑊 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 | ||
Theorem | signswrid 31728* | 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) = 𝑋) | ||
Theorem | signswlid 31729* | 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) → (𝑋 ⨣ 𝑌) = 𝑌) | ||
Theorem | signswn0 31730* | 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) | ||
Theorem | signswch 31731* | 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)) | ||
Theorem | signslema 31732 | Computational part of signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018.) |
⊢ (𝜑 → 𝐸 ∈ ℕ0) & ⊢ (𝜑 → 𝐹 ∈ ℕ0) & ⊢ (𝜑 → 𝐺 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ ℕ0) & ⊢ (𝜑 → (𝐸 < 𝐺 ∧ ¬ 2 ∥ (𝐺 − 𝐸))) & ⊢ (𝜑 → ((𝐻 − 𝐺) − (𝐹 − 𝐸)) ∈ {0, 2}) ⇒ ⊢ (𝜑 → (𝐹 < 𝐻 ∧ ¬ 2 ∥ (𝐻 − 𝐹))) | ||
Theorem | signstfv 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‘(𝐹‘𝑖)))))) | ||
Theorem | signstfval 31734* | 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‘(𝐹‘𝑖))))) | ||
Theorem | signstcl 31735* | 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}) | ||
Theorem | signstf 31736* | 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 ℝ) | ||
Theorem | signstlen 31737* | 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 ℝ → (♯‘(𝑇‘𝐹)) = (♯‘𝐹)) | ||
Theorem | signstf0 31738* | 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‘𝐾)”〉) | ||
Theorem | signstfvn 31739* | 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‘𝐾))) | ||
Theorem | signsvtn0 31740* | 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)))) | ||
Theorem | signstfvp 31741* | 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..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) | ||
Theorem | signstfvneq0 31742* | 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) | ||
Theorem | signstfvcl 31743* | 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}) | ||
Theorem | signstfvc 31744* | 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..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) | ||
Theorem | signstres 31745* | 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..^𝑁)))) | ||
Theorem | signstfveq0a 31746* | Lemma for signstfveq0 31747. (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)) | ||
Theorem | signstfveq0 31747* | 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))) | ||
Theorem | signsvvfval 31748* | 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)) | ||
Theorem | signsvvf 31749* | 𝑉 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 | ||
Theorem | signsvf0 31750* | 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 | ||
Theorem | signsvf1 31751* | 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) | ||
Theorem | signsvfn 31752* | 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))) | ||
Theorem | signsvtp 31753* | 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 < (𝐴 · 𝐵)) → (𝑉‘𝐹) = (𝑉‘𝐸)) | ||
Theorem | signsvtn 31754* | 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) | ||
Theorem | signsvfpn 31755* | 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 < (𝐵 · 𝐴)) → (𝑉‘𝐹) = (𝑉‘𝐸)) | ||
Theorem | signsvfnn 31756* | 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) | ||
Theorem | signlem0 31757* | 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”〉)) = (𝑉‘𝐹)) | ||
Theorem | signshf 31758* | 𝐻, 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))⟶ℝ) | ||
Theorem | signshwrd 31759* | 𝐻, 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 ℝ) | ||
Theorem | signshlen 31760* | 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)) | ||
Theorem | signshnz 31761* | 𝐻 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 ℝ ∧ 𝐶 ∈ ℝ+) → 𝐻 ≠ ∅) | ||
Theorem | efcld 31762 | Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℂ) | ||
Theorem | iblidicc 31763* | The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1) | ||
Theorem | rpsqrtcn 31764 | Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
⊢ (√ ↾ ℝ+) ∈ (ℝ+–cn→ℝ+) | ||
Theorem | divsqrtid 31765 | A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 / (√‘𝐴)) = (√‘𝐴)) | ||
Theorem | cxpcncf1 31766* | 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→ℂ)) | ||
Theorem | efmul2picn 31767* | Multiplying by (i · (2 · π)) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (exp‘((i · (2 · π)) · 𝐵))) ∈ (𝐴–cn→ℂ)) | ||
Theorem | fct2relem 31768 | Lemma for ftc2re 31769. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸) | ||
Theorem | ftc2re 31769* | The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹:𝐸⟶ℂ) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
Theorem | fdvposlt 31770* | Functions with a positive derivative, i.e. monotonously growing functions, preserve strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐹:𝐸⟶ℝ) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ)) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < ((ℝ D 𝐹)‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) < (𝐹‘𝐵)) | ||
Theorem | fdvneggt 31771* | Functions with a negative derivative, i.e. monotonously decreasing functions, inverse strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐹:𝐸⟶ℝ) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ)) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) < 0) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) < (𝐹‘𝐴)) | ||
Theorem | fdvposle 31772* | Functions with a nonnegative derivative, i.e. monotonously growing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐹:𝐸⟶ℝ) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ)) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ ((ℝ D 𝐹)‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐹‘𝐵)) | ||
Theorem | fdvnegge 31773* | Functions with a nonpositive derivative, i.e., decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐹:𝐸⟶ℝ) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ)) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴)) | ||
Theorem | prodfzo03 31774* | A product of three factors, indexed starting with zero. (Contributed by Thierry Arnoux, 14-Dec-2021.) |
⊢ (𝑘 = 0 → 𝐷 = 𝐴) & ⊢ (𝑘 = 1 → 𝐷 = 𝐵) & ⊢ (𝑘 = 2 → 𝐷 = 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^3)) → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ (0..^3)𝐷 = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | actfunsnf1o 31775* | 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 𝐹) | ||
Theorem | actfunsnrndisj 31776* | 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 𝐹) | ||
Theorem | itgexpif 31777* | 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)) | ||
Theorem | fsum2dsub 31778* | Lemma for breprexp 31804- 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...𝑁)𝐵) | ||
Syntax | crepr 31779 | Representations of a number as a sum of nonnegative integers. |
class repr | ||
Definition | df-repr 31780* | 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..^𝑠)(𝑐‘𝑎) = 𝑚})) | ||
Theorem | reprval 31781* | 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..^𝑆)(𝑐‘𝑎) = 𝑀}) | ||
Theorem | repr0 31782 | 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, {∅}, ∅)) | ||
Theorem | reprf 31783 | 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..^𝑆)⟶𝐴) | ||
Theorem | reprsum 31784* | Sums of values of the members of the representation of 𝑀 equal 𝑀. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(repr‘𝑆)𝑀)) ⇒ ⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)(𝐶‘𝑎) = 𝑀) | ||
Theorem | reprle 31785 | 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..^𝑆)) ⇒ ⊢ (𝜑 → (𝐶‘𝑋) ≤ 𝑀) | ||
Theorem | reprsuc 31786* | Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {〈𝑆, 𝑏〉})) ⇒ ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹) | ||
Theorem | reprfi 31787 | Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) ∈ Fin) | ||
Theorem | reprss 31788 | Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐵(repr‘𝑆)𝑀) ⊆ (𝐴(repr‘𝑆)𝑀)) | ||
Theorem | reprinrn 31789* | Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐 ⊆ 𝐵))) | ||
Theorem | reprlt 31790 | There are no representations of 𝑀 with more than 𝑀 terms. Remark of [Nathanson] p. 123 (Contributed by Thierry Arnoux, 7-Dec-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 < 𝑆) ⇒ ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = ∅) | ||
Theorem | hashreprin 31791* | 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..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) | ||
Theorem | reprgt 31792 | 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‘𝑆)𝑀) = ∅) | ||
Theorem | reprinfz1 31793 | 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‘𝑆)𝑁)) | ||
Theorem | reprfi2 31794 | Corollary of reprinfz1 31793. (Contributed by Thierry Arnoux, 15-Dec-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) ⇒ ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin) | ||
Theorem | reprfz1 31795 | Corollary of reprinfz1 31793. (Contributed by Thierry Arnoux, 14-Dec-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) ⇒ ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁)) | ||
Theorem | hashrepr 31796* | 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..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) | ||
Theorem | reprpmtf1o 31797* | 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→𝑂) | ||
Theorem | reprdifc 31798* | 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..^𝑆)𝐶) | ||
Theorem | chpvalz 31799* | Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛)) | ||
Theorem | chtvalz 31800* | Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |