mmtheorems69 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10789

Statement List for Metamath Proof Explorer - 6801-6900 - Page 69 of 108

Type	Label	Description
Statement
Theorem	imneg 6801	Imaginary part of negative.
|- A e. CC   =>   |- (Im` -uA) = -u(Im` A)
Theorem	cjneg 6802	Complex conjugate of negative.
|- A e. CC   =>   |- (*` -uA) = -u(*` A)
Theorem	addcj 6803	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133.
|- A e. CC   =>   |- (A + (*` A)) = (2 x. (Re` A))
Theorem	reret 6804	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	cjrebt 6805	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133.
|- (A e. CC -> (A e. RR <-> (*` A) = A))
Theorem	cjmulrclt 6806	A complex number times its conjugate is real.
|- (A e. CC -> (A x. (*` A)) e. RR)
Theorem	cjmulvalt 6807	A complex number times its conjugate.
|- (A e. CC -> (A x. (*` A)) = (((Re` A)^2) + ((Im` A)^2)))
Theorem	cjmulge0t 6808	A complex number times its conjugate is nonnegative.
|- (A e. CC -> 0 <_ (A x. (*` A)))
Theorem	renegt 6809	Real part of negative.
|- (A e. CC -> (Re` -uA) = -u(Re` A))
Theorem	readdt 6810	Real part distributes over addition.
|- ((A e. CC /\ B e. CC) -> (Re` (A + B)) = ((Re` A) + (Re` B)))
Theorem	resubt 6811	Real part distributes over subtraction.
|- ((A e. CC /\ B e. CC) -> (Re` (A - B)) = ((Re` A) - (Re` B)))
Theorem	imnegt 6812	The imaginary part of a negative number.
|- (A e. CC -> (Im` -uA) = -u(Im` A))
Theorem	imaddt 6813	Imaginary part distributes over addition.
|- ((A e. CC /\ B e. CC) -> (Im` (A + B)) = ((Im` A) + (Im` B)))
Theorem	imsubt 6814	Imaginary part distributes over subtraction.
|- ((A e. CC /\ B e. CC) -> (Im` (A - B)) = ((Im` A) - (Im` B)))
Theorem	cjret 6815	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133.
|- (A e. RR -> (*` A) = A)
Theorem	cjcjt 6816	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133.
|- (A e. CC -> (*` (*` A)) = A)
Theorem	cjaddt 6817	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133.
|- ((A e. CC /\ B e. CC) -> (*` (A + B)) = ((*` A) + (*` B)))
Theorem	cjmult 6818	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133.
|- ((A e. CC /\ B e. CC) -> (*` (A x. B)) = ((*` A) x. (*` B)))
Theorem	cjnegt 6819	Complex conjugate of negative.
|- (A e. CC -> (*` -uA) = -u(*` A))
Theorem	addcjt 6820	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133.
|- (A e. CC -> (A + (*` A)) = (2 x. (Re` A)))
Theorem	cjsubt 6821	Complex conjugate distributes over subtraction.
|- ((A e. CC /\ B e. CC) -> (*` (A - B)) = ((*` A) - (*` B)))
Theorem	cjexpt 6822	Complex conjugate of natural number exponentiation.
|- ((A e. CC /\ N e. NN0) -> (*` (A^N)) = ((*` A)^N))
Theorem	recjt 6823	The real part of a number in terms of complex conjugate.
|- (A e. CC -> (Re` A) = ((A + (*` A)) / 2))
Theorem	imcjt 6824	The imaginary part of a number in terms of complex conjugate.
|- (A e. CC -> (Im` A) = ((A - (*` A)) / (2 x. i)))
Theorem	re0 6825	The real part of zero.
|- (Re` 0) = 0
Theorem	im0 6826	The imaginary part of zero.
|- (Im` 0) = 0
Theorem	re1 6827	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Re` 1) = 1
Theorem	im1 6828	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Im` 1) = 0
Theorem	rei 6829	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Re` i) = 0
Theorem	imi 6830	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Im` i) = 1
Theorem	cj0 6831	The conjugate of zero.
|- (*` 0) = 0
Theorem	cji 6832	The complex conjugate of the imaginary unit.
|- (*` i) = -ui
Theorem	cjreimt 6833	The conjugate of a representation of a complex number in terms of real and imaginary parts.
|- ((A e. RR /\ B e. RR) -> (*` (A + (i x. B))) = (A - (i x. B)))
Theorem	cjreim2t 6834	The conjugate of the representation of a complex number in terms of real and imaginary parts.
|- ((A e. RR /\ B e. RR) -> (*` (A - (i x. B))) = (A + (i x. B)))
Theorem	cj11t 6835	Complex conjugate is a one-to-one function.
|- ((A e. CC /\ B e. CC) -> ((*` A) = (*` B) <-> A = B))
Theorem	cjne0t 6836	A number is non-zero iff its complex conjugate is non-zero.
|- (A e. CC -> (A =/= 0 <-> (*` A) =/= 0))
Theorem	absnegt 6837	Absolute value of negative.
|- (A e. CC -> (abs` -uA) = (abs` A))
Theorem	absclt 6838	Real closure of absolute value.
|- (A e. CC -> (abs` A) e. RR)
Theorem	abscjt 6839	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133.
|- (A e. CC -> (abs` (*` A)) = (abs` A))
Theorem	absvalsqt 6840	Square of value of absolute value function.
|- (A e. CC -> ((abs` A)^2) = (A x. (*` A)))
Theorem	absvalsq2t 6841	Square of value of absolute value function.
|- (A e. CC -> ((abs` A)^2) = (((Re` A)^2) + ((Im` A)^2)))
Theorem	absvalsq 6842	Square of value of absolute value function.
|- A e. CC   =>   |- ((abs` A)^2) = (A x. (*` A))
Theorem	absvalsq2 6843	Square of value of absolute value function.
|- A e. CC   =>   |- ((abs` A)^2) = (((Re` A)^2) + ((Im` A)^2))
Theorem	abscl 6844	Real closure of absolute value.
|- A e. CC   =>   |- (abs` A) e. RR
Theorem	absge0 6845	Absolute value is nonnegative.
|- A e. CC   =>   |- 0 <_ (abs` A)
Theorem	absval2 6846	Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
|- A e. CC   =>   |- (abs` A) = (sqr` (((Re` A)^2) + ((Im` A)^2)))
Theorem	abs00 6847	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133.
|- A e. CC   =>   |- ((abs` A) = 0 <-> A = 0)
Theorem	absgt0 6848	The absolute value of a non-zero number is positive. Remark in [Apostol] p. 363.
|- A e. CC   =>   |- (A =/= 0 <-> 0 < (abs` A))
Theorem	absneg 6849	Absolute value of negative.
|- A e. CC   =>   |- (abs` -uA) = (abs` A)
Theorem	abscj 6850	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133.
|- A e. CC   =>   |- (abs` (*` A)) = (abs` A)
Theorem	abssub 6851	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363.
|- A e. CC   &   |- B e. CC   =>   |- (abs` (A - B)) = (abs` (B - A))
Theorem	absmul 6852	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133.
|- A e. CC   &   |- B e. CC   =>   |- (abs` (A x. B)) = ((abs` A) x. (abs` B))
Theorem	sqabsaddt 6853	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133.
|- ((A e. CC /\ B e. CC) -> ((abs` (A + B))^2) = ((((abs` A)^2) + ((abs` B)^2)) + (2 x. (Re` (A x. (*` B))))))
Theorem	sqabssubt 6854	Square of absolute value of difference.
|- ((A e. CC /\ B e. CC) -> ((abs` (A - B))^2) = ((((abs` A)^2) + ((abs` B)^2)) - (2 x. (Re` (A x. (*` B))))))
Theorem	sqabsadd 6855	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133.
|- A e. CC   &   |- B e. CC   =>   |- ((abs` (A + B))^2) = ((((abs` A)^2) + ((abs` B)^2)) + (2 x. (Re` (A x. (*` B)))))
Theorem	sqabssub 6856	Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.)
|- A e. CC   &   |- B e. CC   =>   |- ((abs` (A - B))^2) = ((((abs` A)^2) + ((abs` B)^2)) - (2 x. (Re` (A x. (*` B)))))
Theorem	absval2t 6857	Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
|- (A e. CC -> (abs` A) = (sqr` (((Re` A)^2) + ((Im` A)^2))))
Theorem	abs00t 6858	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133.
|- (A e. CC -> ((abs` A) = 0 <-> A = 0))
Theorem	absge0t 6859	Absolute value is nonnegative.
|- (A e. CC -> 0 <_ (abs` A))
Theorem	absrpclt 6860	The absolute value of a nonzero number is a positive real. (Contributed by FL, 27-Dec-2007.)
|- ((A e. CC /\ A =/= 0) -> (abs` A) e. RR+)
Theorem	absreimsqt 6861	Square of the absolute value of a number that has been decomposed into real and imaginary parts.
|- ((A e. RR /\ B