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-12230

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

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