 Home Intuitionistic Logic ExplorerTheorem List (p. 92 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 - 9101-9200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcjexp 9101 Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
((A 𝑁 0) → (∗‘(A𝑁)) = ((∗‘A)↑𝑁))

Theoremimval2 9102 The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
(A ℂ → (ℑ‘A) = ((A − (∗‘A)) / (2 · i)))

Theoremre0 9103 The real part of zero. (Contributed by NM, 27-Jul-1999.)
(ℜ‘0) = 0

Theoremim0 9104 The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
(ℑ‘0) = 0

Theoremre1 9105 The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
(ℜ‘1) = 1

Theoremim1 9106 The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
(ℑ‘1) = 0

Theoremrei 9107 The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
(ℜ‘i) = 0

Theoremimi 9108 The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
(ℑ‘i) = 1

Theoremcj0 9109 The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
(∗‘0) = 0

Theoremcji 9110 The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
(∗‘i) = -i

Theoremcjreim 9111 The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.)
((A B ℝ) → (∗‘(A + (i · B))) = (A − (i · B)))

Theoremcjreim2 9112 The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
((A B ℝ) → (∗‘(A − (i · B))) = (A + (i · B)))

Theoremcj11 9113 Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
((A B ℂ) → ((∗‘A) = (∗‘B) ↔ A = B))

Theoremcjap 9114 Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B ℂ) → ((∗‘A) # (∗‘B) ↔ A # B))

Theoremcjap0 9115 A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
(A ℂ → (A # 0 ↔ (∗‘A) # 0))

Theoremcjne0 9116 A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.)
(A ℂ → (A ≠ 0 ↔ (∗‘A) ≠ 0))

Theoremcjdivap 9117 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

Theoremcnrecnv 9118* The inverse to the canonical bijection from (ℝ × ℝ) to from cnref1o 8337. (Contributed by Mario Carneiro, 25-Aug-2014.)
𝐹 = (x ℝ, y ℝ ↦ (x + (i · y)))       𝐹 = (z ℂ ↦ ⟨(ℜ‘z), (ℑ‘z)⟩)

Theoremrecli 9119 The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
A        (ℜ‘A)

Theoremimcli 9120 The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
A        (ℑ‘A)

Theoremcjcli 9121 Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
A        (∗‘A)

Theoremreplimi 9122 Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
A        A = ((ℜ‘A) + (i · (ℑ‘A)))

Theoremcjcji 9123 The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)
A        (∗‘(∗‘A)) = A

Theoremreim0bi 9124 A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
A        (A ℝ ↔ (ℑ‘A) = 0)

Theoremrerebi 9125 A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
A        (A ℝ ↔ (ℜ‘A) = A)

Theoremcjrebi 9126 A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)
A        (A ℝ ↔ (∗‘A) = A)

Theoremrecji 9127 Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
A        (ℜ‘(∗‘A)) = (ℜ‘A)

Theoremimcji 9128 Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
A        (ℑ‘(∗‘A)) = -(ℑ‘A)

Theoremcjmulrcli 9129 A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
A        (A · (∗‘A))

Theoremcjmulvali 9130 A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
A        (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2))

Theoremcjmulge0i 9131 A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
A        0 ≤ (A · (∗‘A))

Theoremrenegi 9132 Real part of negative. (Contributed by NM, 2-Aug-1999.)
A        (ℜ‘-A) = -(ℜ‘A)

Theoremimnegi 9133 Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
A        (ℑ‘-A) = -(ℑ‘A)

Theoremcjnegi 9134 Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
A        (∗‘-A) = -(∗‘A)

Theoremaddcji 9135 A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
A        (A + (∗‘A)) = (2 · (ℜ‘A))

A     &   B        (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B))

A     &   B        (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B))

Theoremremuli 9138 Real part of a product. (Contributed by NM, 28-Jul-1999.)
A     &   B        (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B)))

Theoremimmuli 9139 Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
A     &   B        (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B)))

Theoremcjaddi 9140 Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
A     &   B        (∗‘(A + B)) = ((∗‘A) + (∗‘B))

Theoremcjmuli 9141 Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
A     &   B        (∗‘(A · B)) = ((∗‘A) · (∗‘B))

Theoremipcni 9142 Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
A     &   B        (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B)))

Theoremcjdivapi 9143 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
A     &   B        (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

Theoremcrrei 9144 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
A     &   B        (ℜ‘(A + (i · B))) = A

Theoremcrimi 9145 The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
A     &   B        (ℑ‘(A + (i · B))) = B

Theoremrecld 9146 The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (ℜ‘A) ℝ)

Theoremimcld 9147 The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (ℑ‘A) ℝ)

Theoremcjcld 9148 Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (∗‘A) ℂ)

Theoremreplimd 9149 Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φA = ((ℜ‘A) + (i · (ℑ‘A))))

Theoremremimd 9150 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 Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (∗‘A) = ((ℜ‘A) − (i · (ℑ‘A))))

Theoremcjcjd 9151 The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (∗‘(∗‘A)) = A)

Theoremreim0bd 9152 A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φ → (ℑ‘A) = 0)       (φA ℝ)

Theoremrerebd 9153 A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φ → (ℜ‘A) = A)       (φA ℝ)

Theoremcjrebd 9154 A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φ → (∗‘A) = A)       (φA ℝ)

Theoremcjne0d 9155 A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φA ≠ 0)       (φ → (∗‘A) ≠ 0)

Theoremrecjd 9156 Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (ℜ‘(∗‘A)) = (ℜ‘A))

Theoremimcjd 9157 Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (ℑ‘(∗‘A)) = -(ℑ‘A))

Theoremcjmulrcld 9158 A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (A · (∗‘A)) ℝ)

Theoremcjmulvald 9159 A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2)))

Theoremcjmulge0d 9160 A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → 0 ≤ (A · (∗‘A)))

Theoremrenegd 9161 Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (ℜ‘-A) = -(ℜ‘A))

Theoremimnegd 9162 Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (ℑ‘-A) = -(ℑ‘A))

Theoremcjnegd 9163 Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (∗‘-A) = -(∗‘A))

Theoremaddcjd 9164 A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)       (φ → (A + (∗‘A)) = (2 · (ℜ‘A)))

Theoremcjexpd 9165 Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φ𝑁 0)       (φ → (∗‘(A𝑁)) = ((∗‘A)↑𝑁))

Theoremreaddd 9166 Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B)))

Theoremimaddd 9167 Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B)))

Theoremresubd 9168 Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (ℜ‘(AB)) = ((ℜ‘A) − (ℜ‘B)))

Theoremimsubd 9169 Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (ℑ‘(AB)) = ((ℑ‘A) − (ℑ‘B)))

Theoremremuld 9170 Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B))))

Theoremimmuld 9171 Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))))

Theoremcjaddd 9172 Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (∗‘(A + B)) = ((∗‘A) + (∗‘B)))

Theoremcjmuld 9173 Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (∗‘(A · B)) = ((∗‘A) · (∗‘B)))

Theoremipcnd 9174 Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℂ)    &   (φB ℂ)       (φ → (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B))))

Theoremcjdivapd 9175 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

Theoremrered 9176 A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℝ)       (φ → (ℜ‘A) = A)

Theoremreim0d 9177 The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℝ)       (φ → (ℑ‘A) = 0)

Theoremcjred 9178 A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℝ)       (φ → (∗‘A) = A)

Theoremremul2d 9179 Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℝ)    &   (φB ℂ)       (φ → (ℜ‘(A · B)) = (A · (ℜ‘B)))

Theoremimmul2d 9180 Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℝ)    &   (φB ℂ)       (φ → (ℑ‘(A · B)) = (A · (ℑ‘B)))

Theoremredivapd 9181 Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
(φA ℝ)    &   (φB ℂ)    &   (φA # 0)       (φ → (ℜ‘(B / A)) = ((ℜ‘B) / A))

Theoremimdivapd 9182 Imaginary part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
(φA ℝ)    &   (φB ℂ)    &   (φA # 0)       (φ → (ℑ‘(B / A)) = ((ℑ‘B) / A))

Theoremcrred 9183 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℝ)    &   (φB ℝ)       (φ → (ℜ‘(A + (i · B))) = A)

Theoremcrimd 9184 The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
(φA ℝ)    &   (φB ℝ)       (φ → (ℑ‘(A + (i · B))) = B)

3.6.2  Square root; absolute value

Syntaxcsqrt 9185 Extend class notation to include square root of a complex number.
class

Syntaxcabs 9186 Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs

Definitiondf-rsqrt 9187* Define a function whose value is the square root of a nonnegative real number.

Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root.

(Contributed by Jim Kingdon, 23-Aug-2020.)

√ = (x ℝ ↦ (y ℝ ((y↑2) = x 0 ≤ y)))

Definitiondf-abs 9188 Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
abs = (x ℂ ↦ (√‘(x · (∗‘x))))

Theoremsqrtrval 9189* Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
(A ℝ → (√‘A) = (x ℝ ((x↑2) = A 0 ≤ x)))

Theoremabsval 9190 The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
(A ℂ → (abs‘A) = (√‘(A · (∗‘A))))

Theoremrennim 9191 A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
(A ℝ → (i · A) ∉ ℝ+)

Theoremsqrt0rlem 9192 Lemma for sqrt0 9193. (Contributed by Jim Kingdon, 26-Aug-2020.)
((A ((A↑2) = 0 0 ≤ A)) ↔ A = 0)

Theoremsqrt0 9193 Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
(√‘0) = 0

Theoremsqrtsq 9194 Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
((A 0 ≤ A) → (√‘(A↑2)) = A)

Theoremsqrtmsq 9195 Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
((A 0 ≤ A) → (√‘(A · A)) = A)

Theoremsqrt1 9196 The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
(√‘1) = 1

Theoremsqrt4 9197 The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
(√‘4) = 2

Theoremsqrt9 9198 The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
(√‘9) = 3

Theoremabsneg 9199 Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
(A ℂ → (abs‘-A) = (abs‘A))

Theoremabscj 9200 The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.)
(A ℂ → (abs‘(∗‘A)) = (abs‘A))

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 >