P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
21.25.3.2  Definitions and basic properties
Syntax	ceven 32501	Extend the definition of a class to include the set of even numbers.
class Even
Syntax	codd 32502	Extend the definition of a class to include the set of odd numbers.
class Odd
Definition	df-even 32503	Define the set of even numbers. (Contributed by AV, 14-Jun-2020.)
|- Even = { z e. ZZ | ( z / 2 ) e. ZZ }
Definition	df-odd 32504	Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.)
|- Odd = { z e. ZZ | ( ( z + 1 ) / 2 ) e. ZZ }
Theorem	iseven 32505	The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
Theorem	isodd 32506	The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd integer increased by 1 and then divided by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) )
Theorem	evenz 32507	An even number is an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Even -> Z e. ZZ )
Theorem	oddz 32508	An odd number is an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Odd -> Z e. ZZ )
Theorem	evendiv2z 32509	The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Even -> ( Z / 2 ) e. ZZ )
Theorem	oddp1div2z 32510	The result of dividing an odd number increased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Odd -> ( ( Z + 1 ) / 2 ) e. ZZ )
Theorem	zob 32511	Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.)
|- ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
Theorem	oddm1div2z 32512	The result of dividing an odd number decreased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Odd -> ( ( Z - 1 ) / 2 ) e. ZZ )
Theorem	isodd2 32513	The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd number decreased by 1 and then divided by 2 is still an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z - 1 ) / 2 ) e. ZZ ) )
Theorem	dfodd2 32514	Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.)
|- Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ }
Theorem	dfodd6 32515*	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) }
Theorem	dfeven4 32516*	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
|- Even = { z e. ZZ | E. i e. ZZ z = ( 2 x. i ) }
Theorem	evenm1odd 32517	The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Even -> ( Z - 1 ) e. Odd )
Theorem	evenp1odd 32518	The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Even -> ( Z + 1 ) e. Odd )
Theorem	oddp1eveni 32519	The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Odd -> ( Z + 1 ) e. Even )
Theorem	oddm1eveni 32520	The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.)
|- ( Z e. Odd -> ( Z - 1 ) e. Even )
Theorem	evennodd 32521	An even number is not an odd number. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Even -> -. Z e. Odd )
Theorem	oddneven 32522	An odd number is not an even number. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Odd -> -. Z e. Even )
Theorem	enege 32523	The negative of an even number is even. (Contributed by AV, 20-Jun-2020.)
|- ( A e. Even -> -u A e. Even )
Theorem	onego 32524	The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.)
|- ( A e. Odd -> -u A e. Odd )
Theorem	m1expevenALTV 32525	Exponentiation of -1 by an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 6-Jul-2020.)
|- ( N e. Even -> ( -u 1 ^ N ) = 1 )
Theorem	m1expoddALTV 32526	Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.)
|- ( N e. Odd -> ( -u 1 ^ N ) = -u 1 )
21.25.3.3  Alternate definitions using the "divides" relation
Theorem	dfeven2 32527	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
|- Even = { z e. ZZ | 2 || z }
Theorem	dfodd3 32528	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | -. 2 || z }
Theorem	iseven2 32529	The predicate "is an even number". An even number is an integer which is divisible by 2. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Even <-> ( Z e. ZZ /\ 2 || Z ) )
Theorem	isodd3 32530	The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ -. 2 || Z ) )
Theorem	2dvdseven 32531	2 divides an even number. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Even -> 2 || Z )
Theorem	2ndvdsodd 32532	2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd -> -. 2 || Z )
Theorem	2dvdsoddp1 32533	2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd -> 2 || ( Z + 1 ) )
Theorem	2dvdsoddm1 32534	2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd -> 2 || ( Z - 1 ) )
21.25.3.4  Alternate definitions using the "modulo" operation
Theorem	dfeven3 32535	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
|- Even = { z e. ZZ | ( z mod 2 ) = 0 }
Theorem	dfodd4 32536	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | ( z mod 2 ) = 1 }
Theorem	dfodd5 32537	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | ( z mod 2 ) =/= 0 }
Theorem	zefldiv2ALTV 32538	The floor of an even number divided by 2 is equal to the even number divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.)
|- ( N e. Even -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
Theorem	zofldiv2ALTV 32539	The floor of an odd numer divided by 2 is equal to the odd number first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.)
|- ( N e. Odd -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
Theorem	oddflALTV 32540	Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 18-Jun-2020.)
|- ( K e. Odd -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )
21.25.3.5  Alternate definitions using the "gcd" operation
Theorem	gcdzeq 32541	A positive integer A is equal to its gcd with an integer B if and only if A divides B. Generalization of gcdeq 14211. (Contributed by AV, 1-Jul-2020.)
|- ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> A || B ) )
Theorem	iseven5 32542	The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.)
|- ( Z e. Even <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 2 ) )
Theorem	isodd7 32543	The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 1 ) )
Theorem	dfeven5 32544	Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)
|- Even = { z e. ZZ | ( 2 gcd z ) = 2 }
Theorem	dfodd7 32545	Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.)
|- Odd = { z e. ZZ | ( 2 gcd z ) = 1 }
21.25.3.6  Theorems of part 5 revised
Theorem	zneoALTV 32546	No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. (Contributed by NM, 31-Jul-2004.) (Revised by AV, 16-Jun-2020.)
|- ( ( A e. Even /\ B e. Odd ) -> A =/= B )
Theorem	zeoALTV 32547	An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.)
|- ( Z e. ZZ -> ( Z e. Even \/ Z e. Odd ) )
Theorem	zeo2ALTV 32548	An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.) (Revised by AV, 16-Jun-2020.)
|- ( Z e. ZZ -> ( Z e. Even <-> -. Z e. Odd ) )
Theorem	nneoALTV 32549	A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 19-Jun-2020.)
|- ( N e. NN -> ( N e. Even <-> -. N e. Odd ) )
Theorem	nneoiALTV 32550	A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) (Revised by AV, 19-Jun-2020.)
|- N e. NN   =>    |- ( N e. Even <-> -. N e. Odd )
21.25.3.7  Theorems of part 6 revised
Theorem	odd2np1ALTV 32551*	An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by AV, 19-Jun-2020.)
|- ( N e. ZZ -> ( N e. Odd <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
Theorem	oddm1evenALTV 32552	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. ZZ -> ( N e. Odd <-> ( N - 1 ) e. Even ) )
Theorem	oddp1evenALTV 32553	An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. ZZ -> ( N e. Odd <-> ( N + 1 ) e. Even ) )
Theorem	oexpnegALTV 32554	The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) (Revised by AV, 19-Jun-2020.)
|- ( ( A e. CC /\ N e. NN /\ N e. Odd ) -> ( -u A ^ N ) = -u ( A ^ N ) )
Theorem	oexpnegnz 32555	The exponential of the negative of a number not being 0, when the exponent is odd. (Contributed by AV, 19-Jun-2020.)
|- ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) -> ( -u A ^ N ) = -u ( A ^ N ) )
Theorem	bits0ALTV 32556	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. ZZ -> ( 0 e. (bits ` N ) <-> N e. Odd ) )
Theorem	bits0eALTV 32557	The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. Even -> -. 0 e. (bits ` N ) )
Theorem	bits0oALTV 32558	The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. Odd -> 0 e. (bits ` N ) )
Theorem	divgcdoddALTV 32559	Either A / ( A gcd B ) is odd or B / ( A gcd B ) is odd. (Contributed by Scott Fenton, 19-Apr-2014.) (Revised by AV, 21-Jun-2020.)
|- ( ( A e. NN /\ B e. NN ) -> ( ( A / ( A gcd B ) ) e. Odd \/ ( B / ( A gcd B ) ) e. Odd ) )
Theorem	opoeALTV 32560	The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Odd ) -> ( A + B ) e. Even )
Theorem	opeoALTV 32561	The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Even ) -> ( A + B ) e. Odd )
Theorem	omoeALTV 32562	The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Odd ) -> ( A - B ) e. Even )
Theorem	omeoALTV 32563	The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Even ) -> ( A - B ) e. Odd )
Theorem	oddprmALTV 32564	A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by AV, 21-Jun-2020.)
|- ( N e. ( Prime \ { 2 } ) -> N e. Odd )
21.25.3.8  Theorems of AV's mathbox revised
Theorem	0evenALTV 32565	0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)
|- 0 e. Even
Theorem	0noddALTV 32566	0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)
|- 0 e/ Odd
Theorem	1oddALTV 32567	1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 1 e. Odd
Theorem	1nevenALTV 32568	1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 1 e/ Even
Theorem	2evenALTV 32569	2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 2 e. Even
Theorem	2noddALTV 32570	2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 2 e/ Odd
Theorem	nn0o1gt2ALTV 32571	An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Odd ) -> ( N = 1 \/ 2 < N ) )
Theorem	nnoALTV 32572	An alternate characterization of an odd number greater than 1. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. NN )
Theorem	nn0oALTV 32573	An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Revised by AV, 21-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. NN0 )
Theorem	nn0e 32574	An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Even ) -> ( N / 2 ) e. NN0 )
Theorem	nn0onn0exALTV 32575*	For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.) (Revised by AV, 22-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Odd ) -> E. m e. NN0 N = ( ( 2 x. m ) + 1 ) )
Theorem	nn0enn0exALTV 32576*	For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.) (Revised by AV, 22-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Even ) -> E. m e. NN0 N = ( 2 x. m ) )
Theorem	nnpw2evenALTV 32577	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.)
|- ( N e. NN -> ( 2 ^ N ) e. Even )
21.25.3.9  Perfect Number Theorem (revised)
Theorem	perfectALTVlem1 32578	Lemma for perfectALTV 32580. (Contributed by Mario Carneiro, 7-Jun-2016.) (Revised by AV, 1-Jul-2020.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> B e. Odd )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
Theorem	perfectALTVlem2 32579	Lemma for perfectALTV 32580. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> B e. Odd )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( B e. Prime /\ B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
Theorem	perfectALTV 32580*	The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer N is a perfect number (that is, its divisor sum is 2 N) if and only if it is of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ), where 2 ^ p - 1 is prime (a Mersenne prime). (It follows from this that p is also prime.) This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) (Proof modification is discouraged.)
|- ( ( N e. NN /\ N e. Even ) -> ( ( 1 sigma N ) = ( 2 x. N ) <-> E. p e. ZZ ( ( ( 2 ^ p ) - 1 ) e. Prime /\ N = ( ( 2 ^ ( p - 1 ) ) x. ( ( 2 ^ p ) - 1 ) ) ) ) )
21.25.3.10  Proth's theorem
Theorem	modexp2m1d 32581	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 32582	Lemma for proththd 32583. (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 32583*	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 14445), 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 32584	5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.)
|- ( 5 x. ( 2 ^ 3 ) ) = ; 4 0
Theorem	3exp4mod41 32585	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 32586	Lemma 1 for 41prothprm 32588. (Contributed by AV, 4-Jul-2020.)
|- P = ; 4 1   =>    |- ( ( P - 1 ) / 2 ) = ; 2 0
Theorem	41prothprmlem2 32587	Lemma 2 for 41prothprm 32588. (Contributed by AV, 5-Jul-2020.)
|- P = ; 4 1   =>    |- ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P )
Theorem	41prothprm 32588	41 is a Proth prime. (Contributed by AV, 5-Jul-2020.)
|- P = ; 4 1   =>    |- ( P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) /\ P e. Prime )
21.25.4  Words over a set (extension)
21.25.4.1  Last symbol of a word (extension)
Theorem	lswn0 32589	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.25.4.2  Concatenations with singleton words (extension)
Theorem	ccatw2s1cl 32590	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.25.4.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 32591	Syntax for the prefix operator.
class prefix
Definition	df-pfx 32592*	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 32593	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 32594	A zero length prefix. (Contributed by AV, 2-May-2020.)
|- ( S prefix 0 ) = (/)
Theorem	pfx0 32595	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
|- ( (/) prefix L ) = (/)
Theorem	pfxcl 32596	Closure of the prefix extractor. (Contributed by AV, 2-May-2020.)
|- ( S e. Word A -> ( S prefix L ) e. Word A )
Theorem	pfxmpt 32597*	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 32598	Value of the prefix extractor as restriction. Could replace swrd0val 12576. (Contributed by AV, 2-May-2020.)
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( S |` ( 0..^ L ) ) )
Theorem	pfxf 32599	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 12582. (Contributed by AV, 2-May-2020.)
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) : ( 0..^ L ) --> V )
Theorem	pfxfn 32600	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 ) )