| Metamath
Proof Explorer Theorem List (p. 347 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | signsvfnn 34601* | Adding a letter of a different sign as the highest coefficient changes the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.) |
| ⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏)) & ⊢ 𝑊 = {〈(Base‘ndx), {-1, 0, 1}〉, 〈(+g‘ndx), ⨣ 〉} & ⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) & ⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) & ⊢ (𝜑 → 𝐸 ∈ (Word ℝ ∖ {∅})) & ⊢ (𝜑 → (𝐸‘0) ≠ 0) & ⊢ (𝜑 → 𝐹 = (𝐸 ++ 〈“𝐴”〉)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ 𝑁 = (♯‘𝐸) & ⊢ 𝐵 = (𝐸‘(𝑁 − 1)) ⇒ ⊢ ((𝜑 ∧ (𝐵 · 𝐴) < 0) → ((𝑉‘𝐹) − (𝑉‘𝐸)) = 1) | ||
| Theorem | signlem0 34602* | Adding a zero as the highest coefficient does not change the parity of the sign changes. (Contributed by Thierry Arnoux, 12-Oct-2018.) |
| ⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏)) & ⊢ 𝑊 = {〈(Base‘ndx), {-1, 0, 1}〉, 〈(+g‘ndx), ⨣ 〉} & ⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) & ⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) ⇒ ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) → (𝑉‘(𝐹 ++ 〈“0”〉)) = (𝑉‘𝐹)) | ||
| Theorem | signshf 34603* | 𝐻, corresponding to the word 𝐹 multiplied by (𝑥 − 𝐶), as a function. (Contributed by Thierry Arnoux, 29-Sep-2018.) |
| ⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏)) & ⊢ 𝑊 = {〈(Base‘ndx), {-1, 0, 1}〉, 〈(+g‘ndx), ⨣ 〉} & ⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) & ⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) & ⊢ 𝐻 = ((〈“0”〉 ++ 𝐹) ∘f − ((𝐹 ++ 〈“0”〉) ∘f/c · 𝐶)) ⇒ ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+) → 𝐻:(0..^((♯‘𝐹) + 1))⟶ℝ) | ||
| Theorem | signshwrd 34604* | 𝐻, 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 34605* | 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 34606* | 𝐻 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 ℝ ∧ 𝐶 ∈ ℝ+) → 𝐻 ≠ ∅) | ||
| Theorem | iblidicc 34607* | The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1) | ||
| Theorem | rpsqrtcn 34608 | Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
| ⊢ (√ ↾ ℝ+) ∈ (ℝ+–cn→ℝ+) | ||
| Theorem | divsqrtid 34609 | A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
| ⊢ (𝐴 ∈ ℝ+ → (𝐴 / (√‘𝐴)) = (√‘𝐴)) | ||
| Theorem | cxpcncf1 34610* | The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn 26787. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ⊆ (ℂ ∖ (-∞(,]0))) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴)) ∈ (𝐷–cn→ℂ)) | ||
| Theorem | efmul2picn 34611* | Multiplying by (i · (2 · π)) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
| ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (exp‘((i · (2 · π)) · 𝐵))) ∈ (𝐴–cn→ℂ)) | ||
| Theorem | fct2relem 34612 | Lemma for ftc2re 34613. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
| ⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸) | ||
| Theorem | ftc2re 34613* | The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
| ⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹:𝐸⟶ℂ) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
| Theorem | fdvposlt 34614* | 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 34615* | 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 34616* | 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 34617* | Functions with a nonpositive derivative, i.e., decreasing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
| ⊢ 𝐸 = (𝐶(,)𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐸) & ⊢ (𝜑 → 𝐵 ∈ 𝐸) & ⊢ (𝜑 → 𝐹:𝐸⟶ℝ) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ)) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴)) | ||
| Theorem | prodfzo03 34618* | 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 34619* | 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 34620* | 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 34621* | 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 34622* | Lemma for breprexp 34648- 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...𝑁)𝐵) | ||
| Syntax | crepr 34623 | Representations of a number as a sum of nonnegative integers. |
| class repr | ||
| Definition | df-repr 34624* | 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 34625* | 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 34626 | 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 34627 | 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 34628* | Sums of values of the members of the representation of 𝑀 equal 𝑀. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(repr‘𝑆)𝑀)) ⇒ ⊢ (𝜑 → Σ𝑎 ∈ (0..^𝑆)(𝐶‘𝑎) = 𝑀) | ||
| Theorem | reprle 34629 | 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 34630* | Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {〈𝑆, 𝑏〉})) ⇒ ⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ 𝐴 ran 𝐹) | ||
| Theorem | reprfi 34631 | Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) ∈ Fin) | ||
| Theorem | reprss 34632 | Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐵(repr‘𝑆)𝑀) ⊆ (𝐴(repr‘𝑆)𝑀)) | ||
| Theorem | reprinrn 34633* | Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑐 ∈ ((𝐴 ∩ 𝐵)(repr‘𝑆)𝑀) ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ran 𝑐 ⊆ 𝐵))) | ||
| Theorem | reprlt 34634 | 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 34635* | 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 34636 | 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 34637 | 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 34638 | Corollary of reprinfz1 34637. (Contributed by Thierry Arnoux, 15-Dec-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) ⇒ ⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ∈ Fin) | ||
| Theorem | reprfz1 34639 | Corollary of reprinfz1 34637. (Contributed by Thierry Arnoux, 14-Dec-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) ⇒ ⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁)) | ||
| Theorem | hashrepr 34640* | 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 34641* | 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 34642* | 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 34643* | Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
| ⊢ (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑛 ∈ (1...𝑁)(Λ‘𝑛)) | ||
| Theorem | chtvalz 34644* | Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
| ⊢ (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑛 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑛)) | ||
| Theorem | breprexplema 34645* | Lemma for breprexp 34648 (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 34646 | Lemma for breprexp 34648 (closure). (Contributed by Thierry Arnoux, 7-Dec-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → 𝑍 ∈ ℂ) & ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ)) & ⊢ (𝜑 → 𝑋 ∈ (0..^𝑆)) & ⊢ (𝜑 → 𝑌 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝐿‘𝑋)‘𝑌) ∈ ℂ) | ||
| Theorem | breprexplemc 34647* | Lemma for breprexp 34648 (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 34648* | 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 34649 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 34649* | 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 34650 | The Vinogradov trigonometric sums. |
| class vts | ||
| Definition | df-vts 34651* | Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
| ⊢ vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))))) | ||
| Theorem | vtsval 34652* | Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐿:ℕ⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) = Σ𝑎 ∈ (1...𝑁)((𝐿‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑋))))) | ||
| Theorem | vtscl 34653 | Closure of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 14-Dec-2021.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐿:ℕ⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐿vts𝑁)‘𝑋) ∈ ℂ) | ||
| Theorem | vtsprod 34654* | 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 34655* | 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 34656* | 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 34657* | 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 34658* | 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 34659* | 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 34660 | Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 27525 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 34661 | Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 27523 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 34662* | 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 34663* | 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 34664* | A deduction version of ax-hgt749 34659. (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 34665 | Conditions for ((log x ) / ( sqrt 𝑥)) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (exp‘2) ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((log‘𝐵) / (√‘𝐵)) ≤ ((log‘𝐴) / (√‘𝐴))) | ||
| Theorem | hgt750lem 34666 | Lemma for tgoldbachgtd 34677. (Contributed by Thierry Arnoux, 17-Dec-2021.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ (;10↑;27) ≤ 𝑁) → ((7._3_48) · ((log‘𝑁) / (√‘𝑁))) < (0._0_0_0_4_2_2_48)) | ||
| Theorem | hgt750lem2 34667 | 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 34668* | 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 34669* | 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 34670* | Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
| ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} ⇒ ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ) | ||
| Theorem | hgt750lemb 34671* | 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 34672* | 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 34673* | 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 34674* | Lemma for tgoldbachgtd 34677. (Contributed by Thierry Arnoux, 15-Dec-2021.) |
| ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} & ⊢ (𝜑 → 𝑁 ∈ 𝑂) & ⊢ (𝜑 → (;10↑;27) ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ) | ||
| Theorem | tgoldbachgtde 34675* | Lemma for tgoldbachgtd 34677. (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 34676* | Lemma for tgoldbachgtd 34677. (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 34677* | 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 34678* | 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 34679 | Extends class notation with the class of geometries fulfilling the planarity axioms. |
| class TarskiG2D | ||
| Definition | df-trkg2d 34680* | 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 34681* | 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 34682* | Alternate version of axtglowdim2 28478. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG2D) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) | ||
| Theorem | axtgupdim2ALTV 34683 | Alternate version of axtgupdim2 28479. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → (𝑋 − 𝑈) = (𝑋 − 𝑉)) & ⊢ (𝜑 → (𝑌 − 𝑈) = (𝑌 − 𝑉)) & ⊢ (𝜑 → (𝑍 − 𝑈) = (𝑍 − 𝑉)) & ⊢ (𝜑 → 𝐺 ∈ TarskiG2D) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) | ||
| Syntax | cafs 34684 | Declare the syntax for the outer five segment configuration. |
| class AFS | ||
| Definition | df-afs 34685* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 28473). See df-ofs 35984. 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 34686* | Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → (AFS‘𝐺) = {〈𝑒, 𝑓〉 ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))}) | ||
| Theorem | brafs 34687 | Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.) |
| ⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ 𝑂 = (AFS‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑂〈〈𝑋, 𝑌〉, 〈𝑍, 𝑊〉〉 ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊))))) | ||
| Theorem | tg5segofs 34688 | Rephrase axtg5seg 28473 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 34689 | Extend class notation with the leftpad function. |
| class leftpad | ||
| Definition | df-lpad 34690* | Define the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
| ⊢ leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤))) | ||
| Theorem | lpadval 34691 | Value of the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
| ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐶 leftpad 𝑊)‘𝐿) = (((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)) | ||
| Theorem | lpadlem1 34692 | Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ∈ Word 𝑆) | ||
| Theorem | lpadlem3 34693 | Lemma for lpadlen1 34694. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
| ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐿 ≤ (♯‘𝑊)) ⇒ ⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) = ∅) | ||
| Theorem | lpadlen1 34694 | 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 34695 | Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023.) |
| ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → (♯‘𝑊) ≤ 𝐿) ⇒ ⊢ (𝜑 → (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = (𝐿 − (♯‘𝑊))) | ||
| Theorem | lpadlen2 34696 | 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 34697 | 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 34698 | 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 34699 | 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 34700 | Extend wff notation with the 4-way conjunction. (New usage is discouraged.) |
| wff (𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |