Type | Label | Description |
Statement |
|
Theorem | hashfzo 10801 |
Cardinality of a half-open set of integers. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
β’ (π΅ β (β€β₯βπ΄) β (β―β(π΄..^π΅)) = (π΅ β π΄)) |
|
Theorem | hashfzo0 10802 |
Cardinality of a half-open set of integers based at zero. (Contributed by
Stefan O'Rear, 15-Aug-2015.)
|
β’ (π΅ β β0 β
(β―β(0..^π΅)) =
π΅) |
|
Theorem | hashfzp1 10803 |
Value of the numeric cardinality of a (possibly empty) integer range.
(Contributed by AV, 19-Jun-2021.)
|
β’ (π΅ β (β€β₯βπ΄) β (β―β((π΄ + 1)...π΅)) = (π΅ β π΄)) |
|
Theorem | hashfz0 10804 |
Value of the numeric cardinality of a nonempty range of nonnegative
integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|
β’ (π΅ β β0 β
(β―β(0...π΅)) =
(π΅ + 1)) |
|
Theorem | hashxp 10805 |
The size of the Cartesian product of two finite sets is the product of
their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)
|
β’ ((π΄ β Fin β§ π΅ β Fin) β (β―β(π΄ Γ π΅)) = ((β―βπ΄) Β· (β―βπ΅))) |
|
Theorem | fimaxq 10806* |
A finite set of rational numbers has a maximum. (Contributed by Jim
Kingdon, 6-Sep-2022.)
|
β’ ((π΄ β β β§ π΄ β Fin β§ π΄ β β
) β βπ₯ β π΄ βπ¦ β π΄ π¦ β€ π₯) |
|
Theorem | fiubm 10807* |
Lemma for fiubz 10808 and fiubnn 10809. A general form of those theorems.
(Contributed by Jim Kingdon, 29-Oct-2024.)
|
β’ (π β π΄ β π΅)
& β’ (π β π΅ β β) & β’ (π β πΆ β π΅)
& β’ (π β π΄ β Fin) β β’ (π β βπ₯ β π΅ βπ¦ β π΄ π¦ β€ π₯) |
|
Theorem | fiubz 10808* |
A finite set of integers has an upper bound which is an integer.
(Contributed by Jim Kingdon, 29-Oct-2024.)
|
β’ ((π΄ β β€ β§ π΄ β Fin) β βπ₯ β β€ βπ¦ β π΄ π¦ β€ π₯) |
|
Theorem | fiubnn 10809* |
A finite set of natural numbers has an upper bound which is a a natural
number. (Contributed by Jim Kingdon, 29-Oct-2024.)
|
β’ ((π΄ β β β§ π΄ β Fin) β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) |
|
Theorem | resunimafz0 10810 |
The union of a restriction by an image over an open range of nonnegative
integers and a singleton of an ordered pair is a restriction by an image
over an interval of nonnegative integers. (Contributed by Mario
Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)
|
β’ (π β Fun πΌ)
& β’ (π β πΉ:(0..^(β―βπΉ))βΆdom πΌ)
& β’ (π β π β (0..^(β―βπΉ)))
β β’ (π β (πΌ βΎ (πΉ β (0...π))) = ((πΌ βΎ (πΉ β (0..^π))) βͺ {β¨(πΉβπ), (πΌβ(πΉβπ))β©})) |
|
Theorem | fnfz0hash 10811 |
The size of a function on a finite set of sequential nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Jun-2018.)
|
β’ ((π β β0 β§ πΉ Fn (0...π)) β (β―βπΉ) = (π + 1)) |
|
Theorem | ffz0hash 10812 |
The size of a function on a finite set of sequential nonnegative integers
equals the upper bound of the sequence increased by 1. (Contributed by
Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV,
11-Apr-2021.)
|
β’ ((π β β0 β§ πΉ:(0...π)βΆπ΅) β (β―βπΉ) = (π + 1)) |
|
Theorem | ffzo0hash 10813 |
The size of a function on a half-open range of nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Mar-2018.)
|
β’ ((π β β0 β§ πΉ Fn (0..^π)) β (β―βπΉ) = π) |
|
Theorem | fnfzo0hash 10814 |
The size of a function on a half-open range of nonnegative integers equals
the upper bound of this range. (Contributed by Alexander van der Vekens,
26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.)
|
β’ ((π β β0 β§ πΉ:(0..^π)βΆπ΅) β (β―βπΉ) = π) |
|
Theorem | hashfacen 10815* |
The number of bijections between two sets is a cardinal invariant.
(Contributed by Mario Carneiro, 21-Jan-2015.)
|
β’ ((π΄ β π΅ β§ πΆ β π·) β {π β£ π:π΄β1-1-ontoβπΆ} β {π β£ π:π΅β1-1-ontoβπ·}) |
|
Theorem | leisorel 10816 |
Version of isorel 5808 for strictly increasing functions on the
reals.
(Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro,
9-Sep-2015.)
|
β’ ((πΉ Isom < , < (π΄, π΅) β§ (π΄ β β* β§ π΅ β β*)
β§ (πΆ β π΄ β§ π· β π΄)) β (πΆ β€ π· β (πΉβπΆ) β€ (πΉβπ·))) |
|
Theorem | zfz1isolemsplit 10817 |
Lemma for zfz1iso 10820. Removing one element from an integer
range.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
β’ (π β π β Fin) & β’ (π β π β π) β β’ (π β (1...(β―βπ)) =
((1...(β―β(π
β {π}))) βͺ
{(β―βπ)})) |
|
Theorem | zfz1isolemiso 10818* |
Lemma for zfz1iso 10820. Adding one element to the order
isomorphism.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
β’ (π β π β Fin) & β’ (π β π β β€) & β’ (π β π β π)
& β’ (π β βπ§ β π π§ β€ π)
& β’ (π β πΊ Isom < , <
((1...(β―β(π
β {π}))), (π β {π}))) & β’ (π β π΄ β (1...(β―βπ))) & β’ (π β π΅ β (1...(β―βπ)))
β β’ (π β (π΄ < π΅ β ((πΊ βͺ {β¨(β―βπ), πβ©})βπ΄) < ((πΊ βͺ {β¨(β―βπ), πβ©})βπ΅))) |
|
Theorem | zfz1isolem1 10819* |
Lemma for zfz1iso 10820. Existence of an order isomorphism given
the
existence of shorter isomorphisms. (Contributed by Jim Kingdon,
7-Sep-2022.)
|
β’ (π β πΎ β Ο) & β’ (π β βπ¦(((π¦ β β€ β§ π¦ β Fin) β§ π¦ β πΎ) β βπ π Isom < , < ((1...(β―βπ¦)), π¦))) & β’ (π β π β β€) & β’ (π β π β Fin) & β’ (π β π β suc πΎ)
& β’ (π β π β π)
& β’ (π β βπ§ β π π§ β€ π) β β’ (π β βπ π Isom < , < ((1...(β―βπ)), π)) |
|
Theorem | zfz1iso 10820* |
A finite set of integers has an order isomorphism to a one-based finite
sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
|
β’ ((π΄ β β€ β§ π΄ β Fin) β βπ π Isom < , < ((1...(β―βπ΄)), π΄)) |
|
Theorem | seq3coll 10821* |
The function πΉ contains a sparse set of nonzero
values to be summed.
The function πΊ is an order isomorphism from the set
of nonzero
values of πΉ to a 1-based finite sequence, and
π»
collects these
nonzero values together. Under these conditions, the sum over the
values in π» yields the same result as the sum
over the original set
πΉ. (Contributed by Mario Carneiro,
2-Apr-2014.) (Revised by Jim
Kingdon, 9-Apr-2023.)
|
β’ ((π β§ π β π) β (π + π) = π)
& β’ ((π β§ π β π) β (π + π) = π)
& β’ ((π β§ (π β π β§ π β π)) β (π + π) β π)
& β’ (π β π β π)
& β’ (π β πΊ Isom < , <
((1...(β―βπ΄)),
π΄)) & β’ (π β π β (1...(β―βπ΄))) & β’ (π β π΄ β
(β€β₯βπ)) & β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β π)
& β’ ((π β§ π β (β€β₯β1))
β (π»βπ) β π)
& β’ ((π β§ π β ((π...(πΊβ(β―βπ΄))) β π΄)) β (πΉβπ) = π)
& β’ ((π β§ π β (1...(β―βπ΄))) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seqπ( + , πΉ)β(πΊβπ)) = (seq1( + , π»)βπ)) |
|
4.7 Elementary real and complex
functions
|
|
4.7.1 The "shift" operation
|
|
Syntax | cshi 10822 |
Extend class notation with function shifter.
|
class shift |
|
Definition | df-shft 10823* |
Define a function shifter. This operation offsets the value argument of
a function (ordinarily on a subset of β)
and produces a new
function on β. See shftval 10833 for its value. (Contributed by NM,
20-Jul-2005.)
|
β’ shift = (π β V, π₯ β β β¦ {β¨π¦, π§β© β£ (π¦ β β β§ (π¦ β π₯)ππ§)}) |
|
Theorem | shftlem 10824* |
Two ways to write a shifted set (π΅ + π΄). (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β β§ π΅ β β) β {π₯ β β β£ (π₯ β π΄) β π΅} = {π₯ β£ βπ¦ β π΅ π₯ = (π¦ + π΄)}) |
|
Theorem | shftuz 10825* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
β’ ((π΄ β β€ β§ π΅ β β€) β {π₯ β β β£ (π₯ β π΄) β
(β€β₯βπ΅)} = (β€β₯β(π΅ + π΄))) |
|
Theorem | shftfvalg 10826* |
The value of the sequence shifter operation is a function on β.
π΄ is ordinarily an integer.
(Contributed by NM, 20-Jul-2005.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β β§ πΉ β π) β (πΉ shift π΄) = {β¨π₯, π¦β© β£ (π₯ β β β§ (π₯ β π΄)πΉπ¦)}) |
|
Theorem | ovshftex 10827 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
β’ ((πΉ β π β§ π΄ β β) β (πΉ shift π΄) β V) |
|
Theorem | shftfibg 10828 |
Value of a fiber of the relation πΉ. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
β’ ((πΉ β π β§ π΄ β β β§ π΅ β β) β ((πΉ shift π΄) β {π΅}) = (πΉ β {(π΅ β π΄)})) |
|
Theorem | shftfval 10829* |
The value of the sequence shifter operation is a function on β.
π΄ is ordinarily an integer.
(Contributed by NM, 20-Jul-2005.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ πΉ β V β β’ (π΄ β β β (πΉ shift π΄) = {β¨π₯, π¦β© β£ (π₯ β β β§ (π₯ β π΄)πΉπ¦)}) |
|
Theorem | shftdm 10830* |
Domain of a relation shifted by π΄. The set on the right is more
commonly notated as (dom πΉ + π΄) (meaning add π΄ to every
element of dom πΉ). (Contributed by Mario Carneiro,
3-Nov-2013.)
|
β’ πΉ β V β β’ (π΄ β β β dom (πΉ shift π΄) = {π₯ β β β£ (π₯ β π΄) β dom πΉ}) |
|
Theorem | shftfib 10831 |
Value of a fiber of the relation πΉ. (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄) β {π΅}) = (πΉ β {(π΅ β π΄)})) |
|
Theorem | shftfn 10832* |
Functionality and domain of a sequence shifted by π΄. (Contributed
by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ πΉ β V β β’ ((πΉ Fn π΅ β§ π΄ β β) β (πΉ shift π΄) Fn {π₯ β β β£ (π₯ β π΄) β π΅}) |
|
Theorem | shftval 10833 |
Value of a sequence shifted by π΄. (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄)βπ΅) = (πΉβ(π΅ β π΄))) |
|
Theorem | shftval2 10834 |
Value of a sequence shifted by π΄ β π΅. (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((πΉ shift (π΄ β π΅))β(π΄ + πΆ)) = (πΉβ(π΅ + πΆ))) |
|
Theorem | shftval3 10835 |
Value of a sequence shifted by π΄ β π΅. (Contributed by NM,
20-Jul-2005.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift (π΄ β π΅))βπ΄) = (πΉβπ΅)) |
|
Theorem | shftval4 10836 |
Value of a sequence shifted by -π΄. (Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift -π΄)βπ΅) = (πΉβ(π΄ + π΅))) |
|
Theorem | shftval5 10837 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄)β(π΅ + π΄)) = (πΉβπ΅)) |
|
Theorem | shftf 10838* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ ((πΉ:π΅βΆπΆ β§ π΄ β β) β (πΉ shift π΄):{π₯ β β β£ (π₯ β π΄) β π΅}βΆπΆ) |
|
Theorem | 2shfti 10839 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β ((πΉ shift π΄) shift π΅) = (πΉ shift (π΄ + π΅))) |
|
Theorem | shftidt2 10840 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
β’ πΉ β V β β’ (πΉ shift 0) = (πΉ βΎ β) |
|
Theorem | shftidt 10841 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ (π΄ β β β ((πΉ shift 0)βπ΄) = (πΉβπ΄)) |
|
Theorem | shftcan1 10842 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift π΄) shift -π΄)βπ΅) = (πΉβπ΅)) |
|
Theorem | shftcan2 10843 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift -π΄) shift π΄)βπ΅) = (πΉβπ΅)) |
|
Theorem | shftvalg 10844 |
Value of a sequence shifted by π΄. (Contributed by Scott Fenton,
16-Dec-2017.)
|
β’ ((πΉ β π β§ π΄ β β β§ π΅ β β) β ((πΉ shift π΄)βπ΅) = (πΉβ(π΅ β π΄))) |
|
Theorem | shftval4g 10845 |
Value of a sequence shifted by -π΄. (Contributed by Jim Kingdon,
19-Aug-2021.)
|
β’ ((πΉ β π β§ π΄ β β β§ π΅ β β) β ((πΉ shift -π΄)βπ΅) = (πΉβ(π΄ + π΅))) |
|
Theorem | seq3shft 10846* |
Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.)
(Revised by Jim Kingdon, 17-Oct-2022.)
|
β’ (π β πΉ β π)
& β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π₯ β (β€β₯β(π β π))) β (πΉβπ₯) β π)
& β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) β β’ (π β seqπ( + , (πΉ shift π)) = (seq(π β π)( + , πΉ) shift π)) |
|
4.7.2 Real and imaginary parts;
conjugate
|
|
Syntax | ccj 10847 |
Extend class notation to include complex conjugate function.
|
class β |
|
Syntax | cre 10848 |
Extend class notation to include real part of a complex number.
|
class β |
|
Syntax | cim 10849 |
Extend class notation to include imaginary part of a complex number.
|
class β |
|
Definition | df-cj 10850* |
Define the complex conjugate function. See cjcli 10921 for its closure and
cjval 10853 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
β’ β = (π₯ β β β¦ (β©π¦ β β ((π₯ + π¦) β β β§ (i Β· (π₯ β π¦)) β β))) |
|
Definition | df-re 10851 |
Define a function whose value is the real part of a complex number. See
reval 10857 for its value, recli 10919 for its closure, and replim 10867 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
β’ β = (π₯ β β β¦ ((π₯ + (ββπ₯)) / 2)) |
|
Definition | df-im 10852 |
Define a function whose value is the imaginary part of a complex number.
See imval 10858 for its value, imcli 10920 for its closure, and replim 10867 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
β’ β = (π₯ β β β¦ (ββ(π₯ / i))) |
|
Theorem | cjval 10853* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
β’ (π΄ β β β
(ββπ΄) =
(β©π₯ β
β ((π΄ + π₯) β β β§ (i
Β· (π΄ β π₯)) β
β))) |
|
Theorem | cjth 10854 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
β’ (π΄ β β β ((π΄ + (ββπ΄)) β β β§ (i Β· (π΄ β (ββπ΄))) β
β)) |
|
Theorem | cjf 10855 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
β’
β:ββΆβ |
|
Theorem | cjcl 10856 |
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.)
|
β’ (π΄ β β β
(ββπ΄) β
β) |
|
Theorem | reval 10857 |
The value of the real part of a complex number. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
β’ (π΄ β β β (ββπ΄) = ((π΄ + (ββπ΄)) / 2)) |
|
Theorem | imval 10858 |
The value of the imaginary part of a complex number. (Contributed by
NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
β’ (π΄ β β β (ββπ΄) = (ββ(π΄ / i))) |
|
Theorem | imre 10859 |
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.)
|
β’ (π΄ β β β (ββπ΄) = (ββ(-i Β·
π΄))) |
|
Theorem | reim 10860 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
β’ (π΄ β β β (ββπ΄) = (ββ(i Β·
π΄))) |
|
Theorem | recl 10861 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
β’ (π΄ β β β (ββπ΄) β
β) |
|
Theorem | imcl 10862 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
β’ (π΄ β β β (ββπ΄) β
β) |
|
Theorem | ref 10863 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
β’
β:ββΆβ |
|
Theorem | imf 10864 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
β’
β:ββΆβ |
|
Theorem | crre 10865 |
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.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ + (i
Β· π΅))) = π΄) |
|
Theorem | crim 10866 |
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.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ + (i
Β· π΅))) = π΅) |
|
Theorem | replim 10867 |
Reconstruct a complex number from its real and imaginary parts.
(Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
β’ (π΄ β β β π΄ = ((ββπ΄) + (i Β· (ββπ΄)))) |
|
Theorem | remim 10868 |
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.)
|
β’ (π΄ β β β
(ββπ΄) =
((ββπ΄) β
(i Β· (ββπ΄)))) |
|
Theorem | reim0 10869 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
β’ (π΄ β β β (ββπ΄) = 0) |
|
Theorem | reim0b 10870 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
β’ (π΄ β β β (π΄ β β β (ββπ΄) = 0)) |
|
Theorem | rereb 10871 |
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.)
|
β’ (π΄ β β β (π΄ β β β (ββπ΄) = π΄)) |
|
Theorem | mulreap 10872 |
A product with a real multiplier apart from zero is real iff the
multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
|
β’ ((π΄ β β β§ π΅ β β β§ π΅ # 0) β (π΄ β β β (π΅ Β· π΄) β β)) |
|
Theorem | rere 10873 |
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.)
|
β’ (π΄ β β β (ββπ΄) = π΄) |
|
Theorem | cjreb 10874 |
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.)
|
β’ (π΄ β β β (π΄ β β β
(ββπ΄) = π΄)) |
|
Theorem | recj 10875 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
β’ (π΄ β β β
(ββ(ββπ΄)) = (ββπ΄)) |
|
Theorem | reneg 10876 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) |
|
Theorem | readd 10877 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) |
|
Theorem | resub 10878 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ β
π΅)) = ((ββπ΄) β (ββπ΅))) |
|
Theorem | remullem 10879 |
Lemma for remul 10880, immul 10887, and cjmul 10893. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
((ββ(π΄ Β·
π΅)) =
(((ββπ΄)
Β· (ββπ΅))
β ((ββπ΄)
Β· (ββπ΅))) β§ (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅))) β§ (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅)))) |
|
Theorem | remul 10880 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ Β·
π΅)) =
(((ββπ΄)
Β· (ββπ΅))
β ((ββπ΄)
Β· (ββπ΅)))) |
|
Theorem | remul2 10881 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ Β·
π΅)) = (π΄ Β· (ββπ΅))) |
|
Theorem | redivap 10882 |
Real part of a division. Related to remul2 10881. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
β’ ((π΄ β β β§ π΅ β β β§ π΅ # 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / π΅)) |
|
Theorem | imcj 10883 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ (π΄ β β β
(ββ(ββπ΄)) = -(ββπ΄)) |
|
Theorem | imneg 10884 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ (π΄ β β β
(ββ-π΄) =
-(ββπ΄)) |
|
Theorem | imadd 10885 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) |
|
Theorem | imsub 10886 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ β
π΅)) =
((ββπ΄) β
(ββπ΅))) |
|
Theorem | immul 10887 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ Β·
π΅)) =
(((ββπ΄)
Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅)))) |
|
Theorem | immul2 10888 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ Β·
π΅)) = (π΄ Β· (ββπ΅))) |
|
Theorem | imdivap 10889 |
Imaginary part of a division. Related to immul2 10888. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
β’ ((π΄ β β β§ π΅ β β β§ π΅ # 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / π΅)) |
|
Theorem | cjre 10890 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
β’ (π΄ β β β
(ββπ΄) = π΄) |
|
Theorem | cjcj 10891 |
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.)
|
β’ (π΄ β β β
(ββ(ββπ΄)) = π΄) |
|
Theorem | cjadd 10892 |
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.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) |
|
Theorem | cjmul 10893 |
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.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄
Β· π΅)) =
((ββπ΄)
Β· (ββπ΅))) |
|
Theorem | ipcnval 10894 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ Β·
(ββπ΅))) =
(((ββπ΄)
Β· (ββπ΅))
+ ((ββπ΄)
Β· (ββπ΅)))) |
|
Theorem | cjmulrcl 10895 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ (π΄ β β β (π΄ Β· (ββπ΄)) β β) |
|
Theorem | cjmulval 10896 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ (π΄ β β β (π΄ Β· (ββπ΄)) = (((ββπ΄)β2) + ((ββπ΄)β2))) |
|
Theorem | cjmulge0 10897 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ (π΄ β β β 0 β€ (π΄ Β· (ββπ΄))) |
|
Theorem | cjneg 10898 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
β’ (π΄ β β β
(ββ-π΄) =
-(ββπ΄)) |
|
Theorem | addcj 10899 |
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.)
|
β’ (π΄ β β β (π΄ + (ββπ΄)) = (2 Β· (ββπ΄))) |
|
Theorem | cjsub 10900 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
β’ ((π΄ β β β§ π΅ β β) β
(ββ(π΄ β
π΅)) =
((ββπ΄)
β (ββπ΅))) |