![]() |
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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cjsub 15101 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | cjexp 15102 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) | ||
Theorem | imval2 15103 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
โข (๐ด โ โ โ (โโ๐ด) = ((๐ด โ (โโ๐ด)) / (2 ยท i))) | ||
Theorem | re0 15104 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
โข (โโ0) = 0 | ||
Theorem | im0 15105 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
โข (โโ0) = 0 | ||
Theorem | re1 15106 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโ1) = 1 | ||
Theorem | im1 15107 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโ1) = 0 | ||
Theorem | rei 15108 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโi) = 0 | ||
Theorem | imi 15109 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
โข (โโi) = 1 | ||
Theorem | cj0 15110 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
โข (โโ0) = 0 | ||
Theorem | cji 15111 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
โข (โโi) = -i | ||
Theorem | cjreim 15112 | 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 15113 | 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 15114 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((โโ๐ด) = (โโ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | cjne0 15115 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
โข (๐ด โ โ โ (๐ด โ 0 โ (โโ๐ด) โ 0)) | ||
Theorem | cjdiv 15116 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | cnrecnv 15117* | The inverse to the canonical bijection from (โ ร โ) to โ from cnref1o 12974. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ๐น = (๐ฅ โ โ, ๐ฆ โ โ โฆ (๐ฅ + (i ยท ๐ฆ))) โ โข โก๐น = (๐ง โ โ โฆ โจ(โโ๐ง), (โโ๐ง)โฉ) | ||
Theorem | sqeqd 15118 | 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 15119 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (โโ๐ด) โ โ | ||
Theorem | imcli 15120 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (โโ๐ด) โ โ | ||
Theorem | cjcli 15121 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (โโ๐ด) โ โ | ||
Theorem | replimi 15122 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
โข ๐ด โ โ โ โข ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด))) | ||
Theorem | cjcji 15123 | 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 15124 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
โข ๐ด โ โ โ โข (๐ด โ โ โ (โโ๐ด) = 0) | ||
Theorem | rerebi 15125 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
โข ๐ด โ โ โ โข (๐ด โ โ โ (โโ๐ด) = ๐ด) | ||
Theorem | cjrebi 15126 | 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 15127 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข (โโ(โโ๐ด)) = (โโ๐ด) | ||
Theorem | imcji 15128 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข (โโ(โโ๐ด)) = -(โโ๐ด) | ||
Theorem | cjmulrcli 15129 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
โข ๐ด โ โ โ โข (๐ด ยท (โโ๐ด)) โ โ | ||
Theorem | cjmulvali 15130 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2)) | ||
Theorem | cjmulge0i 15131 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
โข ๐ด โ โ โ โข 0 โค (๐ด ยท (โโ๐ด)) | ||
Theorem | renegi 15132 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (โโ-๐ด) = -(โโ๐ด) | ||
Theorem | imnegi 15133 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (โโ-๐ด) = -(โโ๐ด) | ||
Theorem | cjnegi 15134 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (โโ-๐ด) = -(โโ๐ด) | ||
Theorem | addcji 15135 | 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 15136 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | imaddi 15137 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | remuli 15138 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | immuli 15139 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjaddi 15140 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | cjmuli 15141 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต)) | ||
Theorem | ipcni 15142 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjdivi 15143 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | crrei 15144 | 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 15145 | 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 15146 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | imcld 15147 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | cjcld 15148 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | replimd 15149 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด)))) | ||
Theorem | remimd 15150 | 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 15151 | 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 15152 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = 0) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | rerebd 15153 | 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 15154 | 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 15155 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ๐ด) โ 0) | ||
Theorem | recjd 15156 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = (โโ๐ด)) | ||
Theorem | imcjd 15157 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = -(โโ๐ด)) | ||
Theorem | cjmulrcld 15158 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) โ โ) | ||
Theorem | cjmulvald 15159 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) | ||
Theorem | cjmulge0d 15160 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 0 โค (๐ด ยท (โโ๐ด))) | ||
Theorem | renegd 15161 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | imnegd 15162 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | cjnegd 15163 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | addcjd 15164 | 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 15165 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) | ||
Theorem | readdd 15166 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | imaddd 15167 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | resubd 15168 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | imsubd 15169 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | remuld 15170 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | immuld 15171 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjaddd 15172 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | cjmuld 15173 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | ipcnd 15174 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjdivd 15175 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | rered 15176 | 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 15177 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = 0) | ||
Theorem | cjred 15178 | 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 15179 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | immul2d 15180 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | redivd 15181 | Real part of a division. Related to remul2 15082. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | imdivd 15182 | Imaginary part of a division. Related to remul2 15082. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | crred 15183 | 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 15184 | 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 15185 | Extend class notation to include square root of a complex number. |
class โ | ||
Syntax | cabs 15186 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-sqrt 15187* |
Define a function whose value is the square root of a complex number.
For example, (โโ25) = 5 (ex-sqrt 29971).
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 29971. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15313 for its closure, sqrtval 15189 for its value, sqrtth 15316 and sqsqrti 15327 for its relationship to squares, and sqrt11i 15336 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
โข โ = (๐ฅ โ โ โฆ (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))) | ||
Definition | df-abs 15188 | Define the function for the absolute value (modulus) of a complex number. See abscli 15347 for its closure and absval 15190 or absval2i 15349 for its value. For example, (absโ-2) = 2 (ex-abs 29972). (Contributed by NM, 27-Jul-1999.) |
โข abs = (๐ฅ โ โ โฆ (โโ(๐ฅ ยท (โโ๐ฅ)))) | ||
Theorem | sqrtval 15189* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (โโ๐ด) = (โฉ๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))) | ||
Theorem | absval 15190 | 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 15191 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (i ยท ๐ด) โ โ+) | ||
Theorem | cnpart 15192 | 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 15193 | The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข (โโ0) = 0 | ||
Theorem | 01sqrexlem1 15194* | Lemma for 01sqrex 15201. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฆ โ ๐ ๐ฆ โค 1) | ||
Theorem | 01sqrexlem2 15195* | Lemma for 01sqrex 15201. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ๐ด โ ๐) | ||
Theorem | 01sqrexlem3 15196* | Lemma for 01sqrex 15201. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ฆ โ ๐ ๐ฆ โค ๐ง)) | ||
Theorem | 01sqrexlem4 15197* | Lemma for 01sqrex 15201. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ต โ โ+ โง ๐ต โค 1)) | ||
Theorem | 01sqrexlem5 15198* | Lemma for 01sqrex 15201. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ((๐ โ โ โง ๐ โ โ โง โ๐ฃ โ โ โ๐ข โ ๐ ๐ข โค ๐ฃ) โง (๐ตโ2) = sup(๐, โ, < ))) | ||
Theorem | 01sqrexlem6 15199* | Lemma for 01sqrex 15201. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) โค ๐ด) | ||
Theorem | 01sqrexlem7 15200* | Lemma for 01sqrex 15201. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) = ๐ด) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |