mmtheorems71 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 7001-7100 - Page 71 of 123

Type	Label	Description
Statement
Theorem	cjreb 7001	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	cjmulrcl 7002	A complex number times its conjugate is real.
|- (A e. CC -> (A x. (*` A)) e. RR)
Theorem	cjmulval 7003	A complex number times its conjugate.
|- (A e. CC -> (A x. (*` A)) = (((Re` A)^2) + ((Im` A)^2)))
Theorem	cjmulge0 7004	A complex number times its conjugate is nonnegative.
|- (A e. CC -> 0 <_ (A x. (*` A)))
Theorem	reneg 7005	Real part of negative.
|- (A e. CC -> (Re` -uA) = -u(Re` A))
Theorem	readd 7006	Real part distributes over addition.
|- ((A e. CC /\ B e. CC) -> (Re` (A + B)) = ((Re` A) + (Re` B)))
Theorem	resub 7007	Real part distributes over subtraction.
|- ((A e. CC /\ B e. CC) -> (Re` (A - B)) = ((Re` A) - (Re` B)))
Theorem	imneg 7008	The imaginary part of a negative number.
|- (A e. CC -> (Im` -uA) = -u(Im` A))
Theorem	imadd 7009	Imaginary part distributes over addition.
|- ((A e. CC /\ B e. CC) -> (Im` (A + B)) = ((Im` A) + (Im` B)))
Theorem	imsub 7010	Imaginary part distributes over subtraction.
|- ((A e. CC /\ B e. CC) -> (Im` (A - B)) = ((Im` A) - (Im` B)))
Theorem	cjre 7011	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133.
|- (A e. RR -> (*` A) = A)
Theorem	cjcj 7012	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	cjadd 7013	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 7014	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	cjneg 7015	Complex conjugate of negative.
|- (A e. CC -> (*` -uA) = -u(*` A))
Theorem	addcj 7016	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	cjsub 7017	Complex conjugate distributes over subtraction.
|- ((A e. CC /\ B e. CC) -> (*` (A - B)) = ((*` A) - (*` B)))
Theorem	cjexp 7018	Complex conjugate of natural number exponentiation.
|- ((A e. CC /\ N e. NN0) -> (*` (A^N)) = ((*` A)^N))
Theorem	recj 7019	The real part of a number in terms of complex conjugate.
|- (A e. CC -> (Re` A) = ((A + (*` A)) / 2))
Theorem	imcj 7020	The imaginary part of a number in terms of complex conjugate.
|- (A e. CC -> (Im` A) = ((A - (*` A)) / (2 x. i)))
Theorem	re0 7021	The real part of zero.
|- (Re` 0) = 0
Theorem	im0 7022	The imaginary part of zero.
|- (Im` 0) = 0
Theorem	re1 7023	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Re` 1) = 1
Theorem	im1 7024	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Im` 1) = 0
Theorem	rei 7025	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Re` i) = 0
Theorem	imi 7026	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- (Im` i) = 1
Theorem	cj0 7027	The conjugate of zero.
|- (*` 0) = 0
Theorem	cji 7028	The complex conjugate of the imaginary unit.
|- (*` i) = -ui
Theorem	cjreim 7029	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	cjreim2 7030	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	cj11 7031	Complex conjugate is a one-to-one function. (Proof shortened by Eric Schmidt, 2-Jul-2009. Previous version is cj11OLD 7032.)
|- ((A e. CC /\ B e. CC) -> ((*` A) = (*` B) <-> A = B))
Theorem	cj11OLD 7032	Complex conjugate is a one-to-one function.
|- ((A e. CC /\ B e. CC) -> ((*` A) = (*` B) <-> A = B))
Theorem	cjne0 7033	A number is non-zero iff its complex conjugate is non-zero.
|- (A e. CC -> (A =/= 0 <-> (*` A) =/= 0))
Theorem	absneg 7034	Absolute value of negative.
|- (A e. CC -> (abs` -uA) = (abs` A))
Theorem	abscl 7035	Real closure of absolute value.
|- (A e. CC -> (abs` A) e. RR)
Theorem	abscj 7036	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	absvalsq 7037	Square of value of absolute value function.
|- (A e. CC -> ((abs` A)^2) = (A x. (*` A)))
Theorem	absvalsq2 7038	Square of value of absolute value function.
|- (A e. CC -> ((abs` A)^2) = (((Re` A)^2) + ((Im` A)^2)))
Theorem	absvalsqi 7039	Square of value of absolute value function.
|- A e. CC   =>   |- ((abs` A)^2) = (A x. (*` A))
Theorem	absvalsq2i 7040	Square of value of absolute value function.
|- A e. CC   =>   |- ((abs` A)^2) = (((Re` A)^2) + ((Im` A)^2))
Theorem	abscli 7041	Real closure of absolute value.
|- A e. CC   =>   |- (abs` A) e. RR
Theorem	absge0i 7042	Absolute value is nonnegative.
|- A e. CC   =>   |- 0 <_ (abs` A)
Theorem	absval2i 7043	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	abs00i 7044	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	absgt0i 7045	The absolute value of a non-zero number is positive. Remark in [Apostol] p. 363.
|- A e. CC   =>   |- (A =/= 0 <-> 0 < (abs` A))
Theorem	absnegi 7046	Absolute value of negative.
|- A e. CC   =>   |- (abs` -uA) = (abs` A)
Theorem	abscji 7047	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	abssubi 7048	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	absmuli 7049	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 7050	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 7051	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	sqabsaddi 7052	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	sqabssubi 7053	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	absval2 7054	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 7055	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	absge0 7056	Absolute value is nonnegative.
|- (A e. CC -> 0 <_ (abs` A))
Theorem	absrpcl 7057	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	absreimsq 7058	Square of the absolute value of a number that has been decomposed into real and imaginary parts.
|- ((A e. RR /\ B e. RR) -> ((abs` (A + (i x. B)))^2) = ((A^2) + (B^2)))
Theorem	absreim 7059	Absolute value of a number that has been decomposed into real and imaginary parts.
|- ((A e. RR /\ B e. RR) -> (abs` (A + (i x. B))) = (sqr` ((A^2) + (B^2))))
Theorem	absmul 7060	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	absdivzi 7061	Absolute value distributes over division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (abs` (A / B)) = ((abs` A) / (abs` B)))
Theorem	absdiv 7062	Absolute value distributes over division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (abs` (A / B)) = ((abs` A) / (abs` B)))
Theorem	absidi 7063	A nonnegative number is its own absolute value.
|- A e. RR   =>   |- (0 <_ A -> (abs` A) = A)
Theorem	absid 7064	A nonnegative number is its own absolute value.
|- ((A e. RR /\ 0 <_ A) -> (abs` A) = A)
Theorem	absnid 7065	A negative number is the negative of its own absolute value.
|- ((A e. RR /\ A <_ 0) -> (abs` A) = -uA)
Theorem	leabs 7066	A real number is less than or equal to its absolute value.
|- (A e. RR -> A <_ (abs` A))
Theorem	absor 7067	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 7068	Absolute value of a real number.
|- (A e. RR -> (abs` A) = (sqr` (A^2)))
Theorem	absresq 7069	Square of the absolute value of a real number.
|- (A e. RR -> ((abs` A)^2) = (A^2))
Theorem	absexp 7070	Absolute value of natural number exponentiation.
|- ((A e. CC /\ N e. NN0) -> (abs` (A^N)) = ((abs` A)^N))
Theorem	sqabs 7071	The squares of two reals are equal iff their absolute values are equal.
|- ((A e. RR /\ B e. RR) -> ((A^2) = (B^2) <-> (abs` A) = (abs` B)))
Theorem	absrele 7072	The absolute value of a complex number is greater than or equal to the absolute value of its real part.
|- (A e. CC -> (abs` (Re` A)) <_ (abs` A))
Theorem	absimle 7073	The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part.
|- (A e. CC -> (abs` (Im` A)) <_ (abs` A))
Theorem	absnidi 7074	A negative number is the negative of its own absolute value.
|- A e. RR   =>   |- (A <_ 0 -> (abs` A) = -uA)
Theorem	leabsi 7075	A real number is less than or equal to its absolute value.
|- A e. RR   =>   |- A <_ (abs` A)
Theorem	absori 7076	The absolute value of a real number is either that number or its negative.
|- A e. RR   =>   |- ((abs` A) = A \/ (abs` A) = -uA)
Theorem	absrei 7077	Absolute value of a real number.
|- A e. RR   =>   |- (abs` A) = (sqr` (A^2))
Theorem	abslti 7078	Absolute value and 'less than' relation.
|- A e. RR   &   |- B e. RR   =>   |- ((abs` A) < B <-> (-uB < A /\ A < B))
Theorem	abslei 7079	Absolute value and 'less than or equal to' relation.
|- A e. RR   &   |- B e. RR   =>   |- ((abs` A) <_ B <-> (-uB <_ A /\ A <_ B))
Theorem	abs0 7080	The absolute value of 0.
|- (abs` 0) = 0
Theorem	absi 7081	The absolute value of the imaginary unit.
|- (abs` i) = 1
Theorem	nn0abscl 7082	The absolute value of an integer is a nonnegative integer.
|- (A e. ZZ -> (abs` A) e. NN0)
Theorem	abslt 7083	Absolute value and 'less than' relation.
|- ((A e. RR /\ B e. RR) -> ((abs` A) < B <-> (-uB < A /\ A < B)))
Theorem	absle 7084	Absolute value and 'less than or equal to' relation.
|- ((A e. RR /\ B e. RR) -> ((abs` A) <_ B <-> (-uB <_ A /\ A <_ B)))
Theorem	abssubne0 7085	If the absolute value of a complex number is less than a real, its difference from the real is nonzero.
|- ((A e. CC /\ B e. RR /\ (abs` A) < B) -> (B - A) =/= 0)
Theorem	absdiflt 7086	The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((abs` (A - B)) < C <-> ((B - C) < A /\ A < (B + C))))
Theorem	absdifle 7087	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((abs` (A - B)) <_ C <-> ((B - C) <_ A /\ A <_ (B + C))))
Theorem	lenegsq 7088	Comparison to a nonnegative number based on comparison to squares.
|- ((A e. RR /\ B e. RR /\ 0 <_ B) -> ((A <_ B /\ -uA <_ B) <-> (A^2) <_ (B^2)))
Theorem	releabs 7089	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	recvalzi 7090	Reciprocal expressed with a real denominator.
|- A e. CC   =>   |- (A =/= 0 -> (1 / A) = ((*` A) / ((abs` A)^2)))
Theorem	cjdivi 7091	Complex conjugate distributes over division.
|- A e. CC   &   |- B e. CC   =>   |- (B =/= 0 -> (*` (A / B)) = ((*` A) / (*` B)))
Theorem	cjdiv 7092	Complex conjugate distributes over division.
|- ((A e. CC /\ B e. CC /\ B =/= 0) -> (*` (A / B)) = ((*` A) / (*` B)))
Theorem	releabsi 7093	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	abstrii 7094	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	absidm 7095	The absolute value function is idempotent.
|- (A e. CC -> (abs` (abs` A)) = (abs` A))
Theorem	absgt0 7096	The absolute value of a non-zero number is positive.
|- (A e. CC -> (A =/= 0 <-> 0 < (abs` A)))
Theorem	abssub 7097	Swapping order of subtraction doesn't change the absolute value.
|- ((A e. CC /\ B e. CC) -> (abs` (A - B)) = (abs` (B - A)))
Theorem	abssubge0 7098	Absolute value of a nonnegative difference.
|- ((A e. RR /\ B e. RR /\ A <_ B) -> (abs` (B - A)) = (B - A))
Theorem	abssuble0 7099	Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.)
|- ((A e. RR /\ B e. RR /\ A <_ B) -> (abs` (A - B)) = (B - A))
Theorem	absmax 7100	The maximum of two numbers using absolute value.
|- ((A e. RR /\ B e. RR) -> if(A <_ B, B, A) = (((A + B) + (abs` (A - B))) / 2))