P. 115 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11401-11500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	s3eqd 11401	Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   =>    |- ( ph -> <" A B C "> = <" N O P "> )
Theorem	s4eqd 11402	Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   =>    |- ( ph -> <" A B C D "> = <" N O P Q "> )
Theorem	s5eqd 11403	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   =>    |- ( ph -> <" A B C D E "> = <" N O P Q R "> )
Theorem	s6eqd 11404	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   =>    |- ( ph -> <" A B C D E F "> = <" N O P Q R S "> )
Theorem	s7eqd 11405	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   =>    |- ( ph -> <" A B C D E F G "> = <" N O P Q R S T "> )
Theorem	s8eqd 11406	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   &    |- ( ph -> H = U )   =>    |- ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )
Theorem	s3eq2 11407	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
|- ( B = D -> <" A B C "> = <" A D C "> )
Theorem	s2cld 11408	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> <" A B "> e. Word X )
Theorem	s3cld 11409	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   =>    |- ( ph -> <" A B C "> e. Word X )
Theorem	s4cld 11410	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   =>    |- ( ph -> <" A B C D "> e. Word X )
Theorem	s5cld 11411	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   =>    |- ( ph -> <" A B C D E "> e. Word X )
Theorem	s6cld 11412	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   =>    |- ( ph -> <" A B C D E F "> e. Word X )
Theorem	s7cld 11413	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   =>    |- ( ph -> <" A B C D E F G "> e. Word X )
Theorem	s8cld 11414	A length 8 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. X )   =>    |- ( ph -> <" A B C D E F G H "> e. Word X )
Theorem	s2cl 11415	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X ) -> <" A B "> e. Word X )
Theorem	s3cl 11416	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X /\ C e. X ) -> <" A B C "> e. Word X )
Theorem	s2fv0g 11417	Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> ( <" A B "> ` 0 ) = A )
Theorem	s2fv1g 11418	Extract the second symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> ( <" A B "> ` 1 ) = B )
Theorem	s2leng 11419	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> (♯ ` <" A B "> ) = 2 )
Theorem	s2dmg 11420	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
|- ( ( A e. V /\ B e. W ) -> dom <" A B "> = { 0 , 1 } )
Theorem	s3fv0g 11421	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 0 ) = A )
Theorem	s3fv1g 11422	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 1 ) = B )
Theorem	s3fv2g 11423	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 2 ) = C )
Theorem	s1s2d 11424	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> <" A B C "> = ( <" A "> ++ <" B C "> ) )
Theorem	s1s3d 11425	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> <" A B C D "> = ( <" A "> ++ <" B C D "> ) )
Theorem	s1s4d 11426	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   =>    |- ( ph -> <" A B C D E "> = ( <" A "> ++ <" B C D E "> ) )
Theorem	s1s5d 11427	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   =>    |- ( ph -> <" A B C D E F "> = ( <" A "> ++ <" B C D E F "> ) )
Theorem	s1s6d 11428	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A "> ++ <" B C D E F G "> ) )
Theorem	s1s7d 11429	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   &    |- ( ph -> H e. R )   =>    |- ( ph -> <" A B C D E F G H "> = ( <" A "> ++ <" B C D E F G H "> ) )
Theorem	s2s2d 11430	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> <" A B C D "> = ( <" A B "> ++ <" C D "> ) )
Theorem	s4s2d 11431	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   =>    |- ( ph -> <" A B C D E F "> = ( <" A B C D "> ++ <" E F "> ) )
Theorem	s4s3d 11432	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> ) )
Theorem	s3s4d 11433	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C "> ++ <" D E F G "> ) )
Theorem	s2s5d 11434	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B "> ++ <" C D E F G "> ) )
Theorem	s5s2d 11435	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C D E "> ++ <" F G "> ) )
Theorem	s4s4d 11436	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   &    |- ( ph -> H e. R )   =>    |- ( ph -> <" A B C D E F G H "> = ( <" A B C D "> ++ <" E F G H "> ) )
4.8  Elementary real and complex functions
4.8.1  The "shift" operation
Syntax	cshi 11437	Extend class notation with function shifter.
class shift
Definition	df-shft 11438*	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 11448 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 11439*	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 11440*	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 11441*	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 11442	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 11443	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 11444*	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 11445*	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 11446	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 11447*	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 11448	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 11449	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 11450	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 11451	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 11452	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 11453*	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 11454	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 11455	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( F shift 0 ) = ( F |` CC )
Theorem	shftidt 11456	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 11457	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 11458	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 11459	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 11460	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 11461*	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 11462	Extend class notation to include complex conjugate function.
class *
Syntax	cre 11463	Extend class notation to include real part of a complex number.
class Re
Syntax	cim 11464	Extend class notation to include imaginary part of a complex number.
class Im
Definition	df-cj 11465*	Define the complex conjugate function. See cjcli 11536 for its closure and cjval 11468 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 11466	Define a function whose value is the real part of a complex number. See reval 11472 for its value, recli 11534 for its closure, and replim 11482 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
Definition	df-im 11467	Define a function whose value is the imaginary part of a complex number. See imval 11473 for its value, imcli 11535 for its closure, and replim 11482 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
Theorem	cjval 11468*	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 11469	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 11470	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
|- * : CC --> CC
Theorem	cjcl 11471	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 11472	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 11473	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 11474	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 11475	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 11476	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 11477	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 11478	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 11479	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 11480	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 11481	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 11482	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 11483	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 11484	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 11485	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 11486	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 11487	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 11488	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 11489	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 11490	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	reneg 11491	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 11492	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 11493	Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A - B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )
Theorem	remullem 11494	Lemma for remul 11495, immul 11502, and cjmul 11508. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) /\ ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) /\ ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) ) )
Theorem	remul 11495	Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
Theorem	remul2 11496	Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR /\ B e. CC ) -> ( Re ` ( A x. B ) ) = ( A x. ( Re ` B ) ) )
Theorem	redivap 11497	Real part of a division. Related to remul2 11496. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. RR /\ B # 0 ) -> ( Re ` ( A / B ) ) = ( ( Re ` A ) / B ) )
Theorem	imcj 11498	Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
Theorem	imneg 11499	The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( Im ` -u A ) = -u ( Im ` A ) )
Theorem	imadd 11500	Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )