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	signstfv 34701*	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 34702*	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 34703*	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 34704*	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 34705*	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 34706*	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 34707*	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 34708*	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 34709*	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 34710*	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 34711*	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 34712*	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 34713*	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 34714*	Lemma for signstfveq0 34715. (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 34715*	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 34716*	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 34717*	𝑉 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 34718*	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 34719*	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 34720*	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 34721*	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 34722*	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 34723*	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 34724*	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 34725*	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 34726*	𝐻, 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 34727*	𝐻, 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 34728*	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 34729*	𝐻 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 34730*	The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
Theorem	rpsqrtcn 34731	Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (√ ↾ ℝ+) ∈ (ℝ+–cn→ℝ+)
Theorem	divsqrtid 34732	A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / (√‘𝐴)) = (√‘𝐴))
Theorem	cxpcncf1 34733*	The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn 26714. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ (ℂ ∖ (-∞(,]0)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴)) ∈ (𝐷–cn→ℂ))
Theorem	efmul2picn 34734*	Multiplying by (i · (2 · π)) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (exp‘((i · (2 · π)) · 𝐵))) ∈ (𝐴–cn→ℂ))
Theorem	fct2relem 34735	Lemma for ftc2re 34736. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸)
Theorem	ftc2re 34736*	The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℂ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	fdvposlt 34737*	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 34738*	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 34739*	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 34740*	Functions with a nonpositive derivative, i.e., decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℝ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ))    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴))
Theorem	prodfzo03 34741*	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 34742*	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 34743*	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 34744*	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 34745*	Lemma for breprexp 34771- 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 34746	Representations of a number as a sum of nonnegative integers.
class repr
Definition	df-repr 34747*	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 34748*	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 34749	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 34750	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 34751*	Sums of values of the members of the representation of 𝑀 equal 𝑀. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(repr‘𝑆)𝑀))    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)(𝐶‘𝑎) = 𝑀)
Theorem	reprle 34752	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 34753*	Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))    ⇒   ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
Theorem	reprfi 34754	Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) ∈ Fin)
Theorem	reprss 34755	Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐵(repr‘𝑆)𝑀) ⊆ (𝐴(repr‘𝑆)𝑀))
Theorem	reprinrn 34756*	Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐 ⊆ 𝐵)))
Theorem	reprlt 34757	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 34758*	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 34759	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 34760	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 34761	Corollary of reprinfz1 34760. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin)
Theorem	reprfz1 34762	Corollary of reprinfz1 34760. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁))
Theorem	hashrepr 34763*	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 34764*	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 34765*	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 34766*	Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛))
Theorem	chtvalz 34767*	Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
Theorem	breprexplema 34768*	Lemma for breprexp 34771 (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 34769	Lemma for breprexp 34771 (closure). (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    &   ⊢ (𝜑 → 𝑋 ∈ (0..^𝑆))    &   ⊢ (𝜑 → 𝑌 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐿‘𝑋)‘𝑌) ∈ ℂ)
Theorem	breprexplemc 34770*	Lemma for breprexp 34771 (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 34771*	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 34772 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 34772*	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 34773	The Vinogradov trigonometric sums.
class vts
Definition	df-vts 34774*	Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
Theorem	vtsval 34775*	Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) = Σ𝑎 ∈ (1...𝑁)((𝐿‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑋)))))
Theorem	vtscl 34776	Closure of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) ∈ ℂ)
Theorem	vtsprod 34777*	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 34778*	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 34779*	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 34780*	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 34781*	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𝑥)
21.3.27.3  The Ternary Goldbach Conjecture: Final Statement
Axiom	ax-hgt749 34782*	Statement 7.49 of [Helfgott] p. 70. For a sufficiently big odd 𝑁, this postulates the existence of smoothing functions ℎ (eta star) and 𝑘 (eta plus) such that the lower bound for the circle integral is big enough. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ ∀𝑛 ∈ {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} ((;10↑;27) ≤ 𝑛 → ∃ℎ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑛↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑛)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑛)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑛 · 𝑥)))) d𝑥))
Axiom	ax-ros335 34783	Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 27452 states that the ψ function is bounded by a linear term; this axiom postulates an upper bound for that linear term. This is stated as an axiom until a formal proof can be provided. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) < ((1._0_3_8_83) · 𝑥)
Axiom	ax-ros336 34784	Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 27450 states that the ψ and θ function are asymtotic to each other; this axiom postulates an upper bound for their difference. This is stated as an axiom until a formal proof can be provided. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62) · (√‘𝑥))
Theorem	hgt750lemc 34785*	An upper bound to the summatory function of the von Mangoldt function. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1._0_3_8_83) · 𝑁))
Theorem	hgt750lemd 34786*	An upper bound to the summatory function of the von Mangoldt function on non-primes. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1._4_2_63) · (√‘𝑁)))
Theorem	hgt749d 34787*	A deduction version of ax-hgt749 34782. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑂)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    ⇒   ⊢ (𝜑 → ∃ℎ ∈ ((0[,)+∞) ↑m ℕ)∃𝑘 ∈ ((0[,)+∞) ↑m ℕ)(∀𝑚 ∈ ℕ (𝑘‘𝑚) ≤ (1._0_7_9_9_55) ∧ ∀𝑚 ∈ ℕ (ℎ‘𝑚) ≤ (1._4_14) ∧ ((0._0_0_0_4_2_2_48) · (𝑁↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · ℎ)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝑘)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥))
Theorem	logdivsqrle 34788	Conditions for ((log x ) / ( sqrt 𝑥)) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (exp‘2) ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((log‘𝐵) / (√‘𝐵)) ≤ ((log‘𝐴) / (√‘𝐴)))
Theorem	hgt750lem 34789	Lemma for tgoldbachgtd 34800. (Contributed by Thierry Arnoux, 17-Dec-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48))
Theorem	hgt750lem2 34790	Decimal multiplication galore! (Contributed by Thierry Arnoux, 26-Dec-2021.)
⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (7._3_48)
Theorem	hgt750lemf 34791*	Lemma for the statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℝ)    &   ⊢ (𝜑 → 𝑄 ∈ ℝ)    &   ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ 𝑃)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ 𝑄)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((𝑃↑2) · 𝑄) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
Theorem	hgt750lemg 34792*	Lemma for the statement 7.50 of [Helfgott] p. 69. Applying a permutation 𝑇 to the three factors of a product does not change the result. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ 𝐹 = (𝑐 ∈ 𝑅 ↦ (𝑐 ∘ 𝑇))    &   ⊢ (𝜑 → 𝑇:(0..^3)–1-1-onto→(0..^3))    &   ⊢ (𝜑 → 𝑁:(0..^3)⟶ℕ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑅)    ⇒   ⊢ (𝜑 → ((𝐿‘((𝐹‘𝑁)‘0)) · ((𝐿‘((𝐹‘𝑁)‘1)) · (𝐿‘((𝐹‘𝑁)‘2)))) = ((𝐿‘(𝑁‘0)) · ((𝐿‘(𝑁‘1)) · (𝐿‘(𝑁‘2)))))
Theorem	oddprm2 34793*	Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    ⇒   ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
Theorem	hgt750lemb 34794*	An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 2 ≤ 𝑁)    &   ⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
Theorem	hgt750lema 34795*	An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 2 ≤ 𝑁)    &   ⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}    &   ⊢ 𝐹 = (𝑑 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑑 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))))    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
Theorem	hgt750leme 34796*	An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    &   ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14))    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
Theorem	tgoldbachgnn 34797*	Lemma for tgoldbachgtd 34800. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑂)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	tgoldbachgtde 34798*	Lemma for tgoldbachgtd 34800. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑂)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    &   ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14))    &   ⊢ (𝜑 → ((0._0_0_0_4_2_2_48) · (𝑁↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)    ⇒   ⊢ (𝜑 → 0 < Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
Theorem	tgoldbachgtda 34799*	Lemma for tgoldbachgtd 34800. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑂)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    &   ⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14))    &   ⊢ (𝜑 → ((0._0_0_0_4_2_2_48) · (𝑁↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)    ⇒   ⊢ (𝜑 → 0 < (♯‘((𝑂 ∩ ℙ)(repr‘3)𝑁)))
Theorem	tgoldbachgtd 34800*	Odd integers greater than (;10↑;27) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of [Helfgott] p. 70. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑂)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    ⇒   ⊢ (𝜑 → 0 < (♯‘((𝑂 ∩ ℙ)(repr‘3)𝑁)))