Theorem List for Intuitionistic Logic Explorer - 10601-10700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | hashfzo0 10601 |
Cardinality of a half-open set of integers based at zero. (Contributed by
Stefan O'Rear, 15-Aug-2015.)
|
![( (](lp.gif) ♯![` `](backtick.gif) ![( (](lp.gif) ..^![B B](_cb.gif) ![) )](rp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | hashfzp1 10602 |
Value of the numeric cardinality of a (possibly empty) integer range.
(Contributed by AV, 19-Jun-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ♯![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | hashfz0 10603 |
Value of the numeric cardinality of a nonempty range of nonnegative
integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|
![( (](lp.gif) ♯![` `](backtick.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![B
B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | hashxp 10604 |
The size of the Cartesian product of two finite sets is the product of
their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)
|
![( (](lp.gif) ![( (](lp.gif) ![Fin Fin](_fin.gif) ♯![`
`](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ♯![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fimaxq 10605* |
A finite set of rational numbers has a maximum. (Contributed by Jim
Kingdon, 6-Sep-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![) )](rp.gif) |
|
Theorem | resunimafz0 10606 |
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.)
|
![( (](lp.gif) ![I I](_ci.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ..^ ♯![` `](backtick.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![I I](_ci.gif) ![( (](lp.gif) ![( (](lp.gif) ..^ ♯![` `](backtick.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![I I](_ci.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnfz0hash 10607 |
The size of a function on a finite set of sequential nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Jun-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ♯![`
`](backtick.gif) ![F F](_cf.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ffz0hash 10608 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![0 0](0.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ♯![`
`](backtick.gif) ![F F](_cf.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ffzo0hash 10609 |
The size of a function on a half-open range of nonnegative integers.
(Contributed by Alexander van der Vekens, 25-Mar-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ♯![` `](backtick.gif) ![F F](_cf.gif) ![N N](_cn.gif) ![) )](rp.gif) |
|
Theorem | fnfzo0hash 10610 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ♯![`
`](backtick.gif) ![F F](_cf.gif) ![N N](_cn.gif) ![) )](rp.gif) |
|
Theorem | hashfacen 10611* |
The number of bijections between two sets is a cardinal invariant.
(Contributed by Mario Carneiro, 21-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![{ {](lbrace.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![C C](_cc.gif) ![{ {](lbrace.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![D D](_cd.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | leisorel 10612 |
Version of isorel 5717 for strictly increasing functions on the
reals.
(Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro,
9-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![( (](lp.gif)
![RR* RR*](_bbrast.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![C C](_cc.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zfz1isolemsplit 10613 |
Lemma for zfz1iso 10616. Removing one element from an integer
range.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
![( (](lp.gif) ![Fin Fin](_fin.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![M M](_cm.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ♯![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zfz1isolemiso 10614* |
Lemma for zfz1iso 10616. Adding one element to the order
isomorphism.
(Contributed by Jim Kingdon, 8-Sep-2022.)
|
![( (](lp.gif) ![Fin Fin](_fin.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![...
...](ldots.gif) ♯![`
`](backtick.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![M M](_cm.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![M M](_cm.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ♯![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif)
![M M](_cm.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ♯![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif)
![M M](_cm.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zfz1isolem1 10615* |
Lemma for zfz1iso 10616. Existence of an order isomorphism given
the
existence of shorter isomorphisms. (Contributed by Jim Kingdon,
7-Sep-2022.)
|
![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![Fin Fin](_fin.gif) ![K K](_ck.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![Fin Fin](_fin.gif) ![( (](lp.gif)
![K K](_ck.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![M M](_cm.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![) )](rp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zfz1iso 10616* |
A finite set of integers has an order isomorphism to a one-based finite
sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![Fin Fin](_fin.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![...
...](ldots.gif) ♯![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | seq3coll 10617* |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![k k](_k.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![Z Z](_cz.gif)
![k k](_k.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif)
![n n](_n.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![n n](_n.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq
seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![1 1](1.gif)
![H H](_ch.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.7 Elementary real and complex
functions
|
|
4.7.1 The "shift" operation
|
|
Syntax | cshi 10618 |
Extend class notation with function shifter.
|
![shift shift](_shift.gif) |
|
Definition | df-shft 10619* |
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 10629 for its value. (Contributed by NM,
20-Jul-2005.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif)
![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![f f](_f.gif) ![z z](_z.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | shftlem 10620* |
Two ways to write a shifted set ![( (](lp.gif) ![A A](_ca.gif) . (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![{ {](lbrace.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | shftuz 10621* |
A shift of the upper integers. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftfvalg 10622* |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![A A](_ca.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | ovshftex 10623 |
Existence of the result of applying shift. (Contributed by Jim Kingdon,
15-Aug-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | shftfibg 10624 |
Value of a fiber of the relation . (Contributed by Jim Kingdon,
15-Aug-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | shftfval 10625* |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | shftdm 10626* |
Domain of a relation shifted by . The set on the right is more
commonly notated as ![( (](lp.gif) ![A A](_ca.gif)
(meaning add to every
element of ).
(Contributed by Mario Carneiro, 3-Nov-2013.)
|
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif)
![{ {](lbrace.gif)
![( (](lp.gif) ![A A](_ca.gif)
![F F](_cf.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | shftfib 10627 |
Value of a fiber of the relation . (Contributed by Mario
Carneiro, 4-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) !["
"](backquote.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![F F](_cf.gif) !["
"](backquote.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | shftfn 10628* |
Functionality and domain of a sequence shifted by . (Contributed
by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![{
{](lbrace.gif) ![( (](lp.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | shftval 10629 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftval2 10630 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftval3 10631 |
Value of a sequence shifted by . (Contributed by NM,
20-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftval4 10632 |
Value of a sequence shifted by ![-u -u](shortminus.gif) .
(Contributed by NM,
18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | shftval5 10633 |
Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftf 10634* |
Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif)
![CC CC](bbc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | 2shfti 10635 |
Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftidt2 10636 |
Identity law for the shift operation. (Contributed by Mario Carneiro,
5-Nov-2013.)
|
![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | shftidt 10637 |
Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.)
(Revised by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftcan1 10638 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![` `](backtick.gif) ![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftcan2 10639 |
Cancellation law for the shift operation. (Contributed by NM,
4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![A A](_ca.gif) ![) )](rp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftvalg 10640 |
Value of a sequence shifted by . (Contributed by Scott Fenton,
16-Dec-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | shftval4g 10641 |
Value of a sequence shifted by ![-u -u](shortminus.gif) .
(Contributed by Jim Kingdon,
19-Aug-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![` `](backtick.gif) ![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | seq3shft 10642* |
Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.)
(Revised by Jim Kingdon, 17-Oct-2022.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif)
![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M
M](_cm.gif) ![( (](lp.gif)
![N N](_cn.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![( (](lp.gif)
![N N](_cn.gif) ![) )](rp.gif)
![F F](_cf.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.7.2 Real and imaginary parts;
conjugate
|
|
Syntax | ccj 10643 |
Extend class notation to include complex conjugate function.
|
![* *](ast.gif) |
|
Syntax | cre 10644 |
Extend class notation to include real part of a complex number.
|
![Re Re](re.gif) |
|
Syntax | cim 10645 |
Extend class notation to include imaginary part of a complex number.
|
![Im Im](im.gif) |
|
Definition | df-cj 10646* |
Define the complex conjugate function. See cjcli 10717 for its closure and
cjval 10649 for its value. (Contributed by NM,
9-May-1999.) (Revised by
Mario Carneiro, 6-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![iota_ iota_](_riotabar.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![RR
RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-re 10647 |
Define a function whose value is the real part of a complex number. See
reval 10653 for its value, recli 10715 for its closure, and replim 10663 for its use
in decomposing a complex number. (Contributed by NM, 9-May-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-im 10648 |
Define a function whose value is the imaginary part of a complex number.
See imval 10654 for its value, imcli 10716 for its closure, and replim 10663 for its
use in decomposing a complex number. (Contributed by NM,
9-May-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![_i _i](rmi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjval 10649* |
The value of the conjugate of a complex number. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![iota_ iota_](_riotabar.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif)
![RR RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjth 10650 |
The defining property of the complex conjugate. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjf 10651 |
Domain and codomain of the conjugate function. (Contributed by Mario
Carneiro, 6-Nov-2013.)
|
![* *](ast.gif) ![: :](colon.gif) ![CC CC](bbc.gif) ![--> -->](longrightarrow.gif) ![CC CC](bbc.gif) |
|
Theorem | cjcl 10652 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | reval 10653 |
The value of the real part of a complex number. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imval 10654 |
The value of the imaginary part of a complex number. (Contributed by
NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif) ![_i _i](rmi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imre 10655 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reim 10656 |
The real part of a complex number in terms of the imaginary part
function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | recl 10657 |
The real part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | imcl 10658 |
The imaginary part of a complex number is real. (Contributed by NM,
9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | ref 10659 |
Domain and codomain of the real part function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
![Re Re](re.gif) ![: :](colon.gif) ![CC CC](bbc.gif) ![--> -->](longrightarrow.gif) ![RR RR](bbr.gif) |
|
Theorem | imf 10660 |
Domain and codomain of the imaginary part function. (Contributed by
Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
|
![Im Im](im.gif) ![: :](colon.gif) ![CC CC](bbc.gif) ![--> -->](longrightarrow.gif) ![RR RR](bbr.gif) |
|
Theorem | crre 10661 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | crim 10662 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | replim 10663 |
Reconstruct a complex number from its real and imaginary parts.
(Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | remim 10664 |
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 NM, 10-May-1999.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reim0 10665 |
The imaginary part of a real number is 0. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | reim0b 10666 |
A number is real iff its imaginary part is 0. (Contributed by NM,
26-Sep-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | rereb 10667 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulreap 10668 |
A product with a real multiplier apart from zero is real iff the
multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
|
![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![RR
RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | rere 10669 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | cjreb 10670 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | recj 10671 |
Real part of a complex conjugate. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reneg 10672 |
Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![Re Re](re.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | readd 10673 |
Real part distributes over addition. (Contributed by NM, 17-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | resub 10674 |
Real part distributes over subtraction. (Contributed by NM,
17-Mar-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | remullem 10675 |
Lemma for remul 10676, immul 10683, and cjmul 10689. (Contributed by NM,
28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | remul 10676 |
Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by
Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | remul2 10677 |
Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | redivap 10678 |
Real part of a division. Related to remul2 10677. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imcj 10679 |
Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imneg 10680 |
The imaginary part of a negative number. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![Im Im](im.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imadd 10681 |
Imaginary part distributes over addition. (Contributed by NM,
18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imsub 10682 |
Imaginary part distributes over subtraction. (Contributed by NM,
18-Mar-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | immul 10683 |
Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised
by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | immul2 10684 |
Imaginary part of a product. (Contributed by Mario Carneiro,
2-Aug-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imdivap 10685 |
Imaginary part of a division. Related to immul2 10684. (Contributed by Jim
Kingdon, 14-Jun-2020.)
|
![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjre 10686 |
A real number equals its complex conjugate. Proposition 10-3.4(f) of
[Gleason] p. 133. (Contributed by NM,
8-Oct-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | cjcj 10687 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | cjadd 10688 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjmul 10689 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ipcnval 10690 |
Standard inner product on complex numbers. (Contributed by NM,
29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjmulrcl 10691 |
A complex number times its conjugate is real. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | cjmulval 10692 |
A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjmulge0 10693 |
A complex number times its conjugate is nonnegative. (Contributed by NM,
26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjneg 10694 |
Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addcj 10695 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjsub 10696 |
Complex conjugate distributes over subtraction. (Contributed by NM,
28-Apr-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjexp 10697 |
Complex conjugate of positive integer exponentiation. (Contributed by
NM, 7-Jun-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imval2 10698 |
The imaginary part of a number in terms of complex conjugate.
(Contributed by NM, 30-Apr-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![_i _i](rmi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | re0 10699 |
The real part of zero. (Contributed by NM, 27-Jul-1999.)
|
![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![0 0](0.gif) ![0 0](0.gif) |
|
Theorem | im0 10700 |
The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![0 0](0.gif) ![0 0](0.gif) |