Theorem List for Intuitionistic Logic Explorer - 11101-11200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | climmpt 11101* |
Exhibit a function
with the same convergence properties as the
not-quite-function . (Contributed by Mario Carneiro,
31-Jan-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2clim 11102* |
If two sequences converge to each other, they converge to the same
limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario
Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![j j](_j.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | climshftlemg 11103 |
A shifted function converges if the original function converges.
(Contributed by Mario Carneiro, 5-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif)
![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | climres 11104 |
A function restricted to upper integers converges iff the original
function converges. (Contributed by Mario Carneiro, 13-Jul-2013.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climshft 11105 |
A shifted function converges iff the original function converges.
(Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro,
31-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | serclim0 11106 |
The zero series converges to zero. (Contributed by Paul Chapman,
9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![{ {](lbrace.gif) ![0 0](0.gif) ![} }](rbrace.gif) ![) )](rp.gif)
![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | climshft2 11107* |
A shifted function converges iff the original function converges.
(Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario
Carneiro, 6-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climabs0 11108* |
Convergence to zero of the absolute value is equivalent to convergence
to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro,
31-Jan-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climcn1 11109* |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![z z](_z.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![(
(](lp.gif)
![RR+ RR+](_bbrplus.gif)
![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climcn2 11110* |
Image of a limit under a continuous map, two-arg version. (Contributed
by Mario Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![v v](_v.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![(
(](lp.gif)
![RR+ RR+](_bbrplus.gif)
![E. E.](exists.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![z
z](_z.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![v v](_v.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addcn2 11111* |
Complex number addition is a continuous function. Part of Proposition
14-4.16 of [Gleason] p. 243. (We write
out the definition directly
because df-cn and df-cncf are not yet available to us. See addcncntop 12760
for the abbreviated version.) (Contributed by Mario Carneiro,
31-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif)
![z z](_z.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subcn2 11112* |
Complex number subtraction is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by Mario
Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif)
![z z](_z.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulcn2 11113* |
Complex number multiplication is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by Mario
Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif)
![z z](_z.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reccn2ap 11114* |
The reciprocal function is continuous. The class is just for
convenience in writing the proof and typically would be passed in as an
instance of eqid 2140. (Contributed by Mario Carneiro,
9-Feb-2014.)
Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.)
|
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) #
![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cn1lem 11115* |
A sufficient condition for a function to be continuous. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
![F F](_cf.gif) ![: :](colon.gif) ![CC CC](bbc.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![(
(](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | abscn2 11116* |
The absolute value function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cjcn2 11117* |
The complex conjugate function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![z z](_z.gif)
![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | recn2 11118* |
The real part function is continuous. (Contributed by Mario Carneiro,
9-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![z z](_z.gif)
![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | imcn2 11119* |
The imaginary part function is continuous. (Contributed by Mario
Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![z z](_z.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climcn1lem 11120* |
The limit of a continuous function, theorem form. (Contributed by
Mario Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![H H](_ch.gif) ![: :](colon.gif) ![CC CC](bbc.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![z z](_z.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climabs 11121* |
Limit of the absolute value of a sequence. Proposition 12-2.4(c) of
[Gleason] p. 172. (Contributed by NM,
7-Jun-2006.) (Revised by Mario
Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | climcj 11122* |
Limit of the complex conjugate of a sequence. Proposition 12-2.4(c)
of [Gleason] p. 172. (Contributed by
NM, 7-Jun-2006.) (Revised by
Mario Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![* *](ast.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climre 11123* |
Limit of the real part of a sequence. Proposition 12-2.4(c) of
[Gleason] p. 172. (Contributed by NM,
7-Jun-2006.) (Revised by Mario
Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![Re Re](re.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climim 11124* |
Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of
[Gleason] p. 172. (Contributed by NM,
7-Jun-2006.) (Revised by Mario
Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![Im Im](im.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climrecl 11125* |
The limit of a convergent real sequence is real. Corollary 12-2.5 of
[Gleason] p. 172. (Contributed by NM,
10-Sep-2005.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | climge0 11126* |
A nonnegative sequence converges to a nonnegative number. (Contributed
by NM, 11-Sep-2005.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | climadd 11127* |
Limit of the sum of two converging sequences. Proposition 12-2.1(a)
of [Gleason] p. 168. (Contributed
by NM, 24-Sep-2005.) (Proof
shortened by Mario Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climmul 11128* |
Limit of the product of two converging sequences. Proposition
12-2.1(c) of [Gleason] p. 168.
(Contributed by NM, 27-Dec-2005.)
(Proof shortened by Mario Carneiro, 1-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climsub 11129* |
Limit of the difference of two converging sequences. Proposition
12-2.1(b) of [Gleason] p. 168.
(Contributed by NM, 4-Aug-2007.)
(Proof shortened by Mario Carneiro, 1-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climaddc1 11130* |
Limit of a constant
added to each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
3-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climaddc2 11131* |
Limit of a constant
added to each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
3-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climmulc2 11132* |
Limit of a sequence multiplied by a constant . Corollary
12-2.2 of [Gleason] p. 171.
(Contributed by NM, 24-Sep-2005.)
(Revised by Mario Carneiro, 3-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climsubc1 11133* |
Limit of a constant
subtracted from each term of a sequence.
(Contributed by Mario Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climsubc2 11134* |
Limit of a constant
minus each term of a sequence.
(Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro,
9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climle 11135* |
Comparison of the limits of two sequences. (Contributed by Paul
Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | climsqz 11136* |
Convergence of a sequence sandwiched between another converging
sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by
Mario Carneiro, 3-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif)
![A A](_ca.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | climsqz2 11137* |
Convergence of a sequence sandwiched between another converging
sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised
by Mario Carneiro, 3-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | clim2ser 11138* |
The limit of an infinite series with an initial segment removed.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 1-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M
M](_cm.gif) ![F F](_cf.gif)
![A A](_ca.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![F F](_cf.gif)
![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | clim2ser2 11139* |
The limit of an infinite series with an initial segment added.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 1-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![F F](_cf.gif)
![A A](_ca.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M
M](_cm.gif) ![F F](_cf.gif)
![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iserex 11140* |
An infinite series converges, if and only if the series does with
initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.)
(Revised by Mario Carneiro, 27-Apr-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif)
![seq seq](_seq.gif) ![N N](_cn.gif) ![F F](_cf.gif)
![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | isermulc2 11141* |
Multiplication of an infinite series by a constant. (Contributed by
Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![G G](_cg.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climlec2 11142* |
Comparison of a constant to the limit of a sequence. (Contributed by
NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iserle 11143* |
Comparison of the limits of two infinite series. (Contributed by Paul
Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif)
![A A](_ca.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![G G](_cg.gif)
![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iserge0 11144* |
The limit of an infinite series of nonnegative reals is nonnegative.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario
Carneiro, 3-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif)
![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | climub 11145* |
The limit of a monotonic sequence is an upper bound. (Contributed by
NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | climserle 11146* |
The partial sums of a converging infinite series with nonnegative
terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.)
(Revised by Mario Carneiro, 9-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif)
![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![RR
RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif)
![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | iser3shft 11147* |
Index shift of the limit of an infinite series. (Contributed by Mario
Carneiro, 6-Sep-2013.) (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) ![M M](_cm.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) ![F F](_cf.gif)
![seq seq](_seq.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | climcau 11148* |
A converging sequence of complex numbers is a Cauchy sequence. The
converse would require excluded middle or a different definition of
Cauchy sequence (for example, fixing a rate of convergence as in
climcvg1n 11151). Theorem 12-5.3 of [Gleason] p. 180 (necessity part).
(Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![j j](_j.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![j j](_j.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) |
|
Theorem | climrecvg1n 11149* |
A Cauchy sequence of real numbers converges, existence version. The
rate of convergence is fixed: all terms after the nth term must be
within of the nth term, where is a constant multiplier.
(Contributed by Jim Kingdon, 23-Aug-2021.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![NN NN](bbn.gif) ![--> -->](longrightarrow.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![n n](_n.gif) ![) )](rp.gif) ![( (](lp.gif)
![) )](rp.gif) |
|
Theorem | climcvg1nlem 11150* |
Lemma for climcvg1n 11151. We construct sequences of the real and
imaginary parts of each term of , show those converge, and use
that to show that converges. (Contributed by Jim Kingdon,
24-Aug-2021.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![NN NN](bbn.gif) ![--> -->](longrightarrow.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![n n](_n.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![Re Re](re.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![Im Im](im.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![) )](rp.gif) |
|
Theorem | climcvg1n 11151* |
A Cauchy sequence of complex numbers converges, existence version.
The rate of convergence is fixed: all terms after the nth term must be
within of the nth term, where is a constant
multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![NN NN](bbn.gif) ![--> -->](longrightarrow.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![n n](_n.gif) ![) )](rp.gif) ![( (](lp.gif)
![) )](rp.gif) |
|
Theorem | climcaucn 11152* |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 11148 but adds the part that ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) is complex.
(Contributed by Jim Kingdon, 24-Aug-2021.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![j j](_j.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![j j](_j.gif) ![) )](rp.gif) ![) )](rp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | serf0 11153* |
If an infinite series converges, its underlying sequence converges to
zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro,
16-Feb-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif)
![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
4.8.2 Finite and infinite sums
|
|
Syntax | csu 11154 |
Extend class notation to include finite summations. (An underscore was
added to the ASCII token in order to facilitate set.mm text searches,
since "sum" is a commonly used word in comments.)
|
![sum_ sum_](csigma.gif) ![B B](_cb.gif) |
|
Definition | df-sumdc 11155* |
Define the sum of a series with an index set of integers .
is normally a free variable in , i.e. can be thought of as
![B B](_cb.gif) ![( (](lp.gif) ![k k](_k.gif) . This definition is the result of a collection of
discussions over the most general definition for a sum that does not
need the index set to have a specified ordering. This definition is in
two parts, one for finite sums and one for subsets of the upper
integers. When summing over a subset of the upper integers, we extend
the index set to the upper integers by adding zero outside the domain,
and then sum the set in order, setting the result to the limit of the
partial sums, if it exists. This means that conditionally convergent
sums can be evaluated meaningfully. For finite sums, we are explicitly
order-independent, by picking any bijection to a 1-based finite sequence
and summing in the induced order. In both cases we have an
expression so that we only need to be defined where
.
In the infinite case, we also require that the indexing set be a
decidable subset of an upperset of integers (that is, membership of
integers in it is decidable). These two methods of summation produce
the same result on their common region of definition (i.e. finite sets
of integers). Examples: ![sum_
sum_](csigma.gif) ![{ {](lbrace.gif) ![1
1](1.gif) ![2 2](2.gif) ![4 4](4.gif) means
, and ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) means
1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 11323). (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
|
![sum_
sum_](csigma.gif)
![( (](lp.gif) ![iota iota](riota.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![seq seq](_seq.gif) ![m m](_m.gif)
![( (](lp.gif)
![if if](_if.gif) ![( (](lp.gif)
![A A](_ca.gif) ![[_ [_](_ulbrack.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![)
)](rp.gif)
![x x](_x.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq
seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![m m](_m.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sumeq1 11156 |
Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jun-2019.)
|
![( (](lp.gif) ![sum_
sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | nfsum1 11157 |
Bound-variable hypothesis builder for sum. (Contributed by NM,
11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
|
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![sum_ sum_](csigma.gif) ![B B](_cb.gif) |
|
Theorem | nfsum 11158 |
Bound-variable hypothesis builder for sum: if is (effectively) not
free in and
, it is not free in
![sum_ sum_](csigma.gif) ![A A](_ca.gif) .
(Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro,
13-Jun-2019.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![sum_ sum_](csigma.gif) ![B B](_cb.gif) |
|
Theorem | sumdc 11159* |
Decidability of a subset of upper integers. (Contributed by Jim
Kingdon, 1-Jan-2022.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) DECID ![A A](_ca.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif)
DECID
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | sumeq2 11160* |
Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised
by Mario Carneiro, 13-Jul-2013.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![sum_
sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | cbvsum 11161 |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jun-2019.)
|
![( (](lp.gif) ![C C](_cc.gif) ![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![sum_
sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![C C](_cc.gif) |
|
Theorem | cbvsumv 11162* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
(Revised by Mario Carneiro, 13-Jul-2013.)
|
![( (](lp.gif) ![C C](_cc.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) |
|
Theorem | cbvsumi 11163* |
Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.)
|
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![( (](lp.gif)
![C C](_cc.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) |
|
Theorem | sumeq1i 11164* |
Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
|
![sum_ sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![C C](_cc.gif) |
|
Theorem | sumeq2i 11165* |
Equality inference for sum. (Contributed by NM, 3-Dec-2005.)
|
![( (](lp.gif) ![C C](_cc.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) |
|
Theorem | sumeq12i 11166* |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
![( (](lp.gif) ![D D](_cd.gif) ![sum_ sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![D D](_cd.gif) |
|
Theorem | sumeq1d 11167* |
Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | sumeq2d 11168* |
Equality deduction for sum. Note that unlike sumeq2dv 11169, may
occur in . (Contributed by NM, 1-Nov-2005.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![C C](_cc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | sumeq2dv 11169* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised
by Mario Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | sumeq2ad 11170* |
Equality deduction for sum. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | sumeq2sdv 11171* |
Equality deduction for sum. (Contributed by NM, 3-Jan-2006.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | 2sumeq2dv 11172* |
Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | sumeq12dv 11173* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![D D](_cd.gif) ![( (](lp.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | sumeq12rdv 11174* |
Equality deduction for sum. (Contributed by NM, 1-Dec-2005.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![( (](lp.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | sumfct 11175* |
A lemma to facilitate conversions from the function form to the
class-variable form of a sum. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![sum_
sum_](csigma.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![j j](_j.gif)
![sum_ sum_](csigma.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | fz1f1o 11176* |
A lemma for working with finite sums. (Contributed by Mario Carneiro,
22-Apr-2014.)
|
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ♯![` `](backtick.gif) ![A A](_ca.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ♯![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnf1o 11177 |
Lemma for sum and product theorems. (Contributed by Jim Kingdon,
15-Aug-2022.)
|
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![M M](_cm.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![G G](_cg.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N
N](_cn.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) |
|
Theorem | sumrbdclem 11178* |
Lemma for sumrbdc 11180. (Contributed by Mario Carneiro,
12-Aug-2013.)
(Revised by Jim Kingdon, 8-Apr-2023.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) DECID ![A A](_ca.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) ![N N](_cn.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![N N](_cn.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fsum3cvg 11179* |
The sequence of partial sums of a finite sum converges to the whole
sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim
Kingdon, 12-Nov-2022.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sumrbdc 11180* |
Rebase the starting point of a sum. (Contributed by Mario Carneiro,
14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
DECID
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif)
DECID
![A A](_ca.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif)
![seq seq](_seq.gif) ![N N](_cn.gif) ![F F](_cf.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | summodclem3 11181* |
Lemma for summodc 11184. (Contributed by Mario Carneiro,
29-Mar-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![) )](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![M
M](_cm.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![K K](_ck.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N
N](_cn.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![M M](_cm.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![N N](_cn.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![n n](_n.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![M M](_cm.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) |
|
Theorem | summodclem2a 11182* |
Lemma for summodc 11184. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 9-Apr-2023.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif)
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![N N](_cn.gif)
![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![N
N](_cn.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.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) ![seq seq](_seq.gif) ![M
M](_cm.gif) ![F F](_cf.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | summodclem2 11183* |
Lemma for summodc 11184. (Contributed by Mario Carneiro,
3-Apr-2014.)
(Revised by Jim Kingdon, 4-May-2023.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![seq seq](_seq.gif) ![m m](_m.gif)
![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![seq
seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | summodc 11184* |
A sum has at most one limit. (Contributed by Mario Carneiro,
3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif)
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![[_
[_](_ulbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![n n](_n.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![m m](_m.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) DECID ![seq seq](_seq.gif) ![m m](_m.gif)
![F F](_cf.gif) ![x x](_x.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![seq
seq](_seq.gif) ![1 1](1.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zsumdc 11185* |
Series sum with index set a subset of the upper integers.
(Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim
Kingdon, 8-Apr-2023.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![0
0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif)
![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | isum 11186* |
Series sum with an upper integer index set (i.e. an infinite series).
(Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario
Carneiro, 7-Apr-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![(
(](lp.gif)
![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif)
![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fsumgcl 11187* |
Closure for a function used to describe a sum over a nonempty finite
set. (Contributed by Jim Kingdon, 10-Oct-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![C C](_cc.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![M
M](_cm.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![n n](_n.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![n n](_n.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | fsum3 11188* |
The value of a sum over a nonempty finite set. (Contributed by Jim
Kingdon, 10-Oct-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![C C](_cc.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![M
M](_cm.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![1 1](1.gif) ![... ...](ldots.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![n n](_n.gif) ![C C](_cc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![seq
seq](_seq.gif) ![1 1](1.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif)
![0 0](0.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sum0 11189 |
Any sum over the empty set is zero. (Contributed by Mario Carneiro,
12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
|
![sum_
sum_](csigma.gif)
![0 0](0.gif) |
|
Theorem | isumz 11190* |
Any sum of zero over a summable set is zero. (Contributed by Mario
Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 9-Apr-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) DECID ![A A](_ca.gif) ![Fin Fin](_fin.gif) ![sum_ sum_](csigma.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | fsumf1o 11191* |
Re-index a finite sum using a bijection. (Contributed by Mario
Carneiro, 20-Apr-2014.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif)
![G G](_cg.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | isumss 11192* |
Change the index set to a subset in an upper integer sum.
(Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim
Kingdon, 21-Sep-2022.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![0 0](0.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) DECID ![A A](_ca.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) DECID ![B B](_cb.gif) ![( (](lp.gif)
![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fisumss 11193* |
Change the index set to a subset in a finite sum. (Contributed by Mario
Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![0 0](0.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![Fin Fin](_fin.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | isumss2 11194* |
Change the index set of a sum by adding zeroes. The nonzero elements
are in the contained set and the added zeroes compose the rest of
the containing set which needs to be summable. (Contributed by
Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) DECID ![B B](_cb.gif) ![Fin Fin](_fin.gif) ![) )](rp.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fsum3cvg2 11195* |
The sequence of partial sums of a finite sum converges to the whole sum.
(Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon,
2-Dec-2022.)
|
![( (](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) ![if if](_if.gif) ![( (](lp.gif)
![A A](_ca.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
DECID
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fsumsersdc 11196* |
Special case of series sum over a finite upper integer index set.
(Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Jim
Kingdon, 5-May-2023.)
|
![( (](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) ![if if](_if.gif) ![( (](lp.gif)
![A A](_ca.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
DECID
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![seq
seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fsum3cvg3 11197* |
A finite sum is convergent. (Contributed by Mario Carneiro,
24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![Fin Fin](_fin.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif)
![) )](rp.gif) |
|
Theorem | fsum3ser 11198* |
A finite sum expressed in terms of a partial sum of an infinite series.
The recursive definition follows as fsum1 11213 and fsump1 11221, which should
make our notation clear and from which, along with closure fsumcl 11201, we
will derive the basic properties of finite sums. (Contributed by NM,
11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
|
![( (](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) ![A A](_ca.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)
![CC CC](bbc.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif)
![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fsumcl2lem 11199* |
- Lemma for finite sum closures. (The "-" before "Lemma"
forces the
math content to be displayed in the Statement List - NM 11-Feb-2008.)
(Contributed by Mario Carneiro, 3-Jun-2014.)
|
![( (](lp.gif) ![CC
CC](bbc.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) ![Fin Fin](_fin.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | fsumcllem 11200* |
- Lemma for finite sum closures. (The "-" before "Lemma"
forces the
math content to be displayed in the Statement List - NM 11-Feb-2008.)
(Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro,
3-Jun-2014.)
|
![( (](lp.gif) ![CC
CC](bbc.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) ![Fin Fin](_fin.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![S S](_cs.gif) ![) )](rp.gif) |