P. 348 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34701-34800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ofcs1 34701	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (⟨“𝐴”⟩ ∘f/c 𝑅𝐵) = ⟨“(𝐴𝑅𝐵)”⟩)
Theorem	ofcs2 34702	Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 9-Oct-2018.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (⟨“𝐴𝐵”⟩ ∘f/c 𝑅𝐶) = ⟨“(𝐴𝑅𝐶)(𝐵𝑅𝐶)”⟩)
21.3.25  Polynomials with real coefficients - misc additions
Theorem	plymul02 34703	Product of a polynomial with the zero polynomial. (Contributed by Thierry Arnoux, 26-Sep-2018.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (0𝑝 ∘f · 𝐹) = 0𝑝)
Theorem	plymulx0 34704*	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 34705*	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 34706	Closure of a polynomial with real coefficients. (Contributed by Thierry Arnoux, 18-Sep-2018.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘ℝ))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ∈ ℝ)
Theorem	signsplypnf 34707*	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 34708*	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)
21.3.26  Descartes's rule of signs
21.3.26.1  Sign changes in a word over real numbers
Theorem	signspval 34709*	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 34710*	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 34711	The base of 𝑊 is the unordered triple 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 34712*	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 34713*	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 34714*	𝑊 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 34715*	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 34716*	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 34717*	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 34718*	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))
21.3.26.2  Counting sign changes in a word over real numbers
Theorem	signslema 34719	Computational part of ~? signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018.)
⊢ (𝜑 → 𝐸 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐸 < 𝐺 ∧ ¬ 2 ∥ (𝐺 − 𝐸)))    &   ⊢ (𝜑 → ((𝐻 − 𝐺) − (𝐹 − 𝐸)) ∈ {0, 2})    ⇒   ⊢ (𝜑 → (𝐹 < 𝐻 ∧ ¬ 2 ∥ (𝐻 − 𝐹)))
Theorem	signstfv 34720*	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 34721*	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 34722*	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 34723*	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 34724*	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 34725*	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 34726*	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 34727*	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 34728*	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 34729*	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 34730*	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 34731*	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 34732*	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 34733*	Lemma for signstfveq0 34734. (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 34734*	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 34735*	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 34736*	𝑉 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 34737*	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 34738*	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 34739*	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 34740*	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 34741*	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 34742*	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 34743*	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 34744*	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 34745*	𝐻, 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 34746*	𝐻, 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 34747*	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 34748*	𝐻 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 ℝ ∧ 𝐶 ∈ ℝ+) → 𝐻 ≠ ∅)
21.3.27  Number Theory
Theorem	iblidicc 34749*	The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
Theorem	rpsqrtcn 34750	Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (√ ↾ ℝ+) ∈ (ℝ+–cn→ℝ+)
Theorem	divsqrtid 34751	A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / (√‘𝐴)) = (√‘𝐴))
Theorem	cxpcncf1 34752*	The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn 26710. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ (ℂ ∖ (-∞(,]0)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴)) ∈ (𝐷–cn→ℂ))
Theorem	efmul2picn 34753*	Multiplying by (i · (2 · π)) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (exp‘((i · (2 · π)) · 𝐵))) ∈ (𝐴–cn→ℂ))
Theorem	fct2relem 34754	Lemma for ftc2re 34755. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸)
Theorem	ftc2re 34755*	The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℂ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	fdvposlt 34756*	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 34757*	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 34758*	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 34759*	Functions with a nonpositive derivative, i.e., decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℝ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ))    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴))
Theorem	prodfzo03 34760*	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 34761*	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 34762*	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 34763*	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 34764*	Lemma for breprexp 34790- 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...𝑁)𝐵)
21.3.27.1  Representations of a number as sums of integers
Syntax	crepr 34765	Representations of a number as a sum of nonnegative integers.
class repr
Definition	df-repr 34766*	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 34767*	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 34768	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 34769	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 34770*	Sums of values of the members of the representation of 𝑀 equal 𝑀. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(repr‘𝑆)𝑀))    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)(𝐶‘𝑎) = 𝑀)
Theorem	reprle 34771	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 34772*	Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))    ⇒   ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
Theorem	reprfi 34773	Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) ∈ Fin)
Theorem	reprss 34774	Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐵(repr‘𝑆)𝑀) ⊆ (𝐴(repr‘𝑆)𝑀))
Theorem	reprinrn 34775*	Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐 ⊆ 𝐵)))
Theorem	reprlt 34776	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 34777*	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 34778	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 34779	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 34780	Corollary of reprinfz1 34779. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin)
Theorem	reprfz1 34781	Corollary of reprinfz1 34779. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁))
Theorem	hashrepr 34782*	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 34783*	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 34784*	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 34785*	Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛))
Theorem	chtvalz 34786*	Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
Theorem	breprexplema 34787*	Lemma for breprexp 34790 (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..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
Theorem	breprexplemb 34788	Lemma for breprexp 34790 (closure). (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    &   ⊢ (𝜑 → 𝑋 ∈ (0..^𝑆))    &   ⊢ (𝜑 → 𝑌 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐿‘𝑋)‘𝑌) ∈ ℂ)
Theorem	breprexplemc 34789*	Lemma for breprexp 34790 (induction step). (Contributed by Thierry Arnoux, 6-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    &   ⊢ (𝜑 → 𝑇 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑇 + 1) ≤ 𝑆)    &   ⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))    ⇒   ⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
Theorem	breprexp 34790*	Express the 𝑆 th power of the finite series in terms of the number of representations of integers 𝑚 as sums of 𝑆 terms. This is a general formulation which allows logarithmic weighting of the sums (see https://mathoverflow.net/questions/253246) and a mix of different smoothing functions taken into account in 𝐿. See breprexpnat 34791 for the simple case presented in the proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 6-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    ⇒   ⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))
Theorem	breprexpnat 34791*	Express the 𝑆 th power of the finite series in terms of the number of representations of integers 𝑚 as sums of 𝑆 terms of elements of 𝐴, bounded by 𝑁. Proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ 𝑃 = Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)    &   ⊢ 𝑅 = (♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚))    ⇒   ⊢ (𝜑 → (𝑃↑𝑆) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))(𝑅 · (𝑍↑𝑚)))
21.3.27.2  Vinogradov Trigonometric Sums and the Circle Method
Syntax	cvts 34792	The Vinogradov trigonometric sums.
class vts
Definition	df-vts 34793*	Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
Theorem	vtsval 34794*	Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) = Σ𝑎 ∈ (1...𝑁)((𝐿‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑋)))))
Theorem	vtscl 34795	Closure of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) ∈ ℂ)
Theorem	vtsprod 34796*	Express the Vinogradov trigonometric sums to the power of 𝑆 (Contributed by Thierry Arnoux, 12-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    ⇒   ⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑋) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2 · π)) · (𝑚 · 𝑋)))))
Theorem	circlemeth 34797*	The Hardy, Littlewood and Ramanujan Circle Method, in a generic form, with different weighting / smoothing functions. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    ⇒   ⊢ (𝜑 → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
Theorem	circlemethnat 34798*	The Hardy, Littlewood and Ramanujan Circle Method, Chapter 5.1 of [Nathanson] p. 123. This expresses 𝑅, the number of different ways a nonnegative integer 𝑁 can be represented as the sum of at most 𝑆 integers in the set 𝐴 as an integral of Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ 𝑅 = (♯‘(𝐴(repr‘𝑆)𝑁))    &   ⊢ 𝐹 = ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝐴 ⊆ ℕ    &   ⊢ 𝑆 ∈ ℕ    ⇒   ⊢ 𝑅 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥
Theorem	circlevma 34799*	The Circle Method, where the Vinogradov sums are weighted using the von Mangoldt function, as it appears as proposition 1.1 of [Helfgott] p. 5. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) = ∫(0(,)1)((((Λvts𝑁)‘𝑥)↑3) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
Theorem	circlemethhgt 34800*	The circle method, where the Vinogradov sums are weighted using the Von Mangoldt function and smoothed using functions 𝐻 and 𝐾. Statement 7.49 of [Helfgott] p. 69. At this point there is no further constraint on the smoothing functions. (Contributed by Thierry Arnoux, 22-Dec-2021.)
⊢ (𝜑 → 𝐻:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐾:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)