P. 418 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41701-41800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fargshiftf 41701*	If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → 𝐺:(0..^(#‘𝐹))⟶dom 𝐸)
Theorem	fargshiftf1 41702*	If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–1-1→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸)
Theorem	fargshiftfo 41703*	If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–onto→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸)
Theorem	fargshiftfva 41704*	The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (∀𝑘 ∈ (1...𝑁)(𝐸‘(𝐹‘𝑘)) = ⦋𝑘 / 𝑥⦌𝑃 → ∀𝑙 ∈ (0..^𝑁)(𝐸‘(𝐺‘𝑙)) = ⦋(𝑙 + 1) / 𝑥⦌𝑃))
20.35.6  Words over a set (extension)
20.35.6.1  Last symbol of a word - extension
Theorem	lswn0 41705	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 ‘𝑊) ≠ ∅)
20.35.6.2  Prefixes of a 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 41706	Syntax for the prefix operator.
class prefix
Definition	df-pfx 41707*	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 41708	Value of a prefix. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr ⟨0, 𝐿⟩))
Theorem	pfx00 41709	A zero length prefix. (Contributed by AV, 2-May-2020.)
⊢ (𝑆 prefix 0) = ∅
Theorem	pfx0 41710	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
⊢ (∅ prefix 𝐿) = ∅
Theorem	pfxcl 41711	Closure of the prefix extractor. (Contributed by AV, 2-May-2020.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) ∈ Word 𝐴)
Theorem	pfxmpt 41712*	Value of the prefix extractor as mapping. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) = (𝑥 ∈ (0..^𝐿) ↦ (𝑆‘𝑥)))
Theorem	pfxres 41713	Value of the prefix extractor as restriction. Could replace swrd0val 13466. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) = (𝑆 ↾ (0..^𝐿)))
Theorem	pfxf 41714	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 13473. (Contributed by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊))) → (𝑊 prefix 𝐿):(0..^𝐿)⟶𝑉)
Theorem	pfxfn 41715	Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 prefix 𝐿) Fn (0..^𝐿))
Theorem	pfxlen 41716	Length of a prefix. Could replace swrd0len 13467. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (#‘(𝑆 prefix 𝐿)) = 𝐿)
Theorem	pfxid 41717	A word is a prefix of itself. (Contributed by AV, 2-May-2020.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix (#‘𝑆)) = 𝑆)
Theorem	pfxrn 41718	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 41719	A prefix consisting of at least one symbol is not empty. Could replace swrdn0 13476. (Contributed by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ ∧ 𝐿 ≤ (#‘𝑊)) → (𝑊 prefix 𝐿) ≠ ∅)
Theorem	pfxnd 41720	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 41721	Length of a prefix of a word reduced by a single symbol. Could replace swrd0len0 13482. (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (#‘𝑊) = (𝐿 + 1)) → (#‘(𝑊 prefix 𝐿)) = 𝐿)
Theorem	addlenrevpfx 41722	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 41723	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 41724	A symbol in a prefix of a word, indexed using the prefix' indices. Could replace swrd0fv 13485. (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = (𝑊‘𝐼))
Theorem	pfxfv0 41725	The first symbol in a prefix of a word. Could replace swrd0fv0 13486. (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(#‘𝑊))) → ((𝑊 prefix 𝐿)‘0) = (𝑊‘0))
Theorem	pfxtrcfv 41726	A symbol in a word truncated by one symbol. Could replace swrdtrcfv 13487. (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ (0..^((#‘𝑊) − 1))) → ((𝑊 prefix ((#‘𝑊) − 1))‘𝐼) = (𝑊‘𝐼))
Theorem	pfxtrcfv0 41727	The first symbol in a word truncated by one symbol. Could replace swrdtrcfv0 13488. (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → ((𝑊 prefix ((#‘𝑊) − 1))‘0) = (𝑊‘0))
Theorem	pfxfvlsw 41728	The last symbol in a (not empty) prefix of a word. Could replace swrd0fvlsw 13489. (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 prefix 𝐿)) = (𝑊‘(𝐿 − 1)))
Theorem	pfxeq 41729*	The prefixes of two words are equal iff they have the same length and the same symbols at each position. Could replace swrdeq 13490. (Contributed by AV, 4-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))))
Theorem	pfxtrcfvl 41730	The last symbol in a word truncated by one symbol. Could replace swrdtrcfvl 13496. (Contributed by AV, 5-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → ( lastS ‘(𝑊 prefix ((#‘𝑊) − 1))) = (𝑊‘((#‘𝑊) − 2)))
Theorem	pfxsuffeqwrdeq 41731	Two words are equal if and only if they have the same prefix and the same suffix. Could replace 2swrdeqwrdeq 13499. (Contributed by AV, 5-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑆 ↔ ((#‘𝑊) = (#‘𝑆) ∧ ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ∧ (𝑊 substr ⟨𝐼, (#‘𝑊)⟩) = (𝑆 substr ⟨𝐼, (#‘𝑊)⟩)))))
Theorem	pfxsuff1eqwrdeq 41732	Two (nonempty) words are equal if and only if they have the same prefix and the same single symbol suffix. Could replace 2swrd1eqwrdeq 13500. (Contributed by AV, 6-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈)))))
Theorem	disjwrdpfx 41733*	Sets of words are disjoint if each set contains extensions of distinct words of a fixed length. Could replace disjxwrd 13501. (Contributed by AV, 6-May-2020.)
⊢ Disj 𝑦 ∈ 𝑊 {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦}
Theorem	ccatpfx 41734	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 41735	Recover the left half of a concatenated word. Could replace swrdccat1 13503. (Contributed by AV, 6-May-2020.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) prefix (#‘𝑆)) = 𝑆)
Theorem	pfx1 41736	A prefix of length 1. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 prefix 1) = ⟨“(𝑊‘0)”⟩)
Theorem	pfx2 41737	A prefix of length 2. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	pfxswrd 41738	A prefix of a subword. Could replace swrd0swrd 13507. (Contributed by AV, 8-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝐿 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 substr ⟨𝑀, 𝑁⟩) prefix 𝐿) = (𝑊 substr ⟨𝑀, (𝑀 + 𝐿)⟩)))
Theorem	swrdpfx 41739	A subword of a prefix. Could replace swrdswrd0 13508. (Contributed by AV, 8-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 prefix 𝑁) substr ⟨𝐾, 𝐿⟩) = (𝑊 substr ⟨𝐾, 𝐿⟩)))
Theorem	pfxpfx 41740	A prefix of a prefix. Could replace swrd0swrd0 13509. (Contributed by AV, 8-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 prefix 𝑁) prefix 𝐿) = (𝑊 prefix 𝐿))
Theorem	pfxpfxid 41741	A prefix of a prefix with the same length is the prefix. Could replace swrd0swrdid 13510. (Contributed by AV, 8-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 𝑁) prefix 𝑁) = (𝑊 prefix 𝑁))
Theorem	pfxcctswrd 41742	The concatenation of the prefix of a word and the rest of the word yields the word itself. Could replace wrdcctswrd 13511. (Contributed by AV, 9-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 𝑀) ++ (𝑊 substr ⟨𝑀, (#‘𝑊)⟩)) = 𝑊)
Theorem	lenpfxcctswrd 41743	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 13512. (Contributed by AV, 9-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘((𝑊 prefix 𝑀) ++ (𝑊 substr ⟨𝑀, (#‘𝑊)⟩))) = (#‘𝑊))
Theorem	lenrevpfxcctswrd 41744	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 13513. (Contributed by AV, 9-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘((𝑊 substr ⟨𝑀, (#‘𝑊)⟩) ++ (𝑊 prefix 𝑀))) = (#‘𝑊))
Theorem	pfxlswccat 41745	Reconstruct a nonempty word from its prefix and last symbol. Could replace swrdccatwrd 13514. (Contributed by AV, 9-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 prefix ((#‘𝑊) − 1)) ++ ⟨“( lastS ‘𝑊)”⟩) = 𝑊)
Theorem	ccats1pfxeq 41746	The last symbol of a word concatenated with the word with the last symbol removed having results in the word itself. Could replace ccats1swrdeq 13515. (Contributed by AV, 9-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ ⟨“( lastS ‘𝑈)”⟩)))
Theorem	ccats1pfxeqrex 41747*	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 13524. (Contributed by AV, 9-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) → ∃𝑠 ∈ 𝑉 𝑈 = (𝑊 ++ ⟨“𝑠”⟩)))
Theorem	pfxccatin12lem1 41748	Lemma 1 for pfxccatin12 41750. Could replace swrdccatin12lem2b 13532. (Contributed by AV, 9-May-2020.)
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿))))
Theorem	pfxccatin12lem2 41749	Lemma 2 for pfxccatin12 41750. Could replace swrdccatin12lem2 13535. (Contributed by AV, 9-May-2020.)
⊢ 𝐿 = (#‘𝐴)    ⇒   ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝐾 − (#‘(𝐴 substr ⟨𝑀, 𝐿⟩))))))
Theorem	pfxccatin12 41750	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12 13537. (Contributed by AV, 9-May-2020.)
⊢ 𝐿 = (#‘𝐴)    ⇒   ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))
Theorem	pfxccat3 41751	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 13538. (Contributed by AV, 10-May-2020.)
⊢ 𝐿 = (#‘𝐴)    ⇒   ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))))
Theorem	pfxccatpfx1 41752	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 41753	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 41754	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 13540. (Contributed by AV, 10-May-2020.)
⊢ 𝐿 = (#‘𝐴)    &   ⊢ 𝑀 = (#‘𝐵)    ⇒   ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(𝐿 + 𝑀)) → ((𝐴 ++ 𝐵) prefix 𝑁) = if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿))))))
Theorem	pfxccatid 41755	A prefix of a concatenation of length of the first concatenated word is the first word itself. Could replace swrdccatid 13543. (Contributed by AV, 10-May-2020.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → ((𝐴 ++ 𝐵) prefix 𝑁) = 𝐴)
Theorem	ccats1pfxeqbi 41756	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 13544. (Contributed by AV, 10-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) ↔ 𝑈 = (𝑊 ++ ⟨“( lastS ‘𝑈)”⟩)))
Theorem	pfxccatin12d 41757	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12d 13547. (Contributed by AV, 10-May-2020.)
⊢ (𝜑 → (#‘𝐴) = 𝐿)    &   ⊢ (𝜑 → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉))    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝐿))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))    ⇒   ⊢ (𝜑 → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))
Theorem	reuccatpfxs1lem 41758*	Lemma for reuccatpfxs1 41759. Could replace reuccats1lem 13525. (Contributed by AV, 9-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ ∀𝑠 ∈ 𝑉 ((𝑊 ++ ⟨“𝑠”⟩) ∈ 𝑋 → 𝑆 = 𝑠) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ ⟨“𝑆”⟩)))
Theorem	reuccatpfxs1 41759*	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 13526. (Contributed by AV, 10-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ ⟨“𝑣”⟩) ∈ 𝑋 → ∃!𝑤 ∈ 𝑋 𝑊 = (𝑤 prefix (#‘𝑊))))
Theorem	splvalpfx 41760	Value of the substring replacement operator. (Contributed by AV, 11-May-2020.)
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (#‘𝑆)⟩)))
Theorem	repswpfx 41761	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 41762	Perform a cyclical shift for a word. (Contributed by AV, 11-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (#‘𝑊)))))
Theorem	pfxco 41763	Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 prefix 𝑁)) = ((𝐹 ∘ 𝑊) prefix 𝑁))
20.35.7  Number theory (extension)
20.35.7.1  Fermat numbers At first, the (sequence of) Fermat numbers FermatNo (the 𝑛-th Fermat number is denoted as (FermatNo‘𝑛)) is defined, see df-fmtno 41765, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 41814, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 41820. The fourth Fermat number (i.e., the fifth Fermat prime) (FermatNo‘4) = ;;;;65537 is currently the biggest number proven to be prime in set.mm, see 65537prm 41813 (previously, it was ;;;4001, see 4001prm 15899). Another important result of this section is Goldbach's theorem goldbachth 41784, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 41825. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 41829.
Syntax	cfmtno 41764	Extend class notation with the Fermat numbers.
class FermatNo
Definition	df-fmtno 41765	Define the function that enumerates the Fermat numbers, see definition in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))
Theorem	fmtno 41766	The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))
Theorem	fmtnoge3 41767	Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3))
Theorem	fmtnonn 41768	Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ)
Theorem	fmtnom1nn 41769	A Fermat number minus one is a power of a power of two. (Contributed by AV, 29-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → ((FermatNo‘𝑁) − 1) = (2↑(2↑𝑁)))
Theorem	fmtnoodd 41770	Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁))
Theorem	fmtnorn 41771*	A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021.)
⊢ (𝐹 ∈ ran FermatNo ↔ ∃𝑛 ∈ ℕ0 (FermatNo‘𝑛) = 𝐹)
Theorem	fmtnof1 41772	The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021.)
⊢ FermatNo:ℕ0–1-1→ℕ
Theorem	fmtnoinf 41773	The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.)
⊢ ran FermatNo ∉ Fin
Theorem	fmtnorec1 41774	The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties, 22-Jul-2021. (Contributed by AV, 22-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = ((((FermatNo‘𝑁) − 1)↑2) + 1))
Theorem	sqrtpwpw2p 41775	The floor of the square root of 2 to the power of 2 to the power of a positive integer plus a bounded nonnegative integer. (Contributed by AV, 28-Jul-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < ((2↑((2↑(𝑁 − 1)) + 1)) + 1)) → (⌊‘(√‘((2↑(2↑𝑁)) + 𝑀))) = (2↑(2↑(𝑁 − 1))))
Theorem	fmtnosqrt 41776	The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1))))
Theorem	fmtno0 41777	The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) = 3
Theorem	fmtno1 41778	The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) = 5
Theorem	fmtnorec2lem 41779*	Lemma for fmtnorec2 41780 (induction step). (Contributed by AV, 29-Jul-2021.)
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)))
Theorem	fmtnorec2 41780*	The second recurrence relation for Fermat numbers, see ProofWiki "Product of Sequence of Fermat Numbers plus 2", 29-Jul-2021, https://proofwiki.org/wiki/Product_of_Sequence_of_Fermat_Numbers_plus_2 or Wikipedia "Fermat number", 29-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 29-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = (∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛) + 2))
Theorem	fmtnodvds 41781	Any Fermat number divides a greater Fermat number minus 2. Corrolary of fmtnorec2 41780, see ProofWiki "Product of Sequence of Fermat Numbers plus 2/Corollary", 31-Jul-2021. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ) → (FermatNo‘𝑁) ∥ ((FermatNo‘(𝑁 + 𝑀)) − 2))
Theorem	goldbachthlem1 41782	Lemma 1 for goldbachth 41784. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2))
Theorem	goldbachthlem2 41783	Lemma 2 for goldbachth 41784. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)
Theorem	goldbachth 41784	Goldbach's theorem: Two different Fermat numbers are coprime. See ProofWiki "Goldbach's theorem", 31-Jul-2021, https://proofwiki.org/wiki/Goldbach%27s_Theorem or Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ≠ 𝑀) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)
Theorem	fmtnorec3 41785*	The third recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 2-Aug-2021.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (FermatNo‘𝑁) = ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) · ∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛))))
Theorem	fmtnorec4 41786	The fourth recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 31-Jul-2021.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (FermatNo‘𝑁) = (((FermatNo‘(𝑁 − 1))↑2) − (2 · (((FermatNo‘(𝑁 − 2)) − 1)↑2))))
Theorem	fmtno2 41787	The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) = ;17
Theorem	fmtno3 41788	The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘3) = ;;257
Theorem	fmtno4 41789	The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘4) = ;;;;65537
Theorem	fmtno5lem1 41790	Lemma 1 for fmtno5 41794. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 6) = ;;;;;393216
Theorem	fmtno5lem2 41791	Lemma 2 for fmtno5 41794. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 5) = ;;;;;327680
Theorem	fmtno5lem3 41792	Lemma 3 for fmtno5 41794. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 3) = ;;;;;196608
Theorem	fmtno5lem4 41793	Lemma 4 for fmtno5 41794. (Contributed by AV, 30-Jul-2021.)
⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296
Theorem	fmtno5 41794	The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.)
⊢ (FermatNo‘5) = ;;;;;;;;;4294967297
Theorem	fmtno0prm 41795	The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) ∈ ℙ
Theorem	fmtno1prm 41796	The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) ∈ ℙ
Theorem	fmtno2prm 41797	The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) ∈ ℙ
Theorem	257prm 41798	257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ ;;257 ∈ ℙ
Theorem	fmtno3prm 41799	The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ (FermatNo‘3) ∈ ℙ
Theorem	odz2prm2pw 41800	Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021.)
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1)) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))