P. 350 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34901-35000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ballotlemrinv0 34901*	Lemma for ballotlemrinv 34902. (Contributed by Thierry Arnoux, 18-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐷 = ((𝑆‘𝐶) “ 𝐶)) → (𝐷 ∈ (𝑂 ∖ 𝐸) ∧ 𝐶 = ((𝑆‘𝐷) “ 𝐷)))
Theorem	ballotlemrinv 34902*	𝑅 is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ ◡𝑅 = 𝑅
Theorem	ballotlem1ri 34903*	When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1 ∈ (𝑅‘𝐶) ↔ (𝐼‘𝐶) ∈ 𝐶))
Theorem	ballotlem7 34904*	𝑅 is a bijection between two subsets of (𝑂 ∖ 𝐸): one where a vote for A is picked first, and one where a vote for B is picked first. (Contributed by Thierry Arnoux, 12-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝑅 ↾ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}):{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}–1-1-onto→{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}
Theorem	ballotlem8 34905*	There are as many countings with ties starting with a ballot for 𝐴 as there are starting with a ballot for 𝐵. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) = (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})
Theorem	ballotth 34906*	Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    ⇒   ⊢ (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁))
21.3.24  Signum (sgn or sign) function - misc. additions
Theorem	fzssfzo 34907	Condition for an integer interval to be a subset of a half-open integer interval. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑀...𝐾) ⊆ (𝑀..^𝑁))
Theorem	gsumncl 34908*	Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ 𝐾 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑁...𝑃)) → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) ∈ 𝐾)
Theorem	gsumnunsn 34909*	Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ 𝐾 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑁...𝑃)) → 𝐵 ∈ 𝐾)    &   ⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑘 = (𝑃 + 1)) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ (𝑁...(𝑃 + 1)) ↦ 𝐵)) = ((𝑀 Σg (𝑘 ∈ (𝑁...𝑃) ↦ 𝐵)) + 𝐶))
21.3.24.1  Operations on words
Theorem	ccatmulgnn0dir 34910	Concatenation of words follow the rule mulgnn0dir 19171 (although applying mulgnn0dir 19171 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 34911	Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 5-Oct-2018.)
⊢ (𝜑 → 𝐹 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑇)    ⇒   ⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘f/c 𝑅𝐾) = ((𝐹 ∘f/c 𝑅𝐾) ++ (𝐺 ∘f/c 𝑅𝐾)))
Theorem	ofcs1 34912	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (⟨“𝐴”⟩ ∘f/c 𝑅𝐵) = ⟨“(𝐴𝑅𝐵)”⟩)
Theorem	ofcs2 34913	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	plyrecld 34914	Closure of a polynomial with real coefficients. (Contributed by Thierry Arnoux, 18-Sep-2018.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘ℝ))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ∈ ℝ)
Theorem	signsplypnf 34915*	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 34916*	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 34917*	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 34918*	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 34919	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 34920*	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 34921*	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 34922*	𝑊 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 34923*	The zero-skipping operation propagates 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 34924*	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 34925*	The zero-skipping operation propagates 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 34926*	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 34927	Computational part of ~? signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018.)
⊢ (𝜑 → 𝐸 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐸 < 𝐺 ∧ ¬ 2 ∥ (𝐺 − 𝐸)))    &   ⊢ (𝜑 → ((𝐻 − 𝐺) − (𝐹 − 𝐸)) ∈ {0, 2})    ⇒   ⊢ (𝜑 → (𝐹 < 𝐻 ∧ ¬ 2 ∥ (𝐻 − 𝐹)))
Theorem	signstfv 34928*	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 34929*	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 34930*	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 34931*	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 34932*	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 34933*	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 34934*	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 34935*	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 34936*	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 34937*	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 34938*	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 34939*	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 34940*	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 34941*	Lemma for signstfveq0 34942. (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 34942*	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 34943*	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 34944*	𝑉 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 34945*	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 34946*	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 34947*	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 34948*	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 34949*	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 34950*	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 34951*	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 34952*	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 34953*	𝐻, 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 34954*	𝐻, 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 34955*	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 34956*	𝐻 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 34957*	The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
Theorem	rpsqrtcn 34958	Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (√ ↾ ℝ+) ∈ (ℝ+–cn→ℝ+)
Theorem	divsqrtid 34959	A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / (√‘𝐴)) = (√‘𝐴))
Theorem	cxpcncf1 34960*	The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn 26888. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ (ℂ ∖ (-∞(,]0)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴)) ∈ (𝐷–cn→ℂ))
Theorem	efmul2picn 34961*	Multiplying by (i · (2 · π)) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (exp‘((i · (2 · π)) · 𝐵))) ∈ (𝐴–cn→ℂ))
Theorem	fct2relem 34962	Lemma for ftc2re 34963. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸)
Theorem	ftc2re 34963*	The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℂ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	fdvposlt 34964*	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 34965*	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 34966*	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 34967*	Functions with a nonpositive derivative, i.e., decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℝ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ))    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴))
Theorem	prodfzo03 34968*	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 34969*	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 34970*	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 34971*	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 34972*	Lemma for breprexp 34998- 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 34973	Representations of a number as a sum of nonnegative integers.
class repr
Definition	df-repr 34974*	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 34975*	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 34976	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 34977	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 34978*	Sums of values of the members of the representation of 𝑀 equal 𝑀. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(repr‘𝑆)𝑀))    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)(𝐶‘𝑎) = 𝑀)
Theorem	reprle 34979	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 34980*	Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))    ⇒   ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
Theorem	reprfi 34981	Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) ∈ Fin)
Theorem	reprss 34982	Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐵(repr‘𝑆)𝑀) ⊆ (𝐴(repr‘𝑆)𝑀))
Theorem	reprinrn 34983*	Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐 ⊆ 𝐵)))
Theorem	reprlt 34984	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 34985*	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 34986	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 34987	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 34988	Corollary of reprinfz1 34987. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin)
Theorem	reprfz1 34989	Corollary of reprinfz1 34987. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁))
Theorem	hashrepr 34990*	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 34991*	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 34992*	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 34993*	Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛))
Theorem	chtvalz 34994*	Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
Theorem	breprexplema 34995*	Lemma for breprexp 34998 (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 34996	Lemma for breprexp 34998 (closure). (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    &   ⊢ (𝜑 → 𝑋 ∈ (0..^𝑆))    &   ⊢ (𝜑 → 𝑌 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐿‘𝑋)‘𝑌) ∈ ℂ)
Theorem	breprexplemc 34997*	Lemma for breprexp 34998 (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 34998*	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 34999 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 34999*	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 35000	The Vinogradov trigonometric sums.
class vts