Metamath Proof Explorer - mmtheorems49

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 4801-4900 - Page 49 of 58

Type	Label	Description
Statement
Theorem	absvalt 4801	The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133.
|- (A e. CC -> (abs` A) = (sqr` (A x. (*` A))))
Theorem	recl 4802	The real part of a complex number is real (closure law).
|- A e. CC   =>   |- (Re` A) e. RR
Theorem	imcl 4803	The imaginary part of a complex number is real (closure law).
|- A e. CC   =>   |- (Im` A) e. RR
Theorem	cjcl 4804	Closure law for complex conjugate.
|- A e. CC   =>   |- (*` A) e. CC
Theorem	replim 4805	Construct a complex number from its real and imaginary parts.
|- A e. CC   =>   |- A = ((Re` A) + ((Im` A) x. i))
Theorem	crre 4806	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132.
|- A e. RR   &   |- B e. RR   =>   |- (Re` (A + (B x. i))) = A
Theorem	crim 4807	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132.
|- A e. RR   &   |- B e. RR   =>   |- (Im` (A + (B x. i))) = B
Theorem	cjcj 4808	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	reim0 4809	The imaginary part of a real number is 0.
|- A e. CC   =>   |- (A e. RR <-> (Im` A) = 0)
Theorem	rere 4810	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133.
|- A e. CC   =>   |- (A e. RR <-> (Re` A) = A)
Theorem	cjre 4811	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	recj 4812	Real part of a complex conjugate.
|- A e. CC   =>   |- (Re` (*` A)) = (Re` A)
Theorem	imcj 4813	Imaginary part of a complex conjugate.
|- A e. CC   =>   |- (Im` (*` A)) = -u(Im` A)
Theorem	readd 4814	Real part distributes over addition.
|- A e. CC   &   |- B e. CC   =>   |- (Re` (A + B)) = ((Re` A) + (Re` B))
Theorem	imadd 4815	Imaginary part distributes over addition.
|- A e. CC   &   |- B e. CC   =>   |- (Im` (A + B)) = ((Im` A) + (Im` B))
Theorem	remul 4816	Real part of a product.
|- A e. CC   &   |- B e. CC   =>   |- (Re` (A x. B)) = (((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B)))
Theorem	immul 4817	Imaginary part of a product.
|- A e. CC   &   |- B e. CC   =>   |- (Im` (A x. B)) = (((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B)))
Theorem	cjadd 4818	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	cjmul 4819	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	ipcn 4820	Standard inner product on complex numbers.
|- A e. CC   &   |- B e. CC   =>   |- (Re` (A x. (*` B))) = (((Re` A) x. (Re` B)) + ((Im` A) x. (Im` B)))
Theorem	cjmulrcl 4821	A complex number times its conjugate is real.
|- A e. CC   =>   |- (A x. (*` A)) e. RR
Theorem	cjmulval 4822	A complex number times its conjugate.
|- A e. CC   =>   |- (A x. (*` A)) = (((Re` A)^2) + ((Im` A)^2))
Theorem	cjmulge0 4823	A complex number times its conjugate is nonnegative.
|- A e. CC   =>   |- 0 <_ (A x. (*` A))
Theorem	reneg 4824	Real part of negative.
|- A e. CC   =>   |- (Re` -uA) = -u(Re` A)
Theorem	negre 4825	The negative of a real is real.
|- A e. CC   =>   |- (-uA e. RR <-> A e. RR)
Theorem	imneg 4826	Imaginary part of negative.
|- A e. CC   =>   |- (Im` -uA) = -u(Im` A)
Theorem	cjneg 4827	Complex conjugate of negative.
|- A e. CC   =>   |- (*` -uA) = -u(*` A)
Theorem	addcj 4828	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	cjret 4829	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133.
|- (A e. RR -> (*` A) = A)
Theorem	cjcjt 4830	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 4831	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 4832	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	re0 4833	The real part of zero.
|- (Re` 0) = 0
Theorem	im0 4834	The imaginary part of zero.
|- (Im` 0) = 0
Theorem	cj0 4835	The conjugate of zero.
|- (*` 0) = 0
Theorem	absval2 4836	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	absvalsq 4837	Square of value of absolute value function.
|- A e. CC   =>   |- ((abs` A)^2) = (A x. (*` A))
Theorem	absvalsq2 4838	Square of value of absolute value function.
|- A e. CC   =>   |- ((abs` A)^2) = (((Re` A)^2) + ((Im` A)^2))
Theorem	abs00 4839	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	abscl 4840	Real closure of absolute value.
|- A e. CC   =>   |- (abs` A) e. RR
Theorem	absge0 4841	Absolute value is nonnegative.
|- A e. CC   =>   |- 0 <_ (abs` A)
Theorem	absgt0 4842	The absolute value of a non-zero number is positive. Remark of [Apostol] p. 363.
|- A e. CC   =>   |- (-. A = 0 <-> 0 < (abs` A))
Theorem	absneg 4843	Absolute value of negative.
|- A e. CC   =>   |- (abs` -uA) = (abs` A)
Theorem	abscj 4844	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 4845	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 4846	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	sqabsadd 4847	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	absclt 4848	Real closure of absolute value.
|- (A e. CC -> (abs` A) e. RR)
Theorem	absmult 4849	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	absid 4850	A nonnegative number is its own absolute value.
|- A e. RR   =>   |- (0 <_ A -> (abs` A) = A)
Theorem	absnid 4851	A negative number is the negative of its own absolute value.
|- A e. RR   =>   |- (A <_ 0 -> (abs` A) = -uA)
Theorem	leabs 4852	A real number is less than or equal to its absolute value.
|- A e. RR   =>   |- A <_ (abs` A)
Theorem	absor 4853	The absolute value of a real number is either that number or its negative.
|- A e. RR   =>   |- ((abs` A) = A \/ (abs` A) = -uA)
Theorem	absre 4854	Absolute value of a real number.
|- A e. RR   =>   |- (abs` A) = (sqr` (A^2))
Theorem	abslt 4855	Absolute value and 'less than' relation.
|- A e. RR   &   |- B e. RR   =>   |- ((abs` A) < B <-> (A < B /\ -uA < B))
Theorem	absle 4856	Absolute value and 'less than or equal to' relation.
|- A e. RR   &   |- B e. RR   =>   |- ((abs` A) <_ B <-> (A <_ B /\ -uA <_ B))
Theorem	absltt 4857	Absolute value and 'less than' relation.
|- ((A e. RR /\ B e. RR) -> ((abs` A) < B <-> (A < B /\ -uA < B)))
Theorem	releabs 4858	The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133.
|- A e. CC   =>   |- (Re` A) <_ (abs` A)
Theorem	abstri 4859	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133.
|- A e. CC   &   |- B e. CC   =>   |- (abs` (A + B)) <_ ((abs` A) + (abs` B))
Theorem	abs3dif 4860	Absolute value of differences around common element.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (abs` (A - B)) <_ ((abs` (A - C)) + (abs` (C - B)))
Theorem	abs3lem 4861	Lemma involving absolute value of differences.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. RR   =>   |- (((abs` (A - C)) < (D / 2) /\ (abs` (C - B)) < (D / 2)) -> (abs` (A - B)) < D)
Theorem	absidt 4862	A nonnegative number is its own absolute value.
|- (A e. RR -> (0 <_ A -> (abs` A) = A))
Theorem	absgt0t 4863	The absolute value of a non-zero number is positive.
|- (A e. CC -> (-. A = 0 <-> 0 < (abs` A)))
Theorem	abssubt 4864	Swapping order of subtraction doesn't change the absolute value.
|-