P. 111 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11001-11100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sswrd 11001	The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)
|- ( S C_ T -> Word S C_ Word T )
Theorem	snopiswrd 11002	A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.)
|- ( S e. V -> { <. 0 , S >. } e. Word V )
Theorem	wrdexg 11003	The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.)
|- ( S e. V -> Word S e. _V )
Theorem	wrdexb 11004	The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)
|- ( S e. _V <-> Word S e. _V )
Theorem	wrdexi 11005	The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.)
|- S e. _V   =>    |- Word S e. _V
Theorem	wrdsymbcl 11006	A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
|- ( ( W e. Word V /\ I e. ( 0..^ (♯ ` W ) ) ) -> ( W ` I ) e. V )
Theorem	wrdfn 11007	A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)
|- ( W e. Word S -> W Fn ( 0..^ (♯ ` W ) ) )
Theorem	wrdv 11008	A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) (Proof shortened by JJ, 18-Nov-2022.)
|- ( W e. Word V -> W e. Word _V )
Theorem	wrdlndm 11009	The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.)
|- ( W e. Word V -> (♯ ` W ) e/ dom W )
Theorem	iswrdsymb 11010*	An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)
|- ( ( W e. Word _V /\ A. i e. ( 0..^ (♯ ` W ) ) ( W ` i ) e. V ) -> W e. Word V )
Theorem	wrdfin 11011	A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)
|- ( W e. Word S -> W e. Fin )
Theorem	lennncl 11012	The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( ( W e. Word S /\ W =/= (/) ) -> (♯ ` W ) e. NN )
Theorem	wrdffz 11013	A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)
|- ( W e. Word S -> W : ( 0 ... ( (♯ ` W ) - 1 ) ) --> S )
Theorem	wrdeq 11014	Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( S = T -> Word S = Word T )
Theorem	wrdeqi 11015	Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)
|- S = T   =>    |- Word S = Word T
Theorem	iswrddm0 11016	A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)
|- ( W : (/) --> S -> W e. Word S )
Theorem	wrd0 11017	The empty set is a word (the empty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 13-May-2020.)
|- (/) e. Word S
Theorem	0wrd0 11018	The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)
|- ( W e. Word (/) <-> W = (/) )
Theorem	wrdsymb 11019	A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)
|- ( S e. Word A -> S e. Word ( S " ( 0..^ (♯ ` S ) ) ) )
Theorem	nfwrd 11020	Hypothesis builder for Word S. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- F/_ x S   =>    |- F/_ xWord S
Theorem	csbwrdg 11021*	Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( S e. V -> [_ S / x ]_Word x = Word S )
Theorem	wrdnval 11022*	Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Proof shortened by AV, 13-May-2020.)
|- ( ( V e. X /\ N e. NN0 ) -> { w e. Word V | (♯ ` w ) = N } = ( V ^m ( 0..^ N ) ) )
Theorem	wrdmap 11023	Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- ( ( V e. X /\ N e. NN0 ) -> ( ( W e. Word V /\ (♯ ` W ) = N ) <-> W e. ( V ^m ( 0..^ N ) ) ) )
Theorem	wrdsymb0 11024	A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( W e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ (♯ ` W ) <_ I ) -> ( W ` I ) = (/) ) )
Theorem	wrdlenge1n0 11025	A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)
|- ( W e. Word V -> ( W =/= (/) <-> 1 <_ (♯ ` W ) ) )
Theorem	len0nnbi 11026	The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)
|- ( W e. Word S -> ( W =/= (/) <-> (♯ ` W ) e. NN ) )
Theorem	wrdlenge2n0 11027	A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ 2 <_ (♯ ` W ) ) -> W =/= (/) )
Theorem	wrdsymb1 11028	The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
|- ( ( W e. Word V /\ 1 <_ (♯ ` W ) ) -> ( W ` 0 ) e. V )
Theorem	wrdlen1 11029*	A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018.) (Proof shortened by AV, 19-Oct-2018.)
|- ( ( W e. Word V /\ (♯ ` W ) = 1 ) -> E. v e. V ( W ` 0 ) = v )
Theorem	fstwrdne 11030	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )
Theorem	fstwrdne0 11031	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( N e. NN /\ ( W e. Word V /\ (♯ ` W ) = N ) ) -> ( W ` 0 ) e. V )
Theorem	eqwrd 11032*	Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.)
|- ( ( U e. Word S /\ W e. Word T ) -> ( U = W <-> ( (♯ ` U ) = (♯ ` W ) /\ A. i e. ( 0..^ (♯ ` U ) ) ( U ` i ) = ( W ` i ) ) ) )
Theorem	elovmpowrd 11033*	Implications for the value of an operation defined by the maps-to notation with a class abstraction of words as a result having an element. Note that ph may depend on z as well as on v and y. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- O = ( v e. _V , y e. _V |-> { z e. Word v | ph } )   =>    |- ( Z e. ( V O Y ) -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) )
Theorem	wrdred1 11034	A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)
|- ( F e. Word S -> ( F |` ( 0..^ ( (♯ ` F ) - 1 ) ) ) e. Word S )
Theorem	wrdred1hash 11035	The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
|- ( ( F e. Word S /\ 1 <_ (♯ ` F ) ) -> (♯ ` ( F |` ( 0..^ ( (♯ ` F ) - 1 ) ) ) ) = ( (♯ ` F ) - 1 ) )
4.7.2  Last symbol of a word
Syntax	clsw 11036	Extend class notation with the Last Symbol of a word.
class lastS
Definition	df-lsw 11037	Extract the last symbol of a word. May be not meaningful for other sets which are not words. The name lastS (as abbreviation of "lastSymbol") is a compromise between usually used names for corresponding functions in computer programs (as last() or lastChar()), the terminology used for words in set.mm ("symbol" instead of "character") and brevity ("lastS" is shorter than "lastChar" and "lastSymbol"). Labels of theorems about last symbols of a word will contain the abbreviation "lsw" (Last Symbol of a Word). (Contributed by Alexander van der Vekens, 18-Mar-2018.)
|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
Theorem	lswwrd 11038	Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.)
|- ( W e. Word V -> (lastS ` W ) = ( W ` ( (♯ ` W ) - 1 ) ) )
Theorem	lsw0 11039	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 19-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
|- ( ( W e. Word V /\ (♯ ` W ) = 0 ) -> (lastS ` W ) = (/) )
Theorem	lsw0g 11040	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
|- (lastS ` (/) ) = (/)
Theorem	lsw1 11041	The last symbol of a word of length 1 is the first symbol of this word. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
|- ( ( W e. Word V /\ (♯ ` W ) = 1 ) -> (lastS ` W ) = ( W ` 0 ) )
Theorem	lswcl 11042	Closure of the last symbol: the last symbol of a nonempty word belongs to the alphabet for the word. (Contributed by AV, 2-Aug-2018.) (Proof shortened by AV, 29-Apr-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> (lastS ` W ) e. V )
Theorem	lswlgt0cl 11043	The last symbol of a nonempty word is an element of the alphabet for the word. (Contributed by Alexander van der Vekens, 1-Oct-2018.) (Proof shortened by AV, 29-Apr-2020.)
|- ( ( N e. NN /\ ( W e. Word V /\ (♯ ` W ) = N ) ) -> (lastS ` W ) e. V )
4.7.3  Concatenations of words
Syntax	cconcat 11044	Syntax for the concatenation operator.
class ++
Definition	df-concat 11045*	Define the concatenation operator which combines two words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.)
|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
Theorem	ccatfvalfi 11046*	Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Fin /\ T e. Fin ) -> ( S ++ T ) = ( x e. ( 0..^ ( (♯ ` S ) + (♯ ` T ) ) ) |-> if ( x e. ( 0..^ (♯ ` S ) ) , ( S ` x ) , ( T ` ( x - (♯ ` S ) ) ) ) ) )
Theorem	ccatcl 11047	The concatenation of two words is a word. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 29-Apr-2020.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) e. Word B )
Theorem	ccatclab 11048	The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.)
|- ( ( S e. Word A /\ T e. Word B ) -> ( S ++ T ) e. Word ( A u. B ) )
Theorem	ccatlen 11049	The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.)
|- ( ( S e. Word A /\ T e. Word B ) -> (♯ ` ( S ++ T ) ) = ( (♯ ` S ) + (♯ ` T ) ) )
Theorem	ccat0 11050	The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022.) (Revised by JJ, 18-Jan-2024.)
|- ( ( S e. Word A /\ T e. Word B ) -> ( ( S ++ T ) = (/) <-> ( S = (/) /\ T = (/) ) ) )
Theorem	ccatval1 11051	Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 30-Apr-2020.) (Revised by JJ, 18-Jan-2024.)
|- ( ( S e. Word A /\ T e. Word B /\ I e. ( 0..^ (♯ ` S ) ) ) -> ( ( S ++ T ) ` I ) = ( S ` I ) )
Theorem	ccatval2 11052	Value of a symbol in the right half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( (♯ ` S )..^ ( (♯ ` S ) + (♯ ` T ) ) ) ) -> ( ( S ++ T ) ` I ) = ( T ` ( I - (♯ ` S ) ) ) )
Theorem	ccatval3 11053	Value of a symbol in the right half of a concatenated word, using an index relative to the subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof shortened by AV, 30-Apr-2020.)
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( 0..^ (♯ ` T ) ) ) -> ( ( S ++ T ) ` ( I + (♯ ` S ) ) ) = ( T ` I ) )
Theorem	elfzelfzccat 11054	An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... (♯ ` A ) ) -> N e. ( 0 ... (♯ ` ( A ++ B ) ) ) ) )
Theorem	ccatvalfn 11055	The concatenation of two words is a function over the half-open integer range having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
|- ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) Fn ( 0..^ ( (♯ ` A ) + (♯ ` B ) ) ) )
Theorem	ccatsymb 11056	The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018.) (Proof shortened by AV, 24-Nov-2018.)
|- ( ( A e. Word V /\ B e. Word V /\ I e. ZZ ) -> ( ( A ++ B ) ` I ) = if ( I < (♯ ` A ) , ( A ` I ) , ( B ` ( I - (♯ ` A ) ) ) ) )
Theorem	ccatfv0 11057	The first symbol of a concatenation of two words is the first symbol of the first word if the first word is not empty. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( A e. Word V /\ B e. Word V /\ 0 < (♯ ` A ) ) -> ( ( A ++ B ) ` 0 ) = ( A ` 0 ) )
Theorem	ccatval1lsw 11058	The last symbol of the left (nonempty) half of a concatenated word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( ( A ++ B ) ` ( (♯ ` A ) - 1 ) ) = (lastS ` A ) )
Theorem	ccatval21sw 11059	The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.)
|- ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( ( A ++ B ) ` (♯ ` A ) ) = ( B ` 0 ) )
Theorem	ccatlid 11060	Concatenation of a word by the empty word on the left. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
|- ( S e. Word B -> ( (/) ++ S ) = S )
Theorem	ccatrid 11061	Concatenation of a word by the empty word on the right. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
|- ( S e. Word B -> ( S ++ (/) ) = S )
Theorem	ccatass 11062	Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Word B /\ T e. Word B /\ U e. Word B ) -> ( ( S ++ T ) ++ U ) = ( S ++ ( T ++ U ) ) )
Theorem	ccatrn 11063	The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Word B /\ T e. Word B ) -> ran ( S ++ T ) = ( ran S u. ran T ) )
Theorem	ccatidid 11064	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
|- ( (/) ++ (/) ) = (/)
Theorem	lswccatn0lsw 11065	The last symbol of a word concatenated with a nonempty word is the last symbol of the nonempty word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> (lastS ` ( A ++ B ) ) = (lastS ` B ) )
Theorem	lswccat0lsw 11066	The last symbol of a word concatenated with the empty word is the last symbol of the word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
|- ( W e. Word V -> (lastS ` ( W ++ (/) ) ) = (lastS ` W ) )
4.8  Elementary real and complex functions
4.8.1  The "shift" operation
Syntax	cshi 11067	Extend class notation with function shifter.
class shift
Definition	df-shft 11068*	Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of CC) and produces a new function on CC. See shftval 11078 for its value. (Contributed by NM, 20-Jul-2005.)
|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
Theorem	shftlem 11069*	Two ways to write a shifted set ( B + A ). (Contributed by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. CC /\ B C_ CC ) -> { x e. CC | ( x - A ) e. B } = { x | E. y e. B x = ( y + A ) } )
Theorem	shftuz 11070*	A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> { x e. CC | ( x - A ) e. ( ZZ>= ` B ) } = ( ZZ>= ` ( B + A ) ) )
Theorem	shftfvalg 11071*	The value of the sequence shifter operation is a function on CC. A is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. CC /\ F e. V ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
Theorem	ovshftex 11072	Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ( F e. V /\ A e. CC ) -> ( F shift A ) e. _V )
Theorem	shftfibg 11073	Value of a fiber of the relation F. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )
Theorem	shftfval 11074*	The value of the sequence shifter operation is a function on CC. A is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
Theorem	shftdm 11075*	Domain of a relation shifted by A. The set on the right is more commonly notated as ( dom F + A ) (meaning add A to every element of dom F). (Contributed by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> dom ( F shift A ) = { x e. CC | ( x - A ) e. dom F } )
Theorem	shftfib 11076	Value of a fiber of the relation F. (Contributed by Mario Carneiro, 4-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )
Theorem	shftfn 11077*	Functionality and domain of a sequence shifted by A. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( ( F Fn B /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } )
Theorem	shftval 11078	Value of a sequence shifted by A. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )
Theorem	shftval2 11079	Value of a sequence shifted by A - B. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + C ) ) = ( F ` ( B + C ) ) )
Theorem	shftval3 11080	Value of a sequence shifted by A - B. (Contributed by NM, 20-Jul-2005.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift ( A - B ) ) ` A ) = ( F ` B ) )
Theorem	shftval4 11081	Value of a sequence shifted by -u A. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift -u A ) ` B ) = ( F ` ( A + B ) ) )
Theorem	shftval5 11082	Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` ( B + A ) ) = ( F ` B ) )
Theorem	shftf 11083*	Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C )
Theorem	2shfti 11084	Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) shift B ) = ( F shift ( A + B ) ) )
Theorem	shftidt2 11085	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( F shift 0 ) = ( F |` CC )
Theorem	shftidt 11086	Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> ( ( F shift 0 ) ` A ) = ( F ` A ) )
Theorem	shftcan1 11087	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift A ) shift -u A ) ` B ) = ( F ` B ) )
Theorem	shftcan2 11088	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift -u A ) shift A ) ` B ) = ( F ` B ) )
Theorem	shftvalg 11089	Value of a sequence shifted by A. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )
Theorem	shftval4g 11090	Value of a sequence shifted by -u A. (Contributed by Jim Kingdon, 19-Aug-2021.)
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift -u A ) ` B ) = ( F ` ( A + B ) ) )
Theorem	seq3shft 11091*	Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 17-Oct-2022.)
|- ( ph -> F e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` ( M - N ) ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> seq M ( .+ , ( F shift N ) ) = ( seq ( M - N ) ( .+ , F ) shift N ) )
4.8.2  Real and imaginary parts; conjugate
Syntax	ccj 11092	Extend class notation to include complex conjugate function.
class *
Syntax	cre 11093	Extend class notation to include real part of a complex number.
class Re
Syntax	cim 11094	Extend class notation to include imaginary part of a complex number.
class Im
Definition	df-cj 11095*	Define the complex conjugate function. See cjcli 11166 for its closure and cjval 11098 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
Definition	df-re 11096	Define a function whose value is the real part of a complex number. See reval 11102 for its value, recli 11164 for its closure, and replim 11112 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
Definition	df-im 11097	Define a function whose value is the imaginary part of a complex number. See imval 11103 for its value, imcli 11165 for its closure, and replim 11112 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
Theorem	cjval 11098*	The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( * ` A ) = ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
Theorem	cjth 11099	The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )
Theorem	cjf 11100	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
|- * : CC --> CC