![]() |
Metamath
Proof Explorer Theorem List (p. 152 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cjexp 15101 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) | ||
Theorem | imval2 15102 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
โข (๐ด โ โ โ (โโ๐ด) = ((๐ด โ (โโ๐ด)) / (2 ยท i))) | ||
Theorem | re0 15103 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
โข (โโ0) = 0 | ||
Theorem | im0 15104 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
โข (โโ0) = 0 | ||
Theorem | re1 15105 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโ1) = 1 | ||
Theorem | im1 15106 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโ1) = 0 | ||
Theorem | rei 15107 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโi) = 0 | ||
Theorem | imi 15108 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโi) = 1 | ||
Theorem | cj0 15109 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
โข (โโ0) = 0 | ||
Theorem | cji 15110 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
โข (โโi) = -i | ||
Theorem | cjreim 15111 | The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โโ(๐ด + (i ยท ๐ต))) = (๐ด โ (i ยท ๐ต))) | ||
Theorem | cjreim2 15112 | 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.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โโ(๐ด โ (i ยท ๐ต))) = (๐ด + (i ยท ๐ต))) | ||
Theorem | cj11 15113 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((โโ๐ด) = (โโ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | cjne0 15114 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
โข (๐ด โ โ โ (๐ด โ 0 โ (โโ๐ด) โ 0)) | ||
Theorem | cjdiv 15115 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | cnrecnv 15116* | The inverse to the canonical bijection from (โ ร โ) to โ from cnref1o 12973. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ๐น = (๐ฅ โ โ, ๐ฆ โ โ โฆ (๐ฅ + (i ยท ๐ฆ))) โ โข โก๐น = (๐ง โ โ โฆ โจ(โโ๐ง), (โโ๐ง)โฉ) | ||
Theorem | sqeqd 15117 | A deduction for showing two numbers whose squares are equal are themselves equal. (Contributed by Mario Carneiro, 3-Apr-2015.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ (๐ดโ2) = (๐ตโ2)) & โข (๐ โ 0 โค (โโ๐ด)) & โข (๐ โ 0 โค (โโ๐ต)) & โข ((๐ โง (โโ๐ด) = 0 โง (โโ๐ต) = 0) โ ๐ด = ๐ต) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | recli 15118 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (โโ๐ด) โ โ | ||
Theorem | imcli 15119 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (โโ๐ด) โ โ | ||
Theorem | cjcli 15120 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (โโ๐ด) โ โ | ||
Theorem | replimi 15121 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
โข ๐ด โ โ โ โข ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด))) | ||
Theorem | cjcji 15122 | 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.) |
โข ๐ด โ โ โ โข (โโ(โโ๐ด)) = ๐ด | ||
Theorem | reim0bi 15123 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
โข ๐ด โ โ โ โข (๐ด โ โ โ (โโ๐ด) = 0) | ||
Theorem | rerebi 15124 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
โข ๐ด โ โ โ โข (๐ด โ โ โ (โโ๐ด) = ๐ด) | ||
Theorem | cjrebi 15125 | 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.) |
โข ๐ด โ โ โ โข (๐ด โ โ โ (โโ๐ด) = ๐ด) | ||
Theorem | recji 15126 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข (โโ(โโ๐ด)) = (โโ๐ด) | ||
Theorem | imcji 15127 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข (โโ(โโ๐ด)) = -(โโ๐ด) | ||
Theorem | cjmulrcli 15128 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (๐ด ยท (โโ๐ด)) โ โ | ||
Theorem | cjmulvali 15129 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2)) | ||
Theorem | cjmulge0i 15130 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
โข ๐ด โ โ โ โข 0 โค (๐ด ยท (โโ๐ด)) | ||
Theorem | renegi 15131 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (โโ-๐ด) = -(โโ๐ด) | ||
Theorem | imnegi 15132 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (โโ-๐ด) = -(โโ๐ด) | ||
Theorem | cjnegi 15133 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (โโ-๐ด) = -(โโ๐ด) | ||
Theorem | addcji 15134 | 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.) |
โข ๐ด โ โ โ โข (๐ด + (โโ๐ด)) = (2 ยท (โโ๐ด)) | ||
Theorem | readdi 15135 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | imaddi 15136 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | remuli 15137 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | immuli 15138 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjaddi 15139 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | cjmuli 15140 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต)) | ||
Theorem | ipcni 15141 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjdivi 15142 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | crrei 15143 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + (i ยท ๐ต))) = ๐ด | ||
Theorem | crimi 15144 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + (i ยท ๐ต))) = ๐ต | ||
Theorem | recld 15145 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | imcld 15146 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | cjcld 15147 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | replimd 15148 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด)))) | ||
Theorem | remimd 15149 | 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.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = ((โโ๐ด) โ (i ยท (โโ๐ด)))) | ||
Theorem | cjcjd 15150 | 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.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = ๐ด) | ||
Theorem | reim0bd 15151 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = 0) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | rerebd 15152 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = ๐ด) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | cjrebd 15153 | 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.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = ๐ด) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | cjne0d 15154 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ๐ด) โ 0) | ||
Theorem | recjd 15155 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = (โโ๐ด)) | ||
Theorem | imcjd 15156 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = -(โโ๐ด)) | ||
Theorem | cjmulrcld 15157 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) โ โ) | ||
Theorem | cjmulvald 15158 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) | ||
Theorem | cjmulge0d 15159 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 0 โค (๐ด ยท (โโ๐ด))) | ||
Theorem | renegd 15160 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | imnegd 15161 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | cjnegd 15162 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | addcjd 15163 | 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.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด + (โโ๐ด)) = (2 ยท (โโ๐ด))) | ||
Theorem | cjexpd 15164 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) | ||
Theorem | readdd 15165 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | imaddd 15166 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | resubd 15167 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | imsubd 15168 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | remuld 15169 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | immuld 15170 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjaddd 15171 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | cjmuld 15172 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | ipcnd 15173 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjdivd 15174 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | rered 15175 | 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.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = ๐ด) | ||
Theorem | reim0d 15176 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = 0) | ||
Theorem | cjred 15177 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = ๐ด) | ||
Theorem | remul2d 15178 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | immul2d 15179 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | redivd 15180 | Real part of a division. Related to remul2 15081. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | imdivd 15181 | Imaginary part of a division. Related to remul2 15081. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | crred 15182 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ด) | ||
Theorem | crimd 15183 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ต) | ||
Syntax | csqrt 15184 | Extend class notation to include square root of a complex number. |
class โ | ||
Syntax | cabs 15185 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-sqrt 15186* |
Define a function whose value is the square root of a complex number.
For example, (โโ25) = 5 (ex-sqrt 29974).
Since (๐ฆโ2) = ๐ฅ iff (-๐ฆโ2) = ๐ฅ, we ensure uniqueness by restricting the range to numbers with positive real part, or numbers with 0 real part and nonnegative imaginary part. A description can be found under "Principal square root of a complex number" at http://en.wikipedia.org/wiki/Square_root 29974. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15312 for its closure, sqrtval 15188 for its value, sqrtth 15315 and sqsqrti 15326 for its relationship to squares, and sqrt11i 15335 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
โข โ = (๐ฅ โ โ โฆ (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))) | ||
Definition | df-abs 15187 | Define the function for the absolute value (modulus) of a complex number. See abscli 15346 for its closure and absval 15189 or absval2i 15348 for its value. For example, (absโ-2) = 2 (ex-abs 29975). (Contributed by NM, 27-Jul-1999.) |
โข abs = (๐ฅ โ โ โฆ (โโ(๐ฅ ยท (โโ๐ฅ)))) | ||
Theorem | sqrtval 15188* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (โโ๐ด) = (โฉ๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))) | ||
Theorem | absval 15189 | 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.) |
โข (๐ด โ โ โ (absโ๐ด) = (โโ(๐ด ยท (โโ๐ด)))) | ||
Theorem | rennim 15190 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (i ยท ๐ด) โ โ+) | ||
Theorem | cnpart 15191 | The specification of restriction to the right half-plane partitions the complex plane without 0 into two disjoint pieces, which are related by a reflection about the origin (under the map ๐ฅ โฆ -๐ฅ). (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ (0 โค (โโ-๐ด) โง (i ยท -๐ด) โ โ+))) | ||
Theorem | sqrt0 15192 | The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข (โโ0) = 0 | ||
Theorem | 01sqrexlem1 15193* | Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฆ โ ๐ ๐ฆ โค 1) | ||
Theorem | 01sqrexlem2 15194* | Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ๐ด โ ๐) | ||
Theorem | 01sqrexlem3 15195* | Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ฆ โ ๐ ๐ฆ โค ๐ง)) | ||
Theorem | 01sqrexlem4 15196* | Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ต โ โ+ โง ๐ต โค 1)) | ||
Theorem | 01sqrexlem5 15197* | Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ((๐ โ โ โง ๐ โ โ โง โ๐ฃ โ โ โ๐ข โ ๐ ๐ข โค ๐ฃ) โง (๐ตโ2) = sup(๐, โ, < ))) | ||
Theorem | 01sqrexlem6 15198* | Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) โค ๐ด) | ||
Theorem | 01sqrexlem7 15199* | Lemma for 01sqrex 15200. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) = ๐ด) | ||
Theorem | 01sqrex 15200* | Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฅ โ โ+ (๐ฅ โค 1 โง (๐ฅโ2) = ๐ด)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |