P. 353 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35201-35300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	signshwrd 35201*	𝐻, 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 35202*	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 35203*	𝐻 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 35204*	The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
Theorem	rpsqrtcn 35205	Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (√ ↾ ℝ+) ∈ (ℝ+–cn→ℝ+)
Theorem	divsqrtid 35206	A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / (√‘𝐴)) = (√‘𝐴))
Theorem	cxpcncf1 35207*	The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn 27055. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ⊆ (ℂ ∖ (-∞(,]0)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴)) ∈ (𝐷–cn→ℂ))
Theorem	efmul2picn 35208*	Multiplying by (i · (2 · π)) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (exp‘((i · (2 · π)) · 𝐵))) ∈ (𝐴–cn→ℂ))
Theorem	fct2relem 35209	Lemma for ftc2re 35210. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸)
Theorem	ftc2re 35210*	The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℂ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	fdvposlt 35211*	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 35212*	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 35213*	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 35214*	Functions with a nonpositive derivative, i.e., decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ 𝐸 = (𝐶(,)𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐹:𝐸⟶ℝ)    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ))    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0)    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴))
Theorem	prodfzo03 35215*	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 35216*	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 35217*	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 35218*	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 35219*	Lemma for breprexp 35245- 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 35220	Representations of a number as a sum of nonnegative integers.
class repr
Definition	df-repr 35221*	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 35222*	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 35223	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 35224	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 35225*	Sums of values of the members of the representation of 𝑀 equal 𝑀. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(repr‘𝑆)𝑀))    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)(𝐶‘𝑎) = 𝑀)
Theorem	reprle 35226	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 35227*	Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))    ⇒   ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹)
Theorem	reprfi 35228	Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) ∈ Fin)
Theorem	reprss 35229	Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐵(repr‘𝑆)𝑀) ⊆ (𝐴(repr‘𝑆)𝑀))
Theorem	reprinrn 35230*	Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐 ⊆ 𝐵)))
Theorem	reprlt 35231	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 35232*	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 35233	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 35234	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 35235	Corollary of reprinfz1 35234. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin)
Theorem	reprfz1 35236	Corollary of reprinfz1 35234. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁))
Theorem	hashrepr 35237*	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 35238*	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 35239*	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 35240*	Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛))
Theorem	chtvalz 35241*	Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
Theorem	breprexplema 35242*	Lemma for breprexp 35245 (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 35243	Lemma for breprexp 35245 (closure). (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    &   ⊢ (𝜑 → 𝑋 ∈ (0..^𝑆))    &   ⊢ (𝜑 → 𝑌 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐿‘𝑋)‘𝑌) ∈ ℂ)
Theorem	breprexplemc 35244*	Lemma for breprexp 35245 (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 35245*	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 35246 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 35246*	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 35247	The Vinogradov trigonometric sums.
class vts
Definition	df-vts 35248*	Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
Theorem	vtsval 35249*	Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) = Σ𝑎 ∈ (1...𝑁)((𝐿‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑋)))))
Theorem	vtscl 35250	Closure of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) ∈ ℂ)
Theorem	vtsprod 35251*	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 35252*	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 35253*	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 35254*	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 35255*	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 35256*	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 35257	Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 27790 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 35258	Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 27788 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 35259*	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 35260*	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 35261*	A deduction version of ax-hgt749 35256. (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 35262	Conditions for ((log x ) / ( sqrt 𝑥)) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (exp‘2) ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((log‘𝐵) / (√‘𝐵)) ≤ ((log‘𝐴) / (√‘𝐴)))
Theorem	hgt750lem 35263	Lemma for tgoldbachgtd 35274. (Contributed by Thierry Arnoux, 17-Dec-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48))
Theorem	hgt750lem2 35264	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 35265*	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 35266*	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 35267*	Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    ⇒   ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
Theorem	hgt750lemb 35268*	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 35269*	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 35270*	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 35271*	Lemma for tgoldbachgtd 35274. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑂)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	tgoldbachgtde 35272*	Lemma for tgoldbachgtd 35274. (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 35273*	Lemma for tgoldbachgtd 35274. (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 35274*	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)𝑁)))
Theorem	tgoldbachgt 35275*	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 , expressed using the set 𝐺 of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐺 = {𝑧 ∈ 𝑂 ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}    ⇒   ⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))
21.3.28  Elementary Geometry
21.3.28.1  Two-dimensional geometry This definition has been superseded by DimTarskiG≥ and is no longer needed in the main part of set.mm. It is only kept here for reference.
Syntax	cstrkg2d 35276	Extends class notation with the class of geometries fulfilling the planarity axioms.
class TarskiG2D
Definition	df-trkg2d 35277*	Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of [Schwabhauser] p. 12, and the upper dimension axiom, Axiom A9 of [Schwabhauser] p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019.) (New usage is discouraged.)
⊢ TarskiG2D = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
Theorem	istrkg2d 35278*	Property of fulfilling dimension 2 axiom. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    ⇒   ⊢ (𝐺 ∈ TarskiG2D ↔ (𝐺 ∈ V ∧ (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((((𝑥 − 𝑢) = (𝑥 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑦 − 𝑣) ∧ (𝑧 − 𝑢) = (𝑧 − 𝑣)) ∧ 𝑢 ≠ 𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
Theorem	axtglowdim2ALTV 35279*	Alternate version of axtglowdim2 28914. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG2D)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))
Theorem	axtgupdim2ALTV 35280	Alternate version of axtgupdim2 28915. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → (𝑋 − 𝑈) = (𝑋 − 𝑉))    &   ⊢ (𝜑 → (𝑌 − 𝑈) = (𝑌 − 𝑉))    &   ⊢ (𝜑 → (𝑍 − 𝑈) = (𝑍 − 𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG2D)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
21.3.28.2  Morley's Miracle
Theorem	cgranbtwn 35281	Null angle implies betweenness. (Contributed by SS, 4-Jun-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐼𝐶))    ⇒   ⊢ (𝜑 → (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))
Theorem	btwnlng13 35282	If 𝑍 is between 𝑋 and 𝑌, or 𝑌 is between 𝑋 and 𝑍, then 𝑍 lies on the line 𝑋𝑌. (Contributed by SS, 4-Jun-2026.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))    ⇒   ⊢ (𝜑 → 𝑍 ∈ (𝑋𝐿𝑌))
Theorem	morleylemrneab 35283	Lemma for morley . (Contributed by TA and SS, 4-Jun-2026.)
⊢ 𝑆 = (Base‘𝐺)    &   ⊢ 𝐿 = (LineG‘𝐺)    &   ⊢ ∼ = (cgrA‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    &   ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))    &   ⊢ (𝜑 → ⟨“𝐶𝐴𝑄”⟩ ∼ ⟨“𝑄𝐴𝑅”⟩)    &   ⊢ (𝜑 → ⟨“𝑅𝐴𝐵”⟩ ∼ ⟨“𝑄𝐴𝑅”⟩)    &   ⊢ (𝜑 → ⟨“𝐴𝐵𝑅”⟩ ∼ ⟨“𝑅𝐵𝑃”⟩)    &   ⊢ (𝜑 → ⟨“𝑃𝐵𝐶”⟩ ∼ ⟨“𝑅𝐵𝑃”⟩)    &   ⊢ (𝜑 → ⟨“𝐵𝐶𝑃”⟩ ∼ ⟨“𝑃𝐶𝑄”⟩)    &   ⊢ (𝜑 → ⟨“𝑄𝐶𝐴”⟩ ∼ ⟨“𝑃𝐶𝑄”⟩)    ⇒   ⊢ (𝜑 → ¬ 𝑅 ∈ (𝐴𝐿𝐵))
21.3.28.3  Outer Five Segment (not used, no need to move to main)
Syntax	cafs 35284	Declare the syntax for the outer five segment configuration.
class AFS
Definition	df-afs 35285*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 28909). See df-ofs 36718. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) (Revised by Thierry Arnoux, 15-Mar-2019.)
⊢ AFS = (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))})
Theorem	afsval 35286*	Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → (AFS‘𝐺) = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))})
Theorem	brafs 35287	Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑂 = (AFS‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑂⟨⟨𝑋, 𝑌⟩, ⟨𝑍, 𝑊⟩⟩ ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊)))))
Theorem	tg5segofs 35288	Rephrase axtg5seg 28909 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ 𝑂 = (AFS‘𝐺)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑂⟨⟨𝐸, 𝐹⟩, ⟨𝐻, 𝐼⟩⟩)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐻 − 𝐼))
21.3.29  LeftPad Project See https://github.com/tirix/lets-prove-leftpad.
Syntax	clpad 35289	Extend class notation with the leftpad function.
class leftpad
Definition	df-lpad 35290*	Define the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
Theorem	lpadval 35291	Value of the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐶 leftpad 𝑊)‘𝐿) = (((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊))
Theorem	lpadlem1 35292	Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ∈ Word 𝑆)
Theorem	lpadlem3 35293	Lemma for lpadlen1 35294. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐿 ≤ (♯‘𝑊))    ⇒   ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) = ∅)
Theorem	lpadlen1 35294	Length of a left-padded word, in the case the length of the given word 𝑊 is at least the desired length. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐿 ≤ (♯‘𝑊))    ⇒   ⊢ (𝜑 → (♯‘((𝐶 leftpad 𝑊)‘𝐿)) = (♯‘𝑊))
Theorem	lpadlem2 35295	Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → (♯‘𝑊) ≤ 𝐿)    ⇒   ⊢ (𝜑 → (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = (𝐿 − (♯‘𝑊)))
Theorem	lpadlen2 35296	Length of a left-padded word, in the case the given word 𝑊 is shorter than the desired length. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → (♯‘𝑊) ≤ 𝐿)    ⇒   ⊢ (𝜑 → (♯‘((𝐶 leftpad 𝑊)‘𝐿)) = 𝐿)
Theorem	lpadmax 35297	Length of a left-padded word, in the general case, expressed with an if statement. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (♯‘((𝐶 leftpad 𝑊)‘𝐿)) = if(𝐿 ≤ (♯‘𝑊), (♯‘𝑊), 𝐿))
Theorem	lpadleft 35298	The contents of prefix of a left-padded word is always the letter 𝐶. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(𝐿 − (♯‘𝑊))))    ⇒   ⊢ (𝜑 → (((𝐶 leftpad 𝑊)‘𝐿)‘𝑁) = 𝐶)
Theorem	lpadright 35299	The suffix of a left-padded word the original word 𝑊. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑀 = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊))))    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (((𝐶 leftpad 𝑊)‘𝐿)‘(𝑁 + 𝑀)) = (𝑊‘𝑁))
21.4  Mathbox for Jonathan Ben-Naim Note: On 4-Sep-2016 and after, 745 unused theorems were deleted from this mathbox, and 359 theorems used only once or twice were merged into their referencing theorems. The originals can be recovered from set.mm versions prior to this date.
Syntax	w-bnj17 35300	Extend wff notation with the 4-way conjunction. (New usage is discouraged.)
wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)