![]() |
Metamath
Proof Explorer Theorem List (p. 321 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hashreprin 32001* | 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 32002 | 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 32003 | 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 32004 | Corollary of reprinfz1 32003. (Contributed by Thierry Arnoux, 15-Dec-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) ⇒ ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin) | ||
Theorem | reprfz1 32005 | Corollary of reprinfz1 32003. (Contributed by Thierry Arnoux, 14-Dec-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) ⇒ ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁)) | ||
Theorem | hashrepr 32006* | 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 32007* | 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 32008* | 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 32009* | Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛)) | ||
Theorem | chtvalz 32010* | Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛)) | ||
Theorem | breprexplema 32011* | Lemma for breprexp 32014 (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 32012 | Lemma for breprexp 32014 (closure). (Contributed by Thierry Arnoux, 7-Dec-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝑍 ∈ ℂ) & ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ)) & ⊢ (𝜑 → 𝑋 ∈ (0..^𝑆)) & ⊢ (𝜑 → 𝑌 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝐿‘𝑋)‘𝑌) ∈ ℂ) | ||
Theorem | breprexplemc 32013* | Lemma for breprexp 32014 (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 32014* | 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 32015 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 32015* | 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...(𝑆 · 𝑁))(𝑅 · (𝑍↑𝑚))) | ||
Syntax | cvts 32016 | The Vinogradov trigonometric sums. |
class vts | ||
Definition | df-vts 32017* | Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
⊢ vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))))) | ||
Theorem | vtsval 32018* | Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐿:ℕ⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) = Σ𝑎 ∈ (1...𝑁)((𝐿‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑋))))) | ||
Theorem | vtscl 32019 | Closure of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 14-Dec-2021.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐿:ℕ⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) ∈ ℂ) | ||
Theorem | vtsprod 32020* | 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 32021* | 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 32022* | 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 32023* | 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 32024* | 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𝑥) | ||
Axiom | ax-hgt749 32025* | 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 32026 | Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 26065 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 32027 | Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 26063 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 32028* | 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 32029* | 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 32030* | A deduction version of ax-hgt749 32025. (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 32031 | Conditions for ((log x ) / ( sqrt 𝑥)) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (exp‘2) ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((log‘𝐵) / (√‘𝐵)) ≤ ((log‘𝐴) / (√‘𝐴))) | ||
Theorem | hgt750lem 32032 | Lemma for tgoldbachgtd 32043. (Contributed by Thierry Arnoux, 17-Dec-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48)) | ||
Theorem | hgt750lem2 32033 | 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 32034* | 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 32035* | 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 32036* | Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} ⇒ ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ) | ||
Theorem | hgt750lemb 32037* | 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 32038* | 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 32039* | 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 32040* | Lemma for tgoldbachgtd 32043. (Contributed by Thierry Arnoux, 15-Dec-2021.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} & ⊢ (𝜑 → 𝑁 ∈ 𝑂) & ⊢ (𝜑 → (;10↑;27) ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ) | ||
Theorem | tgoldbachgtde 32041* | Lemma for tgoldbachgtd 32043. (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 32042* | Lemma for tgoldbachgtd 32043. (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 32043* | 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 32044* | 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) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺)) | ||
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 32045 | Extends class notation with the class of geometries fulfilling the planarity axioms. |
class TarskiG2D | ||
Definition | df-trkg2d 32046* | 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 32047* | 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 32048* | Alternate version of axtglowdim2 26264. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG2D) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) | ||
Theorem | axtgupdim2ALTV 32049 | Alternate version of axtgupdim2 26265. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑋 − 𝑈) = (𝑋 − 𝑉)) & ⊢ (𝜑 → (𝑌 − 𝑈) = (𝑌 − 𝑉)) & ⊢ (𝜑 → (𝑍 − 𝑈) = (𝑍 − 𝑉)) & ⊢ (𝜑 → 𝐺 ∈ TarskiG2D) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) | ||
Syntax | cafs 32050 | Declare the syntax for the outer five segment configuration. |
class AFS | ||
Definition | df-afs 32051* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 26259). See df-ofs 33557. 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 32052* | Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → (AFS‘𝐺) = {〈𝑒, 𝑓〉 ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))}) | ||
Theorem | brafs 32053 | Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑂 = (AFS‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑂〈〈𝑋, 𝑌〉, 〈𝑍, 𝑊〉〉 ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊))))) | ||
Theorem | tg5segofs 32054 | Rephrase axtg5seg 26259 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‘𝐺) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑃) & ⊢ (𝜑 → 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑂〈〈𝐸, 𝐹〉, 〈𝐻, 𝐼〉〉) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐻 − 𝐼)) | ||
Syntax | clpad 32055 | Extend class notation with the leftpad function. |
class leftpad | ||
Definition | df-lpad 32056* | Define the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
⊢ leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤))) | ||
Theorem | lpadval 32057 | Value of the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 leftpad 𝑊)‘𝐿) = (((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)) | ||
Theorem | lpadlem1 32058 | Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ∈ Word 𝑆) | ||
Theorem | lpadlem3 32059 | Lemma for lpadlen1 32060. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐿 ≤ (♯‘𝑊)) ⇒ ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) = ∅) | ||
Theorem | lpadlen1 32060 | 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 32061 | Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → (♯‘𝑊) ≤ 𝐿) ⇒ ⊢ (𝜑 → (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = (𝐿 − (♯‘𝑊))) | ||
Theorem | lpadlen2 32062 | 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 32063 | 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 32064 | 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 32065 | The suffix of a left-padded word the original word 𝑊. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝑀 = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊)))) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊))) ⇒ ⊢ (𝜑 → (((𝐶 leftpad 𝑊)‘𝐿)‘(𝑁 + 𝑀)) = (𝑊‘𝑁)) | ||
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 32066 | Extend wff notation with the 4-way conjunction. (New usage is discouraged.) |
wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) | ||
Definition | df-bnj17 32067 | Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) | ||
Syntax | c-bnj14 32068 | 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 32069* | 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 32070 | Extend wff notation with the following predicate: 𝑅 is set-like on 𝐴. (New usage is discouraged.) |
wff 𝑅 Se 𝐴 | ||
Definition | df-bnj13 32071* | 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 32072 | Extend wff notation with the following predicate: 𝑅 is both well-founded and set-like on 𝐴. (New usage is discouraged.) |
wff 𝑅 FrSe 𝐴 | ||
Definition | df-bnj15 32073 | 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 32074 | Extend class notation with the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. (New usage is discouraged.) |
class trCl(𝑋, 𝐴, 𝑅) | ||
Definition | df-bnj18 32075* | 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 32308. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) | ||
Syntax | w-bnj19 32076 | Extend wff notation with the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (New usage is discouraged.) |
wff TrFo(𝐵, 𝐴, 𝑅) | ||
Definition | df-bnj19 32077* | Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥 ∈ 𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵) | ||
Theorem | bnj170 32078 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑)) | ||
Theorem | bnj240 32079 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜓 → 𝜓′) & ⊢ (𝜒 → 𝜒′) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓′ ∧ 𝜒′)) | ||
Theorem | bnj248 32080 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)) | ||
Theorem | bnj250 32081 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃))) | ||
Theorem | bnj251 32082 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | ||
Theorem | bnj252 32083 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃))) | ||
Theorem | bnj253 32084 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj255 32085 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | bnj256 32086 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | bnj257 32087 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜓 ∧ 𝜃 ∧ 𝜒)) | ||
Theorem | bnj258 32088 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒)) | ||
Theorem | bnj268 32089 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | bnj290 32090 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜑 ∧ 𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | bnj291 32091 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓)) | ||
Theorem | bnj312 32092 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | bnj334 32093 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜑 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | bnj345 32094 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜃 ∧ 𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bnj422 32095 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃 ∧ 𝜑 ∧ 𝜓)) | ||
Theorem | bnj432 32096 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜒 ∧ 𝜃) ∧ (𝜑 ∧ 𝜓))) | ||
Theorem | bnj446 32097 | ∧-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜑)) | ||
Theorem | bnj23 32098* | 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 32099 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | bnj62 32100* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑥]𝑥 Fn 𝐴 ↔ 𝑧 Fn 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |