P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reprgt 32501	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 32502	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 32503	Corollary of reprinfz1 32502. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    ⇒   ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin)
Theorem	reprfz1 32504	Corollary of reprinfz1 32502. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁))
Theorem	hashrepr 32505*	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 32506*	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 32507*	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 32508*	Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛))
Theorem	chtvalz 32509*	Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛))
Theorem	breprexplema 32510*	Lemma for breprexp 32513 (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 32511	Lemma for breprexp 32513 (closure). (Contributed by Thierry Arnoux, 7-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))    &   ⊢ (𝜑 → 𝑋 ∈ (0..^𝑆))    &   ⊢ (𝜑 → 𝑌 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐿‘𝑋)‘𝑌) ∈ ℂ)
Theorem	breprexplemc 32512*	Lemma for breprexp 32513 (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 32513*	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 32514 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 32514*	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...(𝑆 · 𝑁))(𝑅 · (𝑍↑𝑚)))
20.3.26.2  Vinogradov Trigonometric Sums and the Circle Method
Syntax	cvts 32515	The Vinogradov trigonometric sums.
class vts
Definition	df-vts 32516*	Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
Theorem	vtsval 32517*	Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) = Σ𝑎 ∈ (1...𝑁)((𝐿‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑋)))))
Theorem	vtscl 32518	Closure of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 14-Dec-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐿:ℕ⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) ∈ ℂ)
Theorem	vtsprod 32519*	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 32520*	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 32521*	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 32522*	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 32523*	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𝑥)
20.3.26.3  The Ternary Goldbach Conjecture: Final Statement
Axiom	ax-hgt749 32524*	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 32525	Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 26534 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 32526	Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 26532 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 32527*	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 32528*	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 32529*	A deduction version of ax-hgt749 32524. (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 32530	Conditions for ((log x ) / ( sqrt 𝑥)) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (exp‘2) ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((log‘𝐵) / (√‘𝐵)) ≤ ((log‘𝐴) / (√‘𝐴)))
Theorem	hgt750lem 32531	Lemma for tgoldbachgtd 32542. (Contributed by Thierry Arnoux, 17-Dec-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48))
Theorem	hgt750lem2 32532	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 32533*	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 32534*	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 32535*	Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    ⇒   ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
Theorem	hgt750lemb 32536*	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 32537*	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 32538*	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 32539*	Lemma for tgoldbachgtd 32542. (Contributed by Thierry Arnoux, 15-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑂)    &   ⊢ (𝜑 → (;10↑;27) ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	tgoldbachgtde 32540*	Lemma for tgoldbachgtd 32542. (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 32541*	Lemma for tgoldbachgtd 32542. (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 32542*	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 32543*	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) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))
20.3.27  Elementary Geometry
20.3.27.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 32544	Extends class notation with the class of geometries fulfilling the planarity axioms.
class TarskiG2D
Definition	df-trkg2d 32545*	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 32546*	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 32547*	Alternate version of axtglowdim2 26735. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG2D)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))
Theorem	axtgupdim2ALTV 32548	Alternate version of axtgupdim2 26736. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → (𝑋 − 𝑈) = (𝑋 − 𝑉))    &   ⊢ (𝜑 → (𝑌 − 𝑈) = (𝑌 − 𝑉))    &   ⊢ (𝜑 → (𝑍 − 𝑈) = (𝑍 − 𝑉))    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG2D)    ⇒   ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
20.3.27.2  Outer Five Segment (not used, no need to move to main)
Syntax	cafs 32549	Declare the syntax for the outer five segment configuration.
class AFS
Definition	df-afs 32550*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 26730). See df-ofs 34212. 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 32551*	Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    ⇒   ⊢ (𝜑 → (AFS‘𝐺) = {⟨𝑒, 𝑓⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))})
Theorem	brafs 32552	Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ 𝑃 = (Base‘𝐺)    &   ⊢ − = (dist‘𝐺)    &   ⊢ 𝐼 = (Itv‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ TarskiG)    &   ⊢ 𝑂 = (AFS‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑂⟨⟨𝑋, 𝑌⟩, ⟨𝑍, 𝑊⟩⟩ ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊)))))
Theorem	tg5segofs 32553	Rephrase axtg5seg 26730 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‘𝐺)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑃)    &   ⊢ (𝜑 → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑂⟨⟨𝐸, 𝐹⟩, ⟨𝐻, 𝐼⟩⟩)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐻 − 𝐼))
20.3.28  LeftPad Project See https://github.com/tirix/lets-prove-leftpad.
Syntax	clpad 32554	Extend class notation with the leftpad function.
class leftpad
Definition	df-lpad 32555*	Define the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
Theorem	lpadval 32556	Value of the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐶 leftpad 𝑊)‘𝐿) = (((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊))
Theorem	lpadlem1 32557	Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ∈ Word 𝑆)
Theorem	lpadlem3 32558	Lemma for lpadlen1 32559. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐿 ≤ (♯‘𝑊))    ⇒   ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) = ∅)
Theorem	lpadlen1 32559	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 32560	Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → (♯‘𝑊) ≤ 𝐿)    ⇒   ⊢ (𝜑 → (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = (𝐿 − (♯‘𝑊)))
Theorem	lpadlen2 32561	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 32562	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 32563	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 32564	The suffix of a left-padded word the original word 𝑊. (Contributed by Thierry Arnoux, 7-Aug-2023.)
⊢ (𝜑 → 𝐿 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑀 = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊))))    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (((𝐶 leftpad 𝑊)‘𝐿)‘(𝑁 + 𝑀)) = (𝑊‘𝑁))
20.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 32565	Extend wff notation with the 4-way conjunction. (New usage is discouraged.)
wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃)
Definition	df-bnj17 32566	Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃))
Syntax	c-bnj14 32567	Extend class notation with the function giving: the class of all elements of 𝐴 that are "smaller" than 𝑋 according to 𝑅. (New usage is discouraged.)
class pred(𝑋, 𝐴, 𝑅)
Definition	df-bnj14 32568*	Define the function giving: the class of all elements of 𝐴 that are "smaller" than 𝑋 according to 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ pred(𝑋, 𝐴, 𝑅) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}
Syntax	w-bnj13 32569	Extend wff notation with the following predicate: 𝑅 is set-like on 𝐴. (New usage is discouraged.)
wff 𝑅 Se 𝐴
Definition	df-bnj13 32570*	Define the following predicate: 𝑅 is set-like on 𝐴. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 pred(𝑥, 𝐴, 𝑅) ∈ V)
Syntax	w-bnj15 32571	Extend wff notation with the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (New usage is discouraged.)
wff 𝑅 FrSe 𝐴
Definition	df-bnj15 32572	Define the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑅 FrSe 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴))
Syntax	c-bnj18 32573	Extend class notation with the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. (New usage is discouraged.)
class trCl(𝑋, 𝐴, 𝑅)
Definition	df-bnj18 32574*	Define the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 32806. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
Syntax	w-bnj19 32575	Extend wff notation with the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (New usage is discouraged.)
wff TrFo(𝐵, 𝐴, 𝑅)
Definition	df-bnj19 32576*	Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥 ∈ 𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵)
20.4.1  First-order logic and set theory
Theorem	bnj170 32577	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
Theorem	bnj240 32578	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → 𝜓′)    &   ⊢ (𝜒 → 𝜒′)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓′ ∧ 𝜒′))
Theorem	bnj248 32579	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃))
Theorem	bnj250 32580	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)))
Theorem	bnj251 32581	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))))
Theorem	bnj252 32582	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)))
Theorem	bnj253 32583	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃))
Theorem	bnj255 32584	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)))
Theorem	bnj256 32585	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
Theorem	bnj257 32586	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ 𝜃 ∧ 𝜒))
Theorem	bnj258 32587	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒))
Theorem	bnj268 32588	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	bnj290 32589	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	bnj291 32590	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓))
Theorem	bnj312 32591	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒 ∧ 𝜃))
Theorem	bnj334 32592	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜑 ∧ 𝜓 ∧ 𝜃))
Theorem	bnj345 32593	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜃 ∧ 𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj422 32594	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃 ∧ 𝜑 ∧ 𝜓))
Theorem	bnj432 32595	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜒 ∧ 𝜃) ∧ (𝜑 ∧ 𝜓)))
Theorem	bnj446 32596	∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑))
Theorem	bnj23 32597*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}    ⇒   ⊢ (∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝑦 → ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑦 → [𝑤 / 𝑥]𝜑))
Theorem	bnj31 32598	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	bnj62 32599*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ([𝑧 / 𝑥]𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴)
Theorem	bnj89 32600*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑦]∃!𝑥𝜑 ↔ ∃!𝑥[𝑍 / 𝑦]𝜑)