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	wrdsymb0 11001	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 11002	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 11003	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 11004	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 11005	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 11006*	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 11007	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 11008	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 11009*	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 11010*	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 11011	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 11012	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 11013	Extend class notation with the Last Symbol of a word.
class lastS
Definition	df-lsw 11014	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 11015	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 11016	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 11017	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
|- (lastS ` (/) ) = (/)
Theorem	lsw1 11018	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 11019	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 11020	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 11021	Syntax for the concatenation operator.
class ++
Definition	df-concat 11022*	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 11023*	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 11024	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 11025	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 11026	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 11027	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 11028	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 11029	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 11030	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 11031	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 11032	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 11033	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 11034	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 11035	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 11036	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 11037	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 11038	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 11039	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 11040	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 11041	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
|- ( (/) ++ (/) ) = (/)
Theorem	lswccatn0lsw 11042	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 11043	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 11044	Extend class notation with function shifter.
class shift
Definition	df-shft 11045*	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 11055 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 11046*	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 11047*	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 11048*	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 11049	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 11050	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 11051*	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 11052*	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 11053	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 11054*	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 11055	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 11056	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 11057	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 11058	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 11059	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 11060*	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 11061	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 11062	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( F shift 0 ) = ( F |` CC )
Theorem	shftidt 11063	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 11064	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 11065	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 11066	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 11067	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 11068*	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 11069	Extend class notation to include complex conjugate function.
class *
Syntax	cre 11070	Extend class notation to include real part of a complex number.
class Re
Syntax	cim 11071	Extend class notation to include imaginary part of a complex number.
class Im
Definition	df-cj 11072*	Define the complex conjugate function. See cjcli 11143 for its closure and cjval 11075 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 11073	Define a function whose value is the real part of a complex number. See reval 11079 for its value, recli 11141 for its closure, and replim 11089 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
Definition	df-im 11074	Define a function whose value is the imaginary part of a complex number. See imval 11080 for its value, imcli 11142 for its closure, and replim 11089 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
Theorem	cjval 11075*	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 11076	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 11077	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
|- * : CC --> CC
Theorem	cjcl 11078	The conjugate of a complex number is a complex number (closure law). (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( * ` A ) e. CC )
Theorem	reval 11079	The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( Re ` A ) = ( ( A + ( * ` A ) ) / 2 ) )
Theorem	imval 11080	The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( Im ` A ) = ( Re ` ( A / _i ) ) )
Theorem	imre 11081	The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )
Theorem	reim 11082	The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
Theorem	recl 11083	The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( Re ` A ) e. RR )
Theorem	imcl 11084	The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- ( A e. CC -> ( Im ` A ) e. RR )
Theorem	ref 11085	Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- Re : CC --> RR
Theorem	imf 11086	Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|- Im : CC --> RR
Theorem	crre 11087	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( ( A e. RR /\ B e. RR ) -> ( Re ` ( A + ( _i x. B ) ) ) = A )
Theorem	crim 11088	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( ( A e. RR /\ B e. RR ) -> ( Im ` ( A + ( _i x. B ) ) ) = B )
Theorem	replim 11089	Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
Theorem	remim 11090	Value of the conjugate of a complex number. The value is the real part minus _i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( A e. CC -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
Theorem	reim0 11091	The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( A e. RR -> ( Im ` A ) = 0 )
Theorem	reim0b 11092	A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
|- ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
Theorem	rereb 11093	A number is real iff it equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 20-Aug-2008.)
|- ( A e. CC -> ( A e. RR <-> ( Re ` A ) = A ) )
Theorem	mulreap 11094	A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. RR /\ B # 0 ) -> ( A e. RR <-> ( B x. A ) e. RR ) )
Theorem	rere 11095	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( A e. RR -> ( Re ` A ) = A )
Theorem	cjreb 11096	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( A e. RR <-> ( * ` A ) = A ) )
Theorem	recj 11097	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	reneg 11098	Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( Re ` -u A ) = -u ( Re ` A ) )
Theorem	readd 11099	Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) )
Theorem	resub 11100	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A - B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )