Home | Intuitionistic Logic Explorer Theorem List (p. 96 of 102) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cj0 9501 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
Theorem | cji 9502 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
Theorem | cjreim 9503 | The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) |
Theorem | cjreim2 9504 | 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.) |
Theorem | cj11 9505 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
Theorem | cjap 9506 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# # | ||
Theorem | cjap0 9507 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# # | ||
Theorem | cjne0 9508 | A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 9507 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.) |
Theorem | cjdivap 9509 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
Theorem | cnrecnv 9510* | The inverse to the canonical bijection from to from cnref1o 8582. (Contributed by Mario Carneiro, 25-Aug-2014.) |
Theorem | recli 9511 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
Theorem | imcli 9512 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
Theorem | cjcli 9513 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
Theorem | replimi 9514 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
Theorem | cjcji 9515 | 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 9516 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
Theorem | rerebi 9517 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
Theorem | cjrebi 9518 | 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 9519 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | imcji 9520 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjmulrcli 9521 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
Theorem | cjmulvali 9522 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjmulge0i 9523 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
Theorem | renegi 9524 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | imnegi 9525 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | cjnegi 9526 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | addcji 9527 | 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.) |
Theorem | readdi 9528 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
Theorem | imaddi 9529 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
Theorem | remuli 9530 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | immuli 9531 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjaddi 9532 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjmuli 9533 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | ipcni 9534 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjdivapi 9535 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
Theorem | crrei 9536 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | crimi 9537 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | recld 9538 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcld 9539 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjcld 9540 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | replimd 9541 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remimd 9542 | Value of the conjugate of a complex number. The value is the real part minus times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjcjd 9543 | 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 9544 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | rerebd 9545 | 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 9546 | 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 9547 | A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 9548 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjap0d 9548 | A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# # | ||
Theorem | recjd 9549 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcjd 9550 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulrcld 9551 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulvald 9552 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulge0d 9553 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | renegd 9554 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imnegd 9555 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjnegd 9556 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | addcjd 9557 | 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.) |
Theorem | cjexpd 9558 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | readdd 9559 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imaddd 9560 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | resubd 9561 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imsubd 9562 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remuld 9563 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immuld 9564 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjaddd 9565 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmuld 9566 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | ipcnd 9567 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjdivapd 9568 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | rered 9569 | 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 9570 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjred 9571 | 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 9572 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immul2d 9573 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | redivapd 9574 | Real part of a division. Related to remul2 9473. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | imdivapd 9575 | Imaginary part of a division. Related to remul2 9473. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | crred 9576 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | crimd 9577 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | caucvgrelemrec 9578* | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
# | ||
Theorem | caucvgrelemcau 9579* | Lemma for caucvgre 9580. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
Theorem | caucvgre 9580* |
Convergence of real sequences.
A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.) |
Theorem | cvg1nlemcxze 9581 | Lemma for cvg1n 9585. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | cvg1nlemf 9582* | Lemma for cvg1n 9585. The modified sequence is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1nlemcau 9583* | Lemma for cvg1n 9585. By selecting spaced out terms for the modified sequence , the terms are within (without the constant ). (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1nlemres 9584* | Lemma for cvg1n 9585. The original sequence has a limit (turns out it is the same as the limit of the modified sequence ). (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1n 9585* |
Convergence of real sequences.
This is a version of caucvgre 9580 with a constant multiplier on the rate of convergence. That is, all terms after the nth term must be within of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | uzin2 9586 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
Theorem | rexanuz 9587* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
Theorem | rexuz3 9588* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | rexanuz2 9589* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | r19.29uz 9590* | A version of 19.29 1511 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
Theorem | r19.2uz 9591* | A version of r19.2m 3309 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
Theorem | recvguniqlem 9592 | Lemma for recvguniq 9593. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
Theorem | recvguniq 9593* | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Syntax | csqrt 9594 | Extend class notation to include square root of a complex number. |
Syntax | cabs 9595 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
Definition | df-rsqrt 9596* |
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.) |
Definition | df-abs 9597 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
Theorem | sqrtrval 9598* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
Theorem | absval 9599 | 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.) |
Theorem | rennim 9600 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |