P. 390 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38901-39000   *Has distinct variable group(s)

Type	Label	Description
Statement
Axiom	ax-hgprmladder 38901	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.)
|- E. d e. ( ZZ>= ` 3 ) E. f e. (RePart ` d ) ( ( ( f ` 0 ) = 7 /\ ( f ` 1 ) = ; 1 3 /\ ( f ` d ) = (; 8 9 x. ( 10 ^; 2 9 ) ) ) /\ A. i e. ( 0..^ d ) ( ( f ` i ) e. ( Prime \ { 2 } ) /\ ( ( f ` ( i + 1 ) ) - ( f ` i ) ) < ( ( 4 x. ( 10 ^; 1 8 ) ) - 4 ) /\ 4 < ( ( f ` ( i + 1 ) ) - ( f ` i ) ) ) )
Theorem	tgblthelfgott 38902	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 38900, ax-hgprmladder 38901 and bgoldbtbnd 38898. (Contributed by AV, 4-Aug-2020.)
|- ( ( N e. Odd /\ 7 < N /\ N < (; 8 8 x. ( 10 ^; 2 9 ) ) ) -> N e. GoldbachOddALTV )
Theorem	tgoldbachlt 38903*	The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big m greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott 38902. (Contributed by AV, 4-Aug-2020.)
|- E. m e. NN ( ( 8 x. ( 10 ^; 3 0 ) ) < m /\ A. n e. Odd ( ( 7 < n /\ n < m ) -> n e. GoldbachOddALTV ) )
Axiom	ax-tgoldbachgt 38904*	The ternary Goldbach conjecture is valid for big odd numbers (i.e. for all odd numbers greater than a fixed m). 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.)
|- E. m e. NN ( m <_ ( 10 ^; 2 7 ) /\ A. n e. Odd ( m < n -> n e. GoldbachOddALTV ) )
Theorem	tgoldbach 38905	The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 38903 and ax-tgoldbachgt 38904. (Contributed by AV, 2-Aug-2020.)
|- A. n e. Odd ( 7 < n -> n e. GoldbachOddALTV )
21.33.5  Proth's theorem
Theorem	modexp2m1d 38906	The square of an integer which is -1 modulo a number greater than 1 is 1 modulo the same modulus. (Contributed by AV, 5-Jul-2020.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> 1 < E )   &    |- ( ph -> ( A mod E ) = ( -u 1 mod E ) )   =>    |- ( ph -> ( ( A ^ 2 ) mod E ) = 1 )
Theorem	proththdlem 38907	Lemma for proththd 38908. (Contributed by AV, 4-Jul-2020.)
|- ( ph -> N e. NN )   &    |- ( ph -> K e. NN )   &    |- ( ph -> P = ( ( K x. ( 2 ^ N ) ) + 1 ) )   =>    |- ( ph -> ( P e. NN /\ 1 < P /\ ( ( P - 1 ) / 2 ) e. NN ) )
Theorem	proththd 38908*	Proth's theorem (1878). If P is a Proth number, i.e. a number of the form k2^n+1 with k less than 2^n, and if there exists an integer x for which x^((P-1)/2) is -1 modulo P, then P is prime. Such a prime is called a Proth prime. Like Pocklington's theorem (see pockthg 14843), Proth's theorem allows for a convenient method for verifying large primes. (Contributed by AV, 5-Jul-2020.)
|- ( ph -> N e. NN )   &    |- ( ph -> K e. NN )   &    |- ( ph -> P = ( ( K x. ( 2 ^ N ) ) + 1 ) )   &    |- ( ph -> K < ( 2 ^ N ) )   &    |- ( ph -> E. x e. ZZ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) )   =>    |- ( ph -> P e. Prime )
Theorem	5tcu2e40 38909	5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.)
|- ( 5 x. ( 2 ^ 3 ) ) = ; 4 0
Theorem	3exp4mod41 38910	3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.)
|- ( ( 3 ^ 4 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )
Theorem	41prothprmlem1 38911	Lemma 1 for 41prothprm 38913. (Contributed by AV, 4-Jul-2020.)
|- P = ; 4 1   =>    |- ( ( P - 1 ) / 2 ) = ; 2 0
Theorem	41prothprmlem2 38912	Lemma 2 for 41prothprm 38913. (Contributed by AV, 5-Jul-2020.)
|- P = ; 4 1   =>    |- ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P )
Theorem	41prothprm 38913	41 is a Proth prime. (Contributed by AV, 5-Jul-2020.)
|- P = ; 4 1   =>    |- ( P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) /\ P e. Prime )
21.33.6  Words over a set (extension)
21.33.6.1  Last symbol of a word (extension)
Theorem	lswn0 38914	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.)
|- ( ( W e. Word V /\ (/) e/ V /\ ( # ` W ) =/= 0 ) -> ( lastS ` W ) =/= (/) )
21.33.6.2  Concatenations with singleton words (extension)
Theorem	ccatw2s1cl 38915	The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )
21.33.6.3  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 38916	Syntax for the prefix operator.
class prefix
Definition	df-pfx 38917*	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 = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
Theorem	pfxval 38918	Value of a prefix. (Contributed by AV, 2-May-2020.)
|- ( ( S e. V /\ L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
Theorem	pfx00 38919	A zero length prefix. (Contributed by AV, 2-May-2020.)
|- ( S prefix 0 ) = (/)
Theorem	pfx0 38920	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
|- ( (/) prefix L ) = (/)
Theorem	pfxcl 38921	Closure of the prefix extractor. (Contributed by AV, 2-May-2020.)
|- ( S e. Word A -> ( S prefix L ) e. Word A )
Theorem	pfxmpt 38922*	Value of the prefix extractor as mapping. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( x e. ( 0..^ L ) |-> ( S ` x ) ) )
Theorem	pfxres 38923	Value of the prefix extractor as restriction. Could replace swrd0val 12772. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( S |` ( 0..^ L ) ) )
Theorem	pfxf 38924	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 12778. (Contributed by AV, 2-May-2020.)
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) : ( 0..^ L ) --> V )
Theorem	pfxfn 38925	Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word V /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) Fn ( 0..^ L ) )
Theorem	pfxlen 38926	Length of a prefix. Could replace swrd0len 12773. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix L ) ) = L )
Theorem	pfxid 38927	A word is a prefix of itself. (Contributed by AV, 2-May-2020.)
|- ( S e. Word A -> ( S prefix ( # ` S ) ) = S )
Theorem	pfxrn 38928	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.)
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix L ) C_ V )
Theorem	pfxn0 38929	A prefix consisting of at least one symbol is not empty. Could replace swrdn0 12781. (Contributed by AV, 2-May-2020.)
|- ( ( W e. Word V /\ L e. NN /\ L <_ ( # ` W ) ) -> ( W prefix L ) =/= (/) )
Theorem	pfxnd 38930	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.)
|- ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( W prefix L ) = (/) )
Theorem	pfxlen0 38931	Length of a prefix of a word reduced by a single symbol. Could replace swrd0len0 12787. TODO-AV: Really useful? swrd0len0 12787 is only used in wwlknred 25444. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) = ( L + 1 ) ) -> ( # ` ( W prefix L ) ) = L )
Theorem	addlenrevpfx 38932	The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) = ( # ` W ) )
Theorem	addlenpfx 38933	The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W prefix M ) ) + ( # ` ( W substr <. M , ( # ` W ) >. ) ) ) = ( # ` W ) )
Theorem	pfxfv 38934	A symbol in a prefix of a word, indexed using the prefix' indices. Could replace swrd0fv 12790. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0..^ L ) ) -> ( ( W prefix L ) ` I ) = ( W ` I ) )
Theorem	pfxfv0 38935	The first symbol in a prefix of a word. Could replace swrd0fv0 12791. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` 0 ) = ( W ` 0 ) )
Theorem	pfxtrcfv 38936	A symbol in a word truncated by one symbol. Could replace swrdtrcfv 12792. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` I ) = ( W ` I ) )
Theorem	pfxtrcfv0 38937	The first symbol in a word truncated by one symbol. Could replace swrdtrcfv0 12793. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )
Theorem	pfxfvlsw 38938	The last symbol in a (not empty) prefix of a word. Could replace swrd0fvlsw 12794. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( W ` ( L - 1 ) ) )
Theorem	pfxeq 38939*	The prefixes of two words are equal iff they have the same length and the same symbols at each position. Could replace swrdeq 12795. (Contributed by AV, 4-May-2020.)
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( M = N /\ A. i e. ( 0..^ M ) ( W ` i ) = ( U ` i ) ) ) )
Theorem	pfxtrcfvl 38940	The last symbol in a word truncated by one symbol. Could replace swrdtrcfvl 12801. (Contributed by AV, 5-May-2020.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
Theorem	pfxsuffeqwrdeq 38941	Two words are equal if and only if they have the same prefix and the same suffix. Could replace 2swrdeqwrdeq 12804. (Contributed by AV, 5-May-2020.)
|- ( ( W e. Word V /\ S e. Word V /\ I e. ( 0..^ ( # ` W ) ) ) -> ( W = S <-> ( ( # ` W ) = ( # ` S ) /\ ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) ) ) )
Theorem	pfxsuff1eqwrdeq 38942	Two (nonempty) words are equal if and only if they have the same prefix and the same single symbol suffix. Could replace 2swrd1eqwrdeq 12805. (Contributed by AV, 6-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
Theorem	disjwrdpfx 38943*	Sets of words are disjoint if each set contains extensions of distinct words of a fixed length. Could replace disjxwrd 12806. (Contributed by AV, 6-May-2020.)
|- Disj y e. W { x e. Word V | ( x prefix N ) = y }
Theorem	ccatpfx 38944	Joining a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020.)
|- ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) = ( S prefix Z ) )
Theorem	pfxccat1 38945	Recover the left half of a concatenated word. Could replace swrdccat1 12808. (Contributed by AV, 6-May-2020.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) prefix ( # ` S ) ) = S )
Theorem	pfx1 38946	A prefix of length 1. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = <" ( W ` 0 ) "> )
Theorem	pfx2 38947	A prefix of length 2. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> )
Theorem	pfxswrd 38948	A prefix of a subword. Could replace swrd0swrd 12812. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( L e. ( 0 ... ( N - M ) ) -> ( ( W substr <. M , N >. ) prefix L ) = ( W substr <. M , ( M + L ) >. ) ) )
Theorem	swrdpfx 38949	A subword of a prefix. Could replace swrdswrd0 12813. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> ( ( W prefix N ) substr <. K , L >. ) = ( W substr <. K , L >. ) ) )
Theorem	pfxpfx 38950	A prefix of a prefix. Could replace swrd0swrd0 12814. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W prefix N ) prefix L ) = ( W prefix L ) )
Theorem	pfxpfxid 38951	A prefix of a prefix with the same length is the prefix. Could replace swrd0swrdid 12815. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix N ) prefix N ) = ( W prefix N ) )
Theorem	pfxcctswrd 38952	The concatenation of the prefix of a word and the rest of the word yields the word itself. Could replace wrdcctswrd 12816. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix M ) ++ ( W substr <. M , ( # ` W ) >. ) ) = W )
Theorem	lenpfxcctswrd 38953	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 12817. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W prefix M ) ++ ( W substr <. M , ( # ` W ) >. ) ) ) = ( # ` W ) )
Theorem	lenrevpfxcctswrd 38954	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 12818. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W prefix M ) ) ) = ( # ` W ) )
Theorem	pfxlswccat 38955	Reconstruct a nonempty word from its prefix and last symbol. Could replace wrdeqcats1OLD 12825 resp. swrdccatwrd 12819. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = W )
Theorem	ccats1pfxeq 38956	The last symbol of a word concatenated with the word with the last symbol removed having results in the word itself. Could replace ccats1swrdeq 12820. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" ( lastS ` U ) "> ) ) )
Theorem	ccats1pfxeqrex 38957*	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 12830. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> E. s e. V U = ( W ++ <" s "> ) ) )
Theorem	pfxccatin12lem1 38958	Lemma 1 for pfxccatin12 38960. Could replace swrdccatin12lem2b 12837. (Contributed by AV, 9-May-2020.)
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( K - ( L - M ) ) e. ( 0..^ ( N - L ) ) ) )
Theorem	pfxccatin12lem2 38959	Lemma 2 for pfxccatin12 38960. Could replace swrdccatin12lem2 12840. (Contributed by AV, 9-May-2020.)
|- L = ( # ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( B prefix ( N - L ) ) ` ( K - ( # ` ( A substr <. M , L >. ) ) ) ) ) )
Theorem	pfxccatin12 38960	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12 12842. (Contributed by AV, 9-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) )
Theorem	pfxccat3 38961	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 12843. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) )
Theorem	pfxccatpfx1 38962	A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
Theorem	pfxccatpfx2 38963	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.)
|- L = ( # ` A )   &    |- M = ( # ` B )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )
Theorem	pfxccat3a 38964	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 12845. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   &    |- M = ( # ` B )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) ) )
Theorem	pfxccatid 38965	A prefix of a concatenation of length of the first concatenated word is the first word itself. Could replace swrdccatid 12848. (Contributed by AV, 10-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) prefix N ) = A )
Theorem	ccats1pfxeqbi 38966	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 12849. (Contributed by AV, 10-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) <-> U = ( W ++ <" ( lastS ` U ) "> ) ) )
Theorem	pfxccatin12d 38967	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12d 12852. (Contributed by AV, 10-May-2020.)
|- ( ph -> ( # ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( 0 ... L ) )   &    |- ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
Theorem	reuccatpfxs1lem 38968*	Lemma for reuccatpfxs1 38969. Could replace reuccats1lem 12831. (Contributed by AV, 9-May-2020.)
|- ( ( ( W e. Word V /\ U e. X ) /\ A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) )
Theorem	reuccatpfxs1 38969*	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 12832. (Contributed by AV, 10-May-2020.)
|- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! w e. X W = ( w prefix ( # ` W ) ) ) )
Theorem	splvalpfx 38970	Value of the substring replacement operator. (Contributed by AV, 11-May-2020.)
|- ( ( S e. V /\ ( F e. NN0 /\ T e. X /\ R e. Y ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
Theorem	repswpfx 38971	A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020.)
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix L ) = ( S repeatS L ) )
Theorem	cshword2 38972	Perform a cyclical shift for a word. (Contributed by AV, 11-May-2020.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
Theorem	pfxco 38973	Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. ( W prefix N ) ) = ( ( F o. W ) prefix N ) )
21.33.7  Auxiliary theorems for graph theory Additional theorems for classical first-order logic with equality, ZF set theory and theory of real and complex numbers used for proving the theorems for graph theory.
21.33.7.1  Negated equality and membership - extension
Theorem	elnelall 38974	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A e. B -> ( A e/ B -> ph ) )
21.33.7.2  Subclasses and subsets - extension
Theorem	clel5 38975*	Alternate definition of class membership: a class X is an element of another class A iff there is an element of A equal to X. (Contributed by AV, 13-Nov-2020.)
|- ( X e. A <-> E. x e. A X = x )
Theorem	dfss7 38976*	Alternate definition of subclass relationship: a class A is a subclass of another class B iff each element of A is equal to an element of B. (Contributed by AV, 13-Nov-2020.)
|- ( A C_ B <-> A. x e. A E. y e. B x = y )
Theorem	sssseq 38977	If a class is a subclass of another class, the classes are equal iff the other class is a subclass of the first class. (Contributed by AV, 23-Dec-2020.)
|- ( B C_ A -> ( A C_ B <-> A = B ) )
Theorem	prcssprc 38978	The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020.)
|- ( ( A C_ B /\ A e/ _V ) -> B e/ _V )
21.33.7.3  The empty set - extension
Theorem	ralnralall 38979*	A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018.)
|- ( A =/= (/) -> ( ( A. x e. A ph /\ A. x e. A -. ph ) -> ps ) )
Theorem	falseral0 38980*	A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020.)
|- ( ( A. x -. ph /\ A. x e. A ph ) -> A = (/) )
Theorem	ralralimp 38981*	Selecting one of two alternatives within a restricted generalization if one of the alternatives is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.)
|- ( ( ph /\ A =/= (/) ) -> ( A. x e. A ( ( ph -> ( th \/ ta ) ) /\ -. th ) -> ta ) )
Theorem	n0rex 38982*	There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.)
|- ( A =/= (/) -> E. x e. A x e. A )
Theorem	ssn0rex 38983*	There is an element in a class with a nonempty subclass which is an element of the subclass. (Contributed by AV, 17-Dec-2020.)
|- ( ( A C_ B /\ A =/= (/) ) -> E. x e. B x e. A )
21.33.7.4  Unordered and ordered pairs - extension
Theorem	elpwdifsn 38984	A subset of a set is an element of the power set of the difference of the set with a singleton if the subset does not contain the singleton element. (Contributed by AV, 10-Jan-2020.)
|- ( ( S e. W /\ S C_ V /\ A e/ S ) -> S e. ~P ( V \ { A } ) )
Theorem	pr1eqbg 38985	A (proper) pair is equal to another (maybe inproper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( ( ( A e. U /\ B e. V /\ C e. X ) /\ A =/= B ) -> ( A = C <-> { A , B } = { B , C } ) )
Theorem	pr1nebg 38986	A (proper) pair is not equal to another (maybe inproper) pair containing one element of the first pair if and only if the other element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( ( ( A e. U /\ B e. V /\ C e. X ) /\ A =/= B ) -> ( A =/= C <-> { A , B } =/= { B , C } ) )
Theorem	prelpw 38987	A pair of two sets belongs to the power class of a class containing those two sets and vice versa. (Contributed by AV, 8-Jan-2020.)
|- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } e. ~P C ) )
Theorem	rexdifpr 38988	Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.)
|- ( E. x e. ( A \ { B , C } ) ph <-> E. x e. A ( x =/= B /\ x =/= C /\ ph ) )
Theorem	issn 38989*	A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.)
|- ( E. x e. A A. y e. A x = y -> E. z A = { z } )
Theorem	n0snor2el 38990*	A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.)
|- ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
Theorem	opidg 38991	The ordered pair <. A , A >. in Kuratowski's representation. Closed form of opid 4184. (Contributed by AV, 18-Sep-2020.)
|- ( A e. _V -> <. A , A >. = { { A } } )
Theorem	snopeqop 38992	Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) )
Theorem	propeqop 38993	Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   &    |- E e. _V   &    |- F e. _V   =>    |- ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
Theorem	propssopi 38994	If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   &    |- E e. _V   &    |- F e. _V   =>    |- ( { <. A , B >. , <. C , D >. } C_ <. E , F >. -> A = C )
Theorem	ssprss 38995	A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.)
|- ( ( A e. V /\ B e. W ) -> ( { A , B } C_ { C , D } <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )
Theorem	ssprsseq 38996	A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.)
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { C , D } <-> { A , B } = { C , D } ) )
Theorem	elpr2elpr 38997*	For an element of an unordered pair which is a subset of a given set, there is another (maybe the same) element of the given set being an element of the unordered pair. (Contributed by AV, 5-Dec-2020.)
|- ( ( X e. V /\ Y e. V /\ A e. { X , Y } ) -> E. b e. V { X , Y } = { A , b } )
21.33.7.5  Indexed union and intersection - extension
Theorem	iunxprg 38998*	A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
|- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( A e. V /\ B e. W ) -> U_ x e. { A , B } C = ( D u. E ) )
Theorem	iunopeqop 38999*	Equivalence for an ordered pair equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.)
|- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( A =/= (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
Theorem	otiunsndisjX 39000*	The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
|- ( B e. X -> Disj a e. V U_ c e. W { <. a , B , c >. } )