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	shftfib 11401	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 11402*	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 11403	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 11404	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 11405	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 11406	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 11407	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 11408*	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 11409	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 11410	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( F shift 0 ) = ( F |` CC )
Theorem	shftidt 11411	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 11412	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 11413	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 11414	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 11415	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 11416*	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 11417	Extend class notation to include complex conjugate function.
class *
Syntax	cre 11418	Extend class notation to include real part of a complex number.
class Re
Syntax	cim 11419	Extend class notation to include imaginary part of a complex number.
class Im
Definition	df-cj 11420*	Define the complex conjugate function. See cjcli 11491 for its closure and cjval 11423 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 11421	Define a function whose value is the real part of a complex number. See reval 11427 for its value, recli 11489 for its closure, and replim 11437 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
Definition	df-im 11422	Define a function whose value is the imaginary part of a complex number. See imval 11428 for its value, imcli 11490 for its closure, and replim 11437 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
Theorem	cjval 11423*	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 11424	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 11425	Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
|- * : CC --> CC
Theorem	cjcl 11426	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 11427	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 11428	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 11429	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 11430	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 11431	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 11432	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 11433	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 11434	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 11435	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 11436	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 11437	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 11438	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 11439	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 11440	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 11441	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 11442	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 11443	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 11444	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 11445	Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	reneg 11446	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 11447	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 11448	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 11449	Lemma for remul 11450, immul 11457, and cjmul 11463. (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 11450	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 11451	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 11452	Real part of a division. Related to remul2 11451. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. RR /\ B # 0 ) -> ( Re ` ( A / B ) ) = ( ( Re ` A ) / B ) )
Theorem	imcj 11453	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 11454	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 11455	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 ) ) )
Theorem	imsub 11456	Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
Theorem	immul 11457	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
Theorem	immul2 11458	Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( A x. ( Im ` B ) ) )
Theorem	imdivap 11459	Imaginary part of a division. Related to immul2 11458. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. RR /\ B # 0 ) -> ( Im ` ( A / B ) ) = ( ( Im ` A ) / B ) )
Theorem	cjre 11460	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.)
|- ( A e. RR -> ( * ` A ) = A )
Theorem	cjcj 11461	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( * ` ( * ` A ) ) = A )
Theorem	cjadd 11462	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) ) )
Theorem	cjmul 11463	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) )
Theorem	ipcnval 11464	Standard inner product on complex numbers. (Contributed by NM, 29-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	cjmulrcl 11465	A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( A x. ( * ` A ) ) e. RR )
Theorem	cjmulval 11466	A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	cjmulge0 11467	A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> 0 <_ ( A x. ( * ` A ) ) )
Theorem	cjneg 11468	Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( * ` -u A ) = -u ( * ` A ) )
Theorem	addcj 11469	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( A + ( * ` A ) ) = ( 2 x. ( Re ` A ) ) )
Theorem	cjsub 11470	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( * ` ( A - B ) ) = ( ( * ` A ) - ( * ` B ) ) )
Theorem	cjexp 11471	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( * ` ( A ^ N ) ) = ( ( * ` A ) ^ N ) )
Theorem	imval2 11472	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
|- ( A e. CC -> ( Im ` A ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )
Theorem	re0 11473	The real part of zero. (Contributed by NM, 27-Jul-1999.)
|- ( Re ` 0 ) = 0
Theorem	im0 11474	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|- ( Im ` 0 ) = 0
Theorem	re1 11475	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Re ` 1 ) = 1
Theorem	im1 11476	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Im ` 1 ) = 0
Theorem	rei 11477	The real part of _i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Re ` _i ) = 0
Theorem	imi 11478	The imaginary part of _i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Im ` _i ) = 1
Theorem	cj0 11479	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|- ( * ` 0 ) = 0
Theorem	cji 11480	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( * ` _i ) = -u _i
Theorem	cjreim 11481	The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( * ` ( A + ( _i x. B ) ) ) = ( A - ( _i x. B ) ) )
Theorem	cjreim2 11482	The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( * ` ( A - ( _i x. B ) ) ) = ( A + ( _i x. B ) ) )
Theorem	cj11 11483	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) = ( * ` B ) <-> A = B ) )
Theorem	cjap 11484	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) # ( * ` B ) <-> A # B ) )
Theorem	cjap0 11485	A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( A e. CC -> ( A # 0 <-> ( * ` A ) # 0 ) )
Theorem	cjne0 11486	A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 11485 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.)
|- ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )
Theorem	cjdivap 11487	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )
Theorem	cnrecnv 11488*	The inverse to the canonical bijection from ( RR X. RR ) to CC from cnref1o 9885. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )   =>    |- `' F = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )
Theorem	recli 11489	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( Re ` A ) e. RR
Theorem	imcli 11490	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( Im ` A ) e. RR
Theorem	cjcli 11491	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( * ` A ) e. CC
Theorem	replimi 11492	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   =>    |- A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) )
Theorem	cjcji 11493	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( * ` ( * ` A ) ) = A
Theorem	reim0bi 11494	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>    |- ( A e. RR <-> ( Im ` A ) = 0 )
Theorem	rerebi 11495	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
|- A e. CC   =>    |- ( A e. RR <-> ( Re ` A ) = A )
Theorem	cjrebi 11496	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)
|- A e. CC   =>    |- ( A e. RR <-> ( * ` A ) = A )
Theorem	recji 11497	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Re ` ( * ` A ) ) = ( Re ` A )
Theorem	imcji 11498	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Im ` ( * ` A ) ) = -u ( Im ` A )
Theorem	cjmulrcli 11499	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) e. RR
Theorem	cjmulvali 11500	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) )