Home | Metamath
Proof Explorer Theorem List (p. 403 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sgoldbaltlem1 40201 | Lemma 1 for sgoldbalt 40203: If an even number greater than 4 is the sum of two primes, one of the prime summands must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd )) | ||
Theorem | sgoldbaltlem2 40202 | Lemma 2 for sgoldbalt 40203: If an even number greater than 4 is the sum of two primes, the primes must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → (𝑃 ∈ Odd ∧ 𝑄 ∈ Odd ))) | ||
Theorem | sgoldbalt 40203* | An alternate (the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020.) |
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | ||
Theorem | nnsum3primes4 40204* | 4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) |
⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) | ||
Theorem | nnsum4primes4 40205* | 4 is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 4 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) | ||
Theorem | nnsum3primesprm 40206* | Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020.) (Proof shortened by AV, 17-Apr-2021.) |
⊢ (𝑃 ∈ ℙ → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑃 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | nnsum4primesprm 40207* | Every prime is "the sum of at most 4" (actually one - the prime itself) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
⊢ (𝑃 ∈ ℙ → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 4 ∧ 𝑃 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | nnsum3primesgbe 40208* | Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) |
⊢ (𝑁 ∈ GoldbachEven → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | nnsum4primesgbe 40209* | Any even Goldbach number is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
⊢ (𝑁 ∈ GoldbachEven → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 4 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | nnsum3primesle9 40210* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 3 primes. (Contributed by AV, 2-Aug-2020.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | nnsum4primesle9 40211* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 4 primes. (Contributed by AV, 24-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 4 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | nnsum4primesodd 40212* | If the (weak) ternary Goldbach conjecture is valid, then every odd integer greater than 5 is the sum of 3 primes. (Contributed by AV, 2-Jul-2020.) |
⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘6) ∧ 𝑁 ∈ Odd ) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) | ||
Theorem | nnsum4primesoddALTV 40213* | If the (strong) ternary Goldbach conjecture is valid, then every odd integer greater than 7 is the sum of 3 primes. (Contributed by AV, 26-Jul-2020.) |
⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) → ((𝑁 ∈ (ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) | ||
Theorem | evengpop3 40214* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of an odd Goldbach number and 3. (Contributed by AV, 24-Jul-2020.) |
⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3))) | ||
Theorem | evengpoap3 40215* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of an odd Goldbach number and 3. (Contributed by AV, 27-Jul-2020.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) → ((𝑁 ∈ (ℤ≥‘;12) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddALTV 𝑁 = (𝑜 + 3))) | ||
Theorem | nnsum4primeseven 40216* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020.) |
⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) | ||
Theorem | nnsum4primesevenALTV 40217* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of 4 primes. (Contributed by AV, 27-Jul-2020.) |
⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) → ((𝑁 ∈ (ℤ≥‘;12) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) | ||
Theorem | wtgoldbnnsum4prm 40218* | If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in [Helfgott] p. 4. (Contributed by AV, 25-Jul-2020.) |
⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 4 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | stgoldbnnsum4prm 40219* | If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020.) |
⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 4 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | bgoldbnnsum3prm 40220* | If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020.) |
⊢ (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | ||
Theorem | bgoldbtbndlem1 40221 | Lemma 1 for bgoldbtbnd 40225: the odd numbers between 7 and 13 (exclusive) are (strong) odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.) |
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 ∈ (7[,);13)) → 𝑁 ∈ GoldbachOddALTV ) | ||
Theorem | bgoldbtbndlem2 40222* | Lemma 2 for bgoldbtbnd 40225. (Contributed by AV, 1-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ 𝑆 = (𝑋 − (𝐹‘(𝐼 − 1))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆))) | ||
Theorem | bgoldbtbndlem3 40223* | Lemma 3 for bgoldbtbnd 40225. (Contributed by AV, 1-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ) & ⊢ 𝑆 = (𝑋 − (𝐹‘𝐼)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆))) | ||
Theorem | bgoldbtbndlem4 40224* | Lemma 4 for bgoldbtbnd 40225. (Contributed by AV, 1-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ) ⇒ ⊢ (((𝜑 ∧ 𝐼 ∈ (1..^𝐷)) ∧ 𝑋 ∈ Odd ) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑋 = ((𝑝 + 𝑞) + 𝑟)))) | ||
Theorem | bgoldbtbnd 40225* | If the binary Goldbach conjecture is valid up to an integer 𝑁, and there is a series ("ladder") of primes with a difference of at most 𝑁 up to an integer 𝑀, then the strong ternary Goldbach conjecture is valid up to 𝑀, see section 1.2.2 in [Helfgott] p. 4 with N = 4 x 10^18, taken from [OeSilva], and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOddALTV )) | ||
Axiom | ax-bgbltosilva 40226 | The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see result of [OeSilva] p. ?. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven ) | ||
Theorem | bgoldbachlt 40227* | The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big 𝑚). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva 40226. (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ∃𝑚 ∈ ℕ ((4 · (;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven )) | ||
Axiom | ax-hgprmladder 40228 | There is a partition ("ladder") of primes from 7 to 8.8 x 10^30 with parts ("rungs") having lengths of at least 4 and at most N - 4, see section 1.2.2 in [Helfgott] p. 4. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ∃𝑑 ∈ (ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) | ||
Theorem | tgblthelfgott 40229 | The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in [Helfgott] p. 4, using bgoldbachlt 40227, ax-hgprmladder 40228 and bgoldbtbnd 40225. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOddALTV ) | ||
Theorem | tgoldbachlt 40230* | The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big 𝑚 greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott 40229. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV )) | ||
Axiom | ax-tgoldbachgt 40231* | The ternary Goldbach conjecture is valid for big odd numbers (i.e. for all odd numbers greater than a fixed 𝑚). This is proven by Helfgott (see section 7.4 in [Helfgott] p. 70) for m = 10^27. Temporarily provided as "axiom". (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )) | ||
Theorem | tgoldbach 40232 | The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 40230 and ax-tgoldbachgt 40231. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ) | ||
Axiom | ax-bgbltosilvaOLD 40233 | Obsolete version of ax-bgbltosilva 40226 as of 9-Sep-2021. (Contributed by AV, 3-Aug-2020.) (New usage is discouraged.) |
⊢ ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (10↑;18))) → 𝑁 ∈ GoldbachEven ) | ||
Theorem | bgoldbachltOLD 40234* | Obsolete version of bgoldbachlt 40227 as of 9-Sep-2021. (Contributed by AV, 3-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑚 ∈ ℕ ((4 · (10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven )) | ||
Axiom | ax-hgprmladderOLD 40235 | Obsolete version of ax-hgprmladder 40228 as of 9-Sep-2021. (Contributed by AV, 3-Aug-2020.) (New usage is discouraged.) |
⊢ ∃𝑑 ∈ (ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) | ||
Theorem | tgblthelfgottOLD 40236 | Obsolete version of tgblthelfgott 40229 as of 9-Sep-2021. (Contributed by AV, 4-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (10↑;29))) → 𝑁 ∈ GoldbachOddALTV ) | ||
Theorem | tgoldbachltOLD 40237* | Obsolete version of tgoldbachlt 40230 as of 9-Sep-2021. (Contributed by AV, 4-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑚 ∈ ℕ ((8 · (10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV )) | ||
Axiom | ax-tgoldbachgtOLD 40238* | Obsolete version of ax-tgoldbachgt 40231 as of 9-Sep-2021. (Contributed by AV, 2-Aug-2020.) (New usage is discouraged.) |
⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )) | ||
Theorem | tgoldbachOLD 40239 | Obsolete version of tgoldbach 40232 as of 9-Sep-2021. (Contributed by AV, 2-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ) | ||
Theorem | wrdred1 40240 | A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.) |
⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word 𝑆) | ||
Theorem | wrdred1hash 40241 | The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (#‘𝐹)) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1)) | ||
Theorem | lswn0 40242 | The last symbol of a not empty word exists. The empty set must be excluded as symbol, because otherwise, it cannot be distinguished between valid cases (∅ is the last symbol) and invalid cases (∅ means that no last symbol exists. This is because of the special definition of a function in set.mm. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ (#‘𝑊) ≠ 0) → ( lastS ‘𝑊) ≠ ∅) | ||
Theorem | ccatw2s1cl 40243 | The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉) | ||
In https://www.allacronyms.com/prefix/abbreviated, "pfx" is proposed as abbreviation for "prefix". Regarding the meaning of "prefix", it is different in computer science (automata theory/formal languages) compared with linguistics: in linguistics, a prefix has a meaning (see Wikipedia "Prefix" https://en.wikipedia.org/wiki/Prefix), whereas in computer science, a prefix is an arbitrary substring/subword starting at the beginning of a string/word (see Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix or https://math.stackexchange.com/questions/2190559/ is-there-standard-terminology-notation-for-the-prefix-of-a-word ). | ||
Syntax | cpfx 40244 | Syntax for the prefix operator. |
class prefix | ||
Definition | df-pfx 40245* | Define an operation which extracts prefixes of words, i.e. subwords starting at the beginning of a word. Definition in section 9.1 of [AhoHopUll] p. 318. "pfx" is used as label fragment. (Contributed by AV, 2-May-2020.) |
⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) | ||
Theorem | pfxval 40246 | Value of a prefix. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr 〈0, 𝐿〉)) | ||
Theorem | pfx00 40247 | A zero length prefix. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 prefix 0) = ∅ | ||
Theorem | pfx0 40248 | A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.) |
⊢ (∅ prefix 𝐿) = ∅ | ||
Theorem | pfxcl 40249 | Closure of the prefix extractor. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) ∈ Word 𝐴) | ||
Theorem | pfxmpt 40250* | Value of the prefix extractor as mapping. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) = (𝑥 ∈ (0..^𝐿) ↦ (𝑆‘𝑥))) | ||
Theorem | pfxres 40251 | Value of the prefix extractor as restriction. Could replace swrd0val 13273. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) = (𝑆 ↾ (0..^𝐿))) | ||
Theorem | pfxf 40252 | A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. Could replace swrd0f 13279. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊))) → (𝑊 prefix 𝐿):(0..^𝐿)⟶𝑉) | ||
Theorem | pfxfn 40253 | Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) Fn (0..^𝐿)) | ||
Theorem | pfxlen 40254 | Length of a prefix. Could replace swrd0len 13274. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (#‘(𝑆 prefix 𝐿)) = 𝐿) | ||
Theorem | pfxid 40255 | A word is a prefix of itself. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix (#‘𝑆)) = 𝑆) | ||
Theorem | pfxrn 40256 | The range of a prefix of a word is a subset of the set of symbols for the word. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ 𝑉) | ||
Theorem | pfxn0 40257 | A prefix consisting of at least one symbol is not empty. Could replace swrdn0 13282. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ ∧ 𝐿 ≤ (#‘𝑊)) → (𝑊 prefix 𝐿) ≠ ∅) | ||
Theorem | pfxnd 40258 | The value of the prefix extractor is the empty set (undefined) if the argument is not within the range of the word. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (#‘𝑊) < 𝐿) → (𝑊 prefix 𝐿) = ∅) | ||
Theorem | pfxlen0 40259 | Length of a prefix of a word reduced by a single symbol. Could replace swrd0len0 13288. TODO-AV: Really useful? swrd0len0 13288 is only used in wwlknred 26251. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (#‘𝑊) = (𝐿 + 1)) → (#‘(𝑊 prefix 𝐿)) = 𝐿) | ||
Theorem | addlenrevpfx 40260 | The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 substr 〈𝑀, (#‘𝑊)〉)) + (#‘(𝑊 prefix 𝑀))) = (#‘𝑊)) | ||
Theorem | addlenpfx 40261 | The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 prefix 𝑀)) + (#‘(𝑊 substr 〈𝑀, (#‘𝑊)〉))) = (#‘𝑊)) | ||
Theorem | pfxfv 40262 | A symbol in a prefix of a word, indexed using the prefix' indices. Could replace swrd0fv 13291. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | pfxfv0 40263 | The first symbol in a prefix of a word. Could replace swrd0fv0 13292. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(#‘𝑊))) → ((𝑊 prefix 𝐿)‘0) = (𝑊‘0)) | ||
Theorem | pfxtrcfv 40264 | A symbol in a word truncated by one symbol. Could replace swrdtrcfv 13293. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ (0..^((#‘𝑊) − 1))) → ((𝑊 prefix ((#‘𝑊) − 1))‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | pfxtrcfv0 40265 | The first symbol in a word truncated by one symbol. Could replace swrdtrcfv0 13294. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → ((𝑊 prefix ((#‘𝑊) − 1))‘0) = (𝑊‘0)) | ||
Theorem | pfxfvlsw 40266 | The last symbol in a (not empty) prefix of a word. Could replace swrd0fvlsw 13295. (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 prefix 𝐿)) = (𝑊‘(𝐿 − 1))) | ||
Theorem | pfxeq 40267* | The prefixes of two words are equal iff they have the same length and the same symbols at each position. Could replace swrdeq 13296. (Contributed by AV, 4-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) | ||
Theorem | pfxtrcfvl 40268 | The last symbol in a word truncated by one symbol. Could replace swrdtrcfvl 13302. (Contributed by AV, 5-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → ( lastS ‘(𝑊 prefix ((#‘𝑊) − 1))) = (𝑊‘((#‘𝑊) − 2))) | ||
Theorem | pfxsuffeqwrdeq 40269 | Two words are equal if and only if they have the same prefix and the same suffix. Could replace 2swrdeqwrdeq 13305. (Contributed by AV, 5-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑆 ↔ ((#‘𝑊) = (#‘𝑆) ∧ ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ∧ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉))))) | ||
Theorem | pfxsuff1eqwrdeq 40270 | Two (nonempty) words are equal if and only if they have the same prefix and the same single symbol suffix. Could replace 2swrd1eqwrdeq 13306. (Contributed by AV, 6-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) | ||
Theorem | disjwrdpfx 40271* | Sets of words are disjoint if each set contains extensions of distinct words of a fixed length. Could replace disjxwrd 13307. (Contributed by AV, 6-May-2020.) |
⊢ Disj 𝑦 ∈ 𝑊 {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦} | ||
Theorem | ccatpfx 40272 | Joining a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆))) → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) = (𝑆 prefix 𝑍)) | ||
Theorem | pfxccat1 40273 | Recover the left half of a concatenated word. Could replace swrdccat1 13309. (Contributed by AV, 6-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) prefix (#‘𝑆)) = 𝑆) | ||
Theorem | pfx1 40274 | A prefix of length 1. (Contributed by AV, 15-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 prefix 1) = 〈“(𝑊‘0)”〉) | ||
Theorem | pfx2 40275 | A prefix of length 2. (Contributed by AV, 15-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → (𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉) | ||
Theorem | pfxswrd 40276 | A prefix of a subword. Could replace swrd0swrd 13313. (Contributed by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝐿 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 substr 〈𝑀, 𝑁〉) prefix 𝐿) = (𝑊 substr 〈𝑀, (𝑀 + 𝐿)〉))) | ||
Theorem | swrdpfx 40277 | A subword of a prefix. Could replace swrdswrd0 13314. (Contributed by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 prefix 𝑁) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉))) | ||
Theorem | pfxpfx 40278 | A prefix of a prefix. Could replace swrd0swrd0 13315. (Contributed by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 prefix 𝑁) prefix 𝐿) = (𝑊 prefix 𝐿)) | ||
Theorem | pfxpfxid 40279 | A prefix of a prefix with the same length is the prefix. Could replace swrd0swrdid 13316. (Contributed by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 𝑁) prefix 𝑁) = (𝑊 prefix 𝑁)) | ||
Theorem | pfxcctswrd 40280 | The concatenation of the prefix of a word and the rest of the word yields the word itself. Could replace wrdcctswrd 13317. (Contributed by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 𝑀) ++ (𝑊 substr 〈𝑀, (#‘𝑊)〉)) = 𝑊) | ||
Theorem | lenpfxcctswrd 40281 | The length of the concatenation of the prefix of a word and the rest of the word is the length of the word. Could replace lencctswrd 13318. (Contributed by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘((𝑊 prefix 𝑀) ++ (𝑊 substr 〈𝑀, (#‘𝑊)〉))) = (#‘𝑊)) | ||
Theorem | lenrevpfxcctswrd 40282 | The length of the concatenation of the rest of a word and the prefix of the word is the length of the word. Could replace lenrevcctswrd 13319. (Contributed by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘((𝑊 substr 〈𝑀, (#‘𝑊)〉) ++ (𝑊 prefix 𝑀))) = (#‘𝑊)) | ||
Theorem | pfxlswccat 40283 | Reconstruct a nonempty word from its prefix and last symbol. Could replace swrdccatwrd 13320. (Contributed by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 prefix ((#‘𝑊) − 1)) ++ 〈“( lastS ‘𝑊)”〉) = 𝑊) | ||
Theorem | ccats1pfxeq 40284 | The last symbol of a word concatenated with the word with the last symbol removed having results in the word itself. Could replace ccats1swrdeq 13321. (Contributed by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“( lastS ‘𝑈)”〉))) | ||
Theorem | ccats1pfxeqrex 40285* | There exists a symbol such that its concatenation with the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. Could replace ccats1swrdeqrex 13330. (Contributed by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) → ∃𝑠 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑠”〉))) | ||
Theorem | pfxccatin12lem1 40286 | Lemma 1 for pfxccatin12 40288. Could replace swrdccatin12lem2b 13337. (Contributed by AV, 9-May-2020.) |
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿)))) | ||
Theorem | pfxccatin12lem2 40287 | Lemma 2 for pfxccatin12 40288. Could replace swrdccatin12lem2 13340. (Contributed by AV, 9-May-2020.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝐾 − (#‘(𝐴 substr 〈𝑀, 𝐿〉)))))) | ||
Theorem | pfxccatin12 40288 | The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12 13342. (Contributed by AV, 9-May-2020.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))) | ||
Theorem | pfxccat3 40289 | The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. Could replace swrdccat3 13343. (Contributed by AV, 10-May-2020.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈𝑀, 𝑁〉), if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))))) | ||
Theorem | pfxccatpfx1 40290 | A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...𝐿)) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 prefix 𝑁)) | ||
Theorem | pfxccatpfx2 40291 | A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020.) |
⊢ 𝐿 = (#‘𝐴) & ⊢ 𝑀 = (#‘𝐵) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) | ||
Theorem | pfxccat3a 40292 | A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. Could replace swrdccat3a 13345. (Contributed by AV, 10-May-2020.) |
⊢ 𝐿 = (#‘𝐴) & ⊢ 𝑀 = (#‘𝐵) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(𝐿 + 𝑀)) → ((𝐴 ++ 𝐵) prefix 𝑁) = if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))))) | ||
Theorem | pfxccatid 40293 | A prefix of a concatenation of length of the first concatenated word is the first word itself. Could replace swrdccatid 13348. (Contributed by AV, 10-May-2020.) |
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → ((𝐴 ++ 𝐵) prefix 𝑁) = 𝐴) | ||
Theorem | ccats1pfxeqbi 40294 | A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. Could replace ccats1swrdeqbi 13349. (Contributed by AV, 10-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) ↔ 𝑈 = (𝑊 ++ 〈“( lastS ‘𝑈)”〉))) | ||
Theorem | pfxccatin12d 40295 | The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12d 13352. (Contributed by AV, 10-May-2020.) |
⊢ (𝜑 → (#‘𝐴) = 𝐿) & ⊢ (𝜑 → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) & ⊢ (𝜑 → 𝑀 ∈ (0...𝐿)) & ⊢ (𝜑 → 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿)))) | ||
Theorem | reuccatpfxs1lem 40296* | Lemma for reuccatpfxs1 40297. Could replace reuccats1lem 13331. (Contributed by AV, 9-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ ∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))) | ||
Theorem | reuccatpfxs1 40297* | There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. Could replace reuccats1 13332. (Contributed by AV, 10-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 → ∃!𝑤 ∈ 𝑋 𝑊 = (𝑤 prefix (#‘𝑊)))) | ||
Theorem | splvalpfx 40298 | Value of the substring replacement operator. (Contributed by AV, 11-May-2020.) |
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) | ||
Theorem | repswpfx 40299 | A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿)) | ||
Theorem | cshword2 40300 | Perform a cyclical shift for a word. (Contributed by AV, 11-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (#‘𝑊))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |