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	imcj 11401	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 11402	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 11403	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 11404	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 11405	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 11406	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 11407	Imaginary part of a division. Related to immul2 11406. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. RR /\ B # 0 ) -> ( Im ` ( A / B ) ) = ( ( Im ` A ) / B ) )
Theorem	cjre 11408	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 11409	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 11410	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 11411	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 11412	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 11413	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 11414	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 11415	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 11416	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 11417	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 11418	Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( * ` ( A - B ) ) = ( ( * ` A ) - ( * ` B ) ) )
Theorem	cjexp 11419	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( * ` ( A ^ N ) ) = ( ( * ` A ) ^ N ) )
Theorem	imval2 11420	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 11421	The real part of zero. (Contributed by NM, 27-Jul-1999.)
|- ( Re ` 0 ) = 0
Theorem	im0 11422	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|- ( Im ` 0 ) = 0
Theorem	re1 11423	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Re ` 1 ) = 1
Theorem	im1 11424	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Im ` 1 ) = 0
Theorem	rei 11425	The real part of _i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Re ` _i ) = 0
Theorem	imi 11426	The imaginary part of _i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Im ` _i ) = 1
Theorem	cj0 11427	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|- ( * ` 0 ) = 0
Theorem	cji 11428	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( * ` _i ) = -u _i
Theorem	cjreim 11429	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 11430	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 11431	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 11432	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) # ( * ` B ) <-> A # B ) )
Theorem	cjap0 11433	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 11434	A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 11433 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.)
|- ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )
Theorem	cjdivap 11435	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 11436*	The inverse to the canonical bijection from ( RR X. RR ) to CC from cnref1o 9858. (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 11437	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 11438	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 11439	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( * ` A ) e. CC
Theorem	replimi 11440	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 11441	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 11442	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 11443	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 11444	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 11445	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Re ` ( * ` A ) ) = ( Re ` A )
Theorem	imcji 11446	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Im ` ( * ` A ) ) = -u ( Im ` A )
Theorem	cjmulrcli 11447	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) e. RR
Theorem	cjmulvali 11448	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) )
Theorem	cjmulge0i 11449	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
|- A e. CC   =>    |- 0 <_ ( A x. ( * ` A ) )
Theorem	renegi 11450	Real part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Re ` -u A ) = -u ( Re ` A )
Theorem	imnegi 11451	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Im ` -u A ) = -u ( Im ` A )
Theorem	cjnegi 11452	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( * ` -u A ) = -u ( * ` A )
Theorem	addcji 11453	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( A + ( * ` A ) ) = ( 2 x. ( Re ` A ) )
Theorem	readdi 11454	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) )
Theorem	imaddi 11455	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) )
Theorem	remuli 11456	Real part of a product. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) )
Theorem	immuli 11457	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) )
Theorem	cjaddi 11458	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) )
Theorem	cjmuli 11459	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) )
Theorem	ipcni 11460	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( Im ` A ) x. ( Im ` B ) ) )
Theorem	cjdivapi 11461	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	crrei 11462	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( Re ` ( A + ( _i x. B ) ) ) = A
Theorem	crimi 11463	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( Im ` ( A + ( _i x. B ) ) ) = B
Theorem	recld 11464	The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` A ) e. RR )
Theorem	imcld 11465	The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` A ) e. RR )
Theorem	cjcld 11466	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) e. CC )
Theorem	replimd 11467	Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
Theorem	remimd 11468	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 Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
Theorem	cjcjd 11469	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` ( * ` A ) ) = A )
Theorem	reim0bd 11470	A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( Im ` A ) = 0 )   =>    |- ( ph -> A e. RR )
Theorem	rerebd 11471	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( Re ` A ) = A )   =>    |- ( ph -> A e. RR )
Theorem	cjrebd 11472	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( * ` A ) = A )   =>    |- ( ph -> A e. RR )
Theorem	cjne0d 11473	A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 11474 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( * ` A ) =/= 0 )
Theorem	cjap0d 11474	A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( * ` A ) # 0 )
Theorem	recjd 11475	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	imcjd 11476	Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
Theorem	cjmulrcld 11477	A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. ( * ` A ) ) e. RR )
Theorem	cjmulvald 11478	A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	cjmulge0d 11479	A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( A x. ( * ` A ) ) )
Theorem	renegd 11480	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` -u A ) = -u ( Re ` A ) )
Theorem	imnegd 11481	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` -u A ) = -u ( Im ` A ) )
Theorem	cjnegd 11482	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` -u A ) = -u ( * ` A ) )
Theorem	addcjd 11483	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + ( * ` A ) ) = ( 2 x. ( Re ` A ) ) )
Theorem	cjexpd 11484	Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( * ` ( A ^ N ) ) = ( ( * ` A ) ^ N ) )
Theorem	readdd 11485	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) )
Theorem	imaddd 11486	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
Theorem	resubd 11487	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A - B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )
Theorem	imsubd 11488	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
Theorem	remuld 11489	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
Theorem	immuld 11490	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
Theorem	cjaddd 11491	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) ) )
Theorem	cjmuld 11492	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) )
Theorem	ipcnd 11493	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( Im ` A ) x. ( Im ` B ) ) ) )
Theorem	cjdivapd 11494	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )
Theorem	rered 11495	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( Re ` A ) = A )
Theorem	reim0d 11496	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( Im ` A ) = 0 )
Theorem	cjred 11497	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( * ` A ) = A )
Theorem	remul2d 11498	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A x. B ) ) = ( A x. ( Re ` B ) ) )
Theorem	immul2d 11499	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A x. B ) ) = ( A x. ( Im ` B ) ) )
Theorem	redivapd 11500	Real part of a division. Related to remul2 11399. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( Re ` ( B / A ) ) = ( ( Re ` B ) / A ) )