HomeHome Intuitionistic Logic Explorer
Theorem List (p. 91 of 95)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9001-9100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremnnesq 9001 A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
(𝑁 ℕ → ((𝑁 / 2) ℕ ↔ ((𝑁↑2) / 2) ℕ))
 
Theorembernneq 9002 Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
((A 𝑁 0 -1 ≤ A) → (1 + (A · 𝑁)) ≤ ((1 + A)↑𝑁))
 
Theorembernneq2 9003 Variation of Bernoulli's inequality bernneq 9002. (Contributed by NM, 18-Oct-2007.)
((A 𝑁 0 0 ≤ A) → (((A − 1) · 𝑁) + 1) ≤ (A𝑁))
 
Theorembernneq3 9004 A corollary of bernneq 9002. (Contributed by Mario Carneiro, 11-Mar-2014.)
((𝑃 (ℤ‘2) 𝑁 0) → 𝑁 < (𝑃𝑁))
 
Theoremexpnbnd 9005* Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
((A B 1 < B) → 𝑘 A < (B𝑘))
 
Theoremexpnlbnd 9006* The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.)
((A + B 1 < B) → 𝑘 ℕ (1 / (B𝑘)) < A)
 
Theoremexpnlbnd2 9007* The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
((A + B 1 < B) → 𝑗 𝑘 (ℤ𝑗)(1 / (B𝑘)) < A)
 
Theoremexp0d 9008 Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑0) = 1)
 
Theoremexp1d 9009 Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑1) = A)
 
Theoremexpeq0d 9010 Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 ℕ)    &   (φ → (A𝑁) = 0)       (φA = 0)
 
Theoremsqvald 9011 Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑2) = (A · A))
 
Theoremsqcld 9012 Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑2) ℂ)
 
Theoremsqeq0d 9013 A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ → (A↑2) = 0)       (φA = 0)
 
Theoremexpcld 9014 Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)       (φ → (A𝑁) ℂ)
 
Theoremexpp1d 9015 Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)       (φ → (A↑(𝑁 + 1)) = ((A𝑁) · A))
 
Theoremexpaddd 9016 Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)    &   (φ𝑀 0)       (φ → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))
 
Theoremexpmuld 9017 Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)    &   (φ𝑀 0)       (φ → (A↑(𝑀 · 𝑁)) = ((A𝑀)↑𝑁))
 
Theoremsqrecapd 9018 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)       (φ → ((1 / A)↑2) = (1 / (A↑2)))
 
Theoremexpclzapd 9019 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) ℂ)
 
Theoremexpap0d 9020 Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) # 0)
 
Theoremexpnegapd 9021 Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A↑-𝑁) = (1 / (A𝑁)))
 
Theoremexprecapd 9022 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → ((1 / A)↑𝑁) = (1 / (A𝑁)))
 
Theoremexpp1zapd 9023 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A↑(𝑁 + 1)) = ((A𝑁) · A))
 
Theoremexpm1apd 9024 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A↑(𝑁 − 1)) = ((A𝑁) / A))
 
Theoremexpsubapd 9025 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)    &   (φ𝑀 ℤ)       (φ → (A↑(𝑀𝑁)) = ((A𝑀) / (A𝑁)))
 
Theoremsqmuld 9026 Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → ((A · B)↑2) = ((A↑2) · (B↑2)))
 
Theoremsqdivapd 9027 Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → ((A / B)↑2) = ((A↑2) / (B↑2)))
 
Theoremexpdivapd 9028 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)    &   (φ𝑁 0)       (φ → ((A / B)↑𝑁) = ((A𝑁) / (B𝑁)))
 
Theoremmulexpd 9029 Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φB ℂ)    &   (φ𝑁 0)       (φ → ((A · B)↑𝑁) = ((A𝑁) · (B𝑁)))
 
Theorem0expd 9030 Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
(φ𝑁 ℕ)       (φ → (0↑𝑁) = 0)
 
Theoremreexpcld 9031 Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φ𝑁 0)       (φ → (A𝑁) ℝ)
 
Theoremexpge0d 9032 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φ𝑁 0)    &   (φ → 0 ≤ A)       (φ → 0 ≤ (A𝑁))
 
Theoremexpge1d 9033 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φ𝑁 0)    &   (φ → 1 ≤ A)       (φ → 1 ≤ (A𝑁))
 
Theoremnnsqcld 9034 The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℕ)       (φ → (A↑2) ℕ)
 
Theoremnnexpcld 9035 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℕ)    &   (φ𝑁 0)       (φ → (A𝑁) ℕ)
 
Theoremnn0expcld 9036 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA 0)    &   (φ𝑁 0)       (φ → (A𝑁) 0)
 
Theoremrpexpcld 9037 Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA +)    &   (φ𝑁 ℤ)       (φ → (A𝑁) +)
 
Theoremreexpclzapd 9038 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℝ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) ℝ)
 
Theoremresqcld 9039 Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)       (φ → (A↑2) ℝ)
 
Theoremsqge0d 9040 A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)       (φ → 0 ≤ (A↑2))
 
Theoremsqgt0apd 9041 The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℝ)    &   (φA # 0)       (φ → 0 < (A↑2))
 
Theoremleexp2ad 9042 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φ → 1 ≤ A)    &   (φ𝑁 (ℤ𝑀))       (φ → (A𝑀) ≤ (A𝑁))
 
Theoremleexp2rd 9043 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φ𝑀 0)    &   (φ𝑁 (ℤ𝑀))    &   (φ → 0 ≤ A)    &   (φA ≤ 1)       (φ → (A𝑁) ≤ (A𝑀))
 
Theoremlt2sqd 9044 The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ → 0 ≤ A)    &   (φ → 0 ≤ B)       (φ → (A < B ↔ (A↑2) < (B↑2)))
 
Theoremle2sqd 9045 The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ → 0 ≤ A)    &   (φ → 0 ≤ B)       (φ → (AB ↔ (A↑2) ≤ (B↑2)))
 
Theoremsq11d 9046 The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℝ)    &   (φB ℝ)    &   (φ → 0 ≤ A)    &   (φ → 0 ≤ B)    &   (φ → (A↑2) = (B↑2))       (φA = B)
 
3.6  Elementary real and complex functions
 
3.6.1  Real and imaginary parts; conjugate
 
Syntaxccj 9047 Extend class notation to include complex conjugate function.
class
 
Syntaxcre 9048 Extend class notation to include real part of a complex number.
class
 
Syntaxcim 9049 Extend class notation to include imaginary part of a complex number.
class
 
Definitiondf-cj 9050* Define the complex conjugate function. See cjcli 9121 for its closure and cjval 9053 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
∗ = (x ℂ ↦ (y ℂ ((x + y) (i · (xy)) ℝ)))
 
Definitiondf-re 9051 Define a function whose value is the real part of a complex number. See reval 9057 for its value, recli 9119 for its closure, and replim 9067 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
ℜ = (x ℂ ↦ ((x + (∗‘x)) / 2))
 
Definitiondf-im 9052 Define a function whose value is the imaginary part of a complex number. See imval 9058 for its value, imcli 9120 for its closure, and replim 9067 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
ℑ = (x ℂ ↦ (ℜ‘(x / i)))
 
Theoremcjval 9053* The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
(A ℂ → (∗‘A) = (x ℂ ((A + x) (i · (Ax)) ℝ)))
 
Theoremcjth 9054 The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
(A ℂ → ((A + (∗‘A)) (i · (A − (∗‘A))) ℝ))
 
Theoremcjf 9055 Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
∗:ℂ⟶ℂ
 
Theoremcjcl 9056 The conjugate of a complex number is a complex number (closure law). (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(A ℂ → (∗‘A) ℂ)
 
Theoremreval 9057 The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(A ℂ → (ℜ‘A) = ((A + (∗‘A)) / 2))
 
Theoremimval 9058 The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(A ℂ → (ℑ‘A) = (ℜ‘(A / i)))
 
Theoremimre 9059 The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 6-Nov-2013.)
(A ℂ → (ℑ‘A) = (ℜ‘(-i · A)))
 
Theoremreim 9060 The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
(A ℂ → (ℜ‘A) = (ℑ‘(i · A)))
 
Theoremrecl 9061 The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(A ℂ → (ℜ‘A) ℝ)
 
Theoremimcl 9062 The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
(A ℂ → (ℑ‘A) ℝ)
 
Theoremref 9063 Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
ℜ:ℂ⟶ℝ
 
Theoremimf 9064 Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
ℑ:ℂ⟶ℝ
 
Theoremcrre 9065 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
((A B ℝ) → (ℜ‘(A + (i · B))) = A)
 
Theoremcrim 9066 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
((A B ℝ) → (ℑ‘(A + (i · B))) = B)
 
Theoremreplim 9067 Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
(A ℂ → A = ((ℜ‘A) + (i · (ℑ‘A))))
 
Theoremremim 9068 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 NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
(A ℂ → (∗‘A) = ((ℜ‘A) − (i · (ℑ‘A))))
 
Theoremreim0 9069 The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
(A ℝ → (ℑ‘A) = 0)
 
Theoremreim0b 9070 A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
(A ℂ → (A ℝ ↔ (ℑ‘A) = 0))
 
Theoremrereb 9071 A number is real iff it equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 20-Aug-2008.)
(A ℂ → (A ℝ ↔ (ℜ‘A) = A))
 
Theoremmulreap 9072 A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (A ℝ ↔ (B · A) ℝ))
 
Theoremrere 9073 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)
 
Theoremcjreb 9074 A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (A ℝ ↔ (∗‘A) = A))
 
Theoremrecj 9075 Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (ℜ‘(∗‘A)) = (ℜ‘A))
 
Theoremreneg 9076 Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (ℜ‘-A) = -(ℜ‘A))
 
Theoremreadd 9077 Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
((A B ℂ) → (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B)))
 
Theoremresub 9078 Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
((A B ℂ) → (ℜ‘(AB)) = ((ℜ‘A) − (ℜ‘B)))
 
Theoremremullem 9079 Lemma for remul 9080, immul 9087, and cjmul 9093. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((A B ℂ) → ((ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B))) (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))) (∗‘(A · B)) = ((∗‘A) · (∗‘B))))
 
Theoremremul 9080 Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((A B ℂ) → (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B))))
 
Theoremremul2 9081 Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
((A B ℂ) → (ℜ‘(A · B)) = (A · (ℜ‘B)))
 
Theoremredivap 9082 Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B))
 
Theoremimcj 9083 Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (ℑ‘(∗‘A)) = -(ℑ‘A))
 
Theoremimneg 9084 The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (ℑ‘-A) = -(ℑ‘A))
 
Theoremimadd 9085 Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
((A B ℂ) → (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B)))
 
Theoremimsub 9086 Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.)
((A B ℂ) → (ℑ‘(AB)) = ((ℑ‘A) − (ℑ‘B)))
 
Theoremimmul 9087 Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((A B ℂ) → (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))))
 
Theoremimmul2 9088 Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
((A B ℂ) → (ℑ‘(A · B)) = (A · (ℑ‘B)))
 
Theoremimdivap 9089 Imaginary part of a division. Related to immul2 9088. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B))
 
Theoremcjre 9090 A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.)
(A ℝ → (∗‘A) = A)
 
Theoremcjcj 9091 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 ℂ → (∗‘(∗‘A)) = A)
 
Theoremcjadd 9092 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 B ℂ) → (∗‘(A + B)) = ((∗‘A) + (∗‘B)))
 
Theoremcjmul 9093 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 B ℂ) → (∗‘(A · B)) = ((∗‘A) · (∗‘B)))
 
Theoremipcnval 9094 Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
((A B ℂ) → (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B))))
 
Theoremcjmulrcl 9095 A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (A · (∗‘A)) ℝ)
 
Theoremcjmulval 9096 A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2)))
 
Theoremcjmulge0 9097 A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → 0 ≤ (A · (∗‘A)))
 
Theoremcjneg 9098 Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℂ → (∗‘-A) = -(∗‘A))
 
Theoremaddcj 9099 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 ℂ → (A + (∗‘A)) = (2 · (ℜ‘A)))
 
Theoremcjsub 9100 Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.)
((A B ℂ) → (∗‘(AB)) = ((∗‘A) − (∗‘B)))
    < Previous  Next >

Page List
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-9427
  Copyright terms: Public domain < Previous  Next >