Theorem List for Intuitionistic Logic Explorer - 11301-11400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | trireciplem 11301 |
Lemma for trirecip 11302. Show that the sum converges. (Contributed
by
Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro,
22-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![F F](_cf.gif)
![1 1](1.gif) |
|
Theorem | trirecip 11302 |
The sum of the reciprocals of the triangle numbers converge to two.
This is Metamath 100 proof #42. (Contributed by Scott Fenton,
23-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|
![sum_
sum_](csigma.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![2 2](2.gif) |
|
4.8.7 Geometric series
|
|
Theorem | expcnvap0 11303* |
A sequence of powers of a complex number with absolute value
smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.)
(Revised by Jim Kingdon, 23-Oct-2022.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![n n](_n.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | expcnvre 11304* |
A sequence of powers of a nonnegative real number less than one
converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![n n](_n.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | expcnv 11305* |
A sequence of powers of a complex number with absolute value
smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.)
(Revised by Jim Kingdon, 28-Oct-2022.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![n n](_n.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | explecnv 11306* |
A sequence of terms converges to zero when it is less than powers of a
number whose
absolute value is smaller than 1. (Contributed by
NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![1 1](1.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) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | geosergap 11307* |
The value of the finite geometric series ![A A](_ca.gif) ![^ ^](uparrow.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1
1](1.gif) ...
![A A](_ca.gif) ![^ ^](uparrow.gif) ![(
(](lp.gif) ![1 1](1.gif) . (Contributed by Mario Carneiro, 2-May-2016.)
(Revised by Jim Kingdon, 24-Oct-2022.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![1 1](1.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | geoserap 11308* |
The value of the finite geometric series
![A A](_ca.gif) ![^ ^](uparrow.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ...
![A A](_ca.gif) ![^ ^](uparrow.gif) ![(
(](lp.gif) ![1 1](1.gif) . This is Metamath 100 proof #66. (Contributed by
NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # ![1 1](1.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pwm1geoserap1 11309* |
The n-th power of a number decreased by 1 expressed by the finite
geometric series
![A A](_ca.gif) ![^ ^](uparrow.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ... ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1
1](1.gif) .
(Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon,
24-Oct-2022.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) # ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | absltap 11310 |
Less-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) # ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | absgtap 11311 |
Greater-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) # ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | geolim 11312* |
The partial sums in the infinite series
![A A](_ca.gif) ![^ ^](uparrow.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ...
converge to ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) . (Contributed by NM,
15-May-2006.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif)
![seq seq](_seq.gif) ![0 0](0.gif) ![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | geolim2 11313* |
The partial sums in the geometric series ![A A](_ca.gif) ![^ ^](uparrow.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1
1](1.gif) ...
converge to ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) .
(Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.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) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k
k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M
M](_cm.gif) ![F F](_cf.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | georeclim 11314* |
The limit of a geometric series of reciprocals. (Contributed by Paul
Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif)
![seq seq](_seq.gif) ![0 0](0.gif) ![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | geo2sum 11315* |
The value of the finite geometric series ![2 2](2.gif) ![^ ^](uparrow.gif) ![-u -u](shortminus.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![-u -u](shortminus.gif) ...
![2 2](2.gif) ![^ ^](uparrow.gif) ![-u
-u](shortminus.gif) ,
multiplied by a constant. (Contributed by Mario
Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![1
1](1.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![2
2](2.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | geo2sum2 11316* |
The value of the finite geometric series
...
![2 2](2.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1 1](1.gif) . (Contributed by Mario Carneiro, 7-Sep-2016.)
|
![( (](lp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | geo2lim 11317* |
The value of the infinite geometric series
![2 2](2.gif) ![^ ^](uparrow.gif) ![-u -u](shortminus.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![-u -u](shortminus.gif) ... , multiplied by a constant. (Contributed
by Mario Carneiro, 15-Jun-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![^ ^](uparrow.gif) ![k
k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![seq seq](_seq.gif) ![1 1](1.gif) ![F F](_cf.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | geoisum 11318* |
The infinite sum of ![A A](_ca.gif) ![^ ^](uparrow.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ... is
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) .
(Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | geoisumr 11319* |
The infinite sum of reciprocals
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ... is ![(
(](lp.gif) ![1 1](1.gif) .
(Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | geoisum1 11320* |
The infinite sum of ![A A](_ca.gif) ![^ ^](uparrow.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ... is ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) .
(Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | geoisum1c 11321* |
The infinite sum of
![( (](lp.gif) ![R R](_cr.gif) ![^ ^](uparrow.gif) ![1 1](1.gif) ![( (](lp.gif) ![R R](_cr.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ... is
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![R R](_cr.gif) . (Contributed by NM, 2-Nov-2007.) (Revised
by Mario Carneiro, 26-Apr-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![R R](_cr.gif) ![1 1](1.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![^ ^](uparrow.gif) ![k
k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 0.999... 11322 |
The recurring decimal 0.999..., which is defined as the infinite sum 0.9 +
0.09 + 0.009 + ... i.e. ![1 1](1.gif) ![0 0](0.gif) ![^ ^](uparrow.gif) ![1 1](1.gif) ![0 0](0.gif) ![^ ^](uparrow.gif) ![1
1](1.gif) ![0 0](0.gif) ![^ ^](uparrow.gif)
, is exactly equal to
1. (Contributed by NM, 2-Nov-2007.)
(Revised by AV, 8-Sep-2021.)
|
![sum_
sum_](csigma.gif)
![( (](lp.gif) ;![1 1](1.gif) ![0 0](0.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) ![1 1](1.gif) |
|
Theorem | geoihalfsum 11323 |
Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... =
1. Uses geoisum1 11320. This is a representation of .111... in
binary with
an infinite number of 1's. Theorem 0.999... 11322 proves a similar claim for
.999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.)
(Proof shortened by AV, 9-Jul-2022.)
|
![sum_
sum_](csigma.gif)
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![^ ^](uparrow.gif) ![k k](_k.gif) ![) )](rp.gif) ![1 1](1.gif) |
|
4.8.8 Ratio test for infinite series
convergence
|
|
Theorem | cvgratnnlembern 11324 |
Lemma for cvgratnn 11332. Upper bound for a geometric progression of
positive ratio less than one. (Contributed by Jim Kingdon,
24-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![M M](_cm.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![1 1](1.gif) ![)
)](rp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnnlemnexp 11325* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon, 15-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![(
(](lp.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnnlemmn 11326* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
15-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnnlemseq 11327* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnnlemabsle 11328* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![sum_
sum_](csigma.gif)
![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![sum_
sum_](csigma.gif)
![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnnlemsumlt 11329* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon,
23-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif)
![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnnlemfm 11330* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon, 23-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![1 1](1.gif) ![) )](rp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnnlemrate 11331* |
Lemma for cvgratnn 11332. (Contributed by Jim Kingdon, 21-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![1 1](1.gif) ![) )](rp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cvgratnn 11332* |
Ratio test for convergence of a complex infinite series. If the ratio
of the
absolute values of successive terms in an infinite
sequence is
less than 1 for all terms, then the infinite sum of
the terms of
converges to a complex number. Although this
theorem is similar to cvgratz 11333 and cvgratgt0 11334, the decision to
index starting at one is not merely cosmetic, as proving convergence
using climcvg1n 11151 is sensitive to how a sequence is indexed.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
12-Nov-2022.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![1 1](1.gif) ![F F](_cf.gif)
![) )](rp.gif) |
|
Theorem | cvgratz 11333* |
Ratio test for convergence of a complex infinite series. If the ratio
of the
absolute values of successive terms in an infinite sequence
is less than 1
for all terms, then the infinite sum of the terms
of converges
to a complex number. (Contributed by NM,
26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
|
![( (](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) ![1 1](1.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) ![CC
CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif)
![) )](rp.gif) |
|
Theorem | cvgratgt0 11334* |
Ratio test for convergence of a complex infinite series. If the ratio
of the
absolute values of successive terms in an infinite sequence
is less than 1
for all terms beyond some index , then the
infinite sum of the terms of converges to a complex number.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
11-Nov-2022.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.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) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.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) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif)
![F F](_cf.gif)
![) )](rp.gif) |
|
4.8.9 Mertens' theorem
|
|
Theorem | mertenslemub 11335* |
Lemma for mertensabs 11338. An upper bound for . (Contributed by
Jim Kingdon, 3-Dec-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![0 0](0.gif) ![G G](_cg.gif)
![{ {](lbrace.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![0
0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![sum_
sum_](csigma.gif)
![( (](lp.gif) ![0
0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mertenslemi1 11336* |
Lemma for mertensabs 11338. (Contributed by Mario Carneiro,
29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![j j](_j.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![j j](_j.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![NN0
NN0](_bbn0.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![j j](_j.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![0 0](0.gif) ![K K](_ck.gif)
![( (](lp.gif)
![seq seq](_seq.gif) ![0 0](0.gif) ![G G](_cg.gif)
![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![0
0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![s s](_s.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![sum_ sum_](csigma.gif)
![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![j j](_j.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![t t](_t.gif) ![) )](rp.gif) ![(
(](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![m m](_m.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![s s](_s.gif) ![( (](lp.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![P P](_cp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![P P](_cp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![j j](_j.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![E E](_ce.gif) ![) )](rp.gif) |
|
Theorem | mertenslem2 11337* |
Lemma for mertensabs 11338. (Contributed by Mario Carneiro,
28-Apr-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![j j](_j.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![j j](_j.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![NN0
NN0](_bbn0.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![j j](_j.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![0 0](0.gif) ![K K](_ck.gif)
![( (](lp.gif)
![seq seq](_seq.gif) ![0 0](0.gif) ![G G](_cg.gif)
![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![0
0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![s s](_s.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![sum_ sum_](csigma.gif)
![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![j j](_j.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![m m](_m.gif) ![) )](rp.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![j j](_j.gif)
![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![E E](_ce.gif) ![) )](rp.gif) |
|
Theorem | mertensabs 11338* |
Mertens' theorem. If ![A A](_ca.gif) ![( (](lp.gif) ![j j](_j.gif) is an absolutely convergent series and
![B B](_cb.gif) ![( (](lp.gif) ![k k](_k.gif) is convergent, then
![( (](lp.gif) ![sum_ sum_](csigma.gif) ![NN0 NN0](_bbn0.gif) ![A A](_ca.gif) ![( (](lp.gif) ![j j](_j.gif) ![sum_ sum_](csigma.gif) ![NN0 NN0](_bbn0.gif) ![B B](_cb.gif) ![( (](lp.gif) ![k k](_k.gif) ![) )](rp.gif)
![sum_ sum_](csigma.gif) ![NN0
NN0](_bbn0.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![j j](_j.gif) ![B B](_cb.gif) ![( (](lp.gif) ![j j](_j.gif) ![) )](rp.gif) (and
this latter series is convergent). This latter sum is commonly known as
the Cauchy product of the sequences. The proof follows the outline at
http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem.
(Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![j j](_j.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![j j](_j.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![NN0
NN0](_bbn0.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![k k](_k.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![k k](_k.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![j j](_j.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![0 0](0.gif) ![K K](_ck.gif)
![( (](lp.gif)
![seq seq](_seq.gif) ![0 0](0.gif) ![G G](_cg.gif)
![( (](lp.gif) ![seq seq](_seq.gif) ![0 0](0.gif) ![F F](_cf.gif) ![( (](lp.gif)
![seq seq](_seq.gif) ![0 0](0.gif) ![H H](_ch.gif) ![( (](lp.gif) ![sum_ sum_](csigma.gif) ![sum_ sum_](csigma.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.8.10 Finite and infinite
products
|
|
4.8.10.1 Product sequences
|
|
Theorem | prodf 11339* |
An infinite product of complex terms is a function from an upper set of
integers to .
(Contributed by Scott Fenton, 4-Dec-2017.)
|
![( (](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) ![CC
CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![: :](colon.gif) ![Z Z](_cz.gif) ![--> -->](longrightarrow.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | clim2prod 11340* |
The limit of an infinite product with an initial segment added.
(Contributed by Scott Fenton, 18-Dec-2017.)
|
![( (](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) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | clim2divap 11341* |
The limit of an infinite product with an initial segment removed.
(Contributed by Scott Fenton, 20-Dec-2017.)
|
![( (](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) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) # ![0 0](0.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 | prod3fmul 11342* |
The product of two infinite products. (Contributed by Scott Fenton,
18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
|
![( (](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) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.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) ![seq seq](_seq.gif) ![M M](_cm.gif) ![H H](_ch.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif)
![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | prodf1 11343 |
The value of the partial products in a one-valued infinite product.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif)
![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | prodf1f 11344 |
A one-valued infinite product is equal to the constant one function.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | prodfclim1 11345 |
The constant one product converges to one. (Contributed by Scott
Fenton, 5-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | prodfap0 11346* |
The product of finitely many terms apart from zero is apart from zero.
(Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon,
23-Mar-2024.)
|
![( (](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) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) # ![0 0](0.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) # ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | prodfrecap 11347* |
The reciprocal of a finite product. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
![( (](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) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![... ...](ldots.gif) ![N N](_cn.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![...
...](ldots.gif) ![N N](_cn.gif) ![) )](rp.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) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.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 | prodfdivap 11348* |
The quotient of two products. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
![( (](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) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.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)
![seq seq](_seq.gif) ![M M](_cm.gif) ![H H](_ch.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.8.10.2 Non-trivial convergence
|
|
Theorem | ntrivcvgap 11349* |
A non-trivially converging infinite product converges. (Contributed by
Scott Fenton, 18-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif)
![y y](_y.gif) ![) )](rp.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)
![) )](rp.gif) |
|
Theorem | ntrivcvgap0 11350* |
A product that converges to a value apart from zero converges
non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
|
![( (](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)
![X X](_cx.gif) ![( (](lp.gif) #
![0 0](0.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
4.8.10.3 Complex products
|
|
Syntax | cprod 11351 |
Extend class notation to include complex products.
|
![prod_ prod_](prod.gif) ![B B](_cb.gif) |
|
Definition | df-proddc 11352* |
Define the product of a series with an index set of integers .
This definition takes most of the aspects of df-sumdc 11155 and adapts them
for multiplication instead of addition. However, we insist that in the
infinite case, there is a nonzero tail of the sequence. This ensures
that the convergence criteria match those of infinite sums.
(Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon,
21-Mar-2024.)
|
![prod_
prod_](prod.gif)
![( (](lp.gif) ![iota iota](riota.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.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 ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![y y](_y.gif)
![seq seq](_seq.gif) ![m m](_m.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![)
)](rp.gif)
![x x](_x.gif) ![) )](rp.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) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | prodeq1f 11353 |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif)
![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | prodeq1 11354* |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
![( (](lp.gif) ![prod_
prod_](prod.gif)
![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | nfcprod1 11355* |
Bound-variable hypothesis builder for product. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![prod_ prod_](prod.gif) ![B B](_cb.gif) |
|
Theorem | nfcprod 11356* |
Bound-variable hypothesis builder for product: if is (effectively)
not free in
and , it is not free
in ![prod_ prod_](prod.gif) ![A A](_ca.gif) .
(Contributed by Scott Fenton, 1-Dec-2017.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![prod_ prod_](prod.gif) ![B B](_cb.gif) |
|
Theorem | prodeq2w 11357* |
Equality theorem for product, when the class expressions and
are equal everywhere. Proved using only Extensionality. (Contributed
by Scott Fenton, 4-Dec-2017.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | prodeq2 11358* |
Equality theorem for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![prod_
prod_](prod.gif)
![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | cbvprod 11359* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](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) ![prod_
prod_](prod.gif)
![prod_ prod_](prod.gif) ![C C](_cc.gif) |
|
Theorem | cbvprodv 11360* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![C C](_cc.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) |
|
Theorem | cbvprodi 11361* |
Change bound variable in a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![F/_ F/_](_finvbar.gif) ![k k](_k.gif) ![F/_ F/_](_finvbar.gif) ![j j](_j.gif) ![( (](lp.gif)
![C C](_cc.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) |
|
Theorem | prodeq1i 11362* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![prod_ prod_](prod.gif)
![prod_ prod_](prod.gif) ![C C](_cc.gif) |
|
Theorem | prodeq2i 11363* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![C C](_cc.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) |
|
Theorem | prodeq12i 11364* |
Equality inference for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![D D](_cd.gif) ![prod_ prod_](prod.gif)
![prod_ prod_](prod.gif) ![D D](_cd.gif) |
|
Theorem | prodeq1d 11365* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | prodeq2d 11366* |
Equality deduction for product. Note that unlike prodeq2dv 11367,
may occur in . (Contributed by Scott Fenton, 4-Dec-2017.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![C C](_cc.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | prodeq2dv 11367* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | prodeq2sdv 11368* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | 2cprodeq2dv 11369* |
Equality deduction for double product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif)
![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | prodeq12dv 11370* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![D D](_cd.gif) ![( (](lp.gif)
![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | prodeq12rdv 11371* |
Equality deduction for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![( (](lp.gif)
![prod_ prod_](prod.gif) ![prod_ prod_](prod.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | prodrbdclem 11372* |
Lemma for prodrbdc 11375. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 4-Apr-2024.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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 | fproddccvg 11373* |
The sequence of partial products of a finite product converges to
the whole product. (Contributed by Scott Fenton, 4-Dec-2017.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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 | prodrbdclem2 11374* |
Lemma for prodrbdc 11375. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![M M](_cm.gif) ![) )](rp.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 | prodrbdc 11375* |
Rebase the starting point of a product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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 | prodmodclem3 11376* |
Lemma for prodmodc 11379. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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) ![j j](_j.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif)
♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif)
![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![j j](_j.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.gif) ![) )](rp.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) ![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 | prodmodclem2a 11377* |
Lemma for prodmodc 11379. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 11-Apr-2024.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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) ![j j](_j.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif)
♯![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif)
![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![K K](_ck.gif) ![` `](backtick.gif) ![j j](_j.gif) ![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![1 1](1.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) ![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 | prodmodclem2 11378* |
Lemma for prodmodc 11379. (Contributed by Scott Fenton, 4-Dec-2017.)
(Revised by Jim Kingdon, 13-Apr-2024.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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) ![j j](_j.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.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 ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif)
![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif)
![x x](_x.gif) ![) )](rp.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)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | prodmodc 11379* |
A product has at most one limit. (Contributed by Scott Fenton,
4-Dec-2017.) (Modified by Jim Kingdon, 14-Apr-2024.)
|
![( (](lp.gif) ![if if](_if.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![1 1](1.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) ![j j](_j.gif)
![k k](_k.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.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 ![A A](_ca.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif)
![y y](_y.gif) ![seq seq](_seq.gif) ![m m](_m.gif) ![F F](_cf.gif)
![x x](_x.gif) ![) )](rp.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 | zproddc 11380* |
Series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif)
![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![A. A.](forall.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)
![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif) ![seq
seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iprodap 11381* |
Series product with an upper integer index set (i.e. an infinite
product.) (Contributed by Scott Fenton, 5-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) # ![seq seq](_seq.gif) ![n n](_n.gif) ![F F](_cf.gif)
![y y](_y.gif) ![) )](rp.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) ![prod_ prod_](prod.gif)
![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zprodap0 11382* |
Nonzero series product with index set a subset of the upper integers.
(Contributed by Scott Fenton, 6-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) #
![0 0](0.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif)
![X X](_cx.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![A A](_ca.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) ![1
1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![prod_ prod_](prod.gif) ![X X](_cx.gif) ![) )](rp.gif) |
|
Theorem | iprodap0 11383* |
Nonzero series product with an upper integer index set (i.e. an
infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.)
|
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) #
![0 0](0.gif) ![( (](lp.gif) ![seq seq](_seq.gif) ![M M](_cm.gif) ![F F](_cf.gif)
![X X](_cx.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) ![prod_ prod_](prod.gif)
![X X](_cx.gif) ![) )](rp.gif) |
|
4.8.10.4 Finite products
|
|
Theorem | fprodseq 11384* |
The value of a product over a nonempty finite set. (Contributed by
Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
|
![( (](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) ![prod_ prod_](prod.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) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.9 Elementary trigonometry
|
|
4.9.1 The exponential, sine, and cosine
functions
|
|
Syntax | ce 11385 |
Extend class notation to include the exponential function.
|
![exp exp](_exp.gif) |
|
Syntax | ceu 11386 |
Extend class notation to include Euler's constant = 2.71828....
|
![_e _e](rme.gif) |
|
Syntax | csin 11387 |
Extend class notation to include the sine function.
|
![sin sin](_sin.gif) |
|
Syntax | ccos 11388 |
Extend class notation to include the cosine function.
|
![cos cos](_cos.gif) |
|
Syntax | ctan 11389 |
Extend class notation to include the tangent function.
|
![tan tan](_tan.gif) |
|
Syntax | cpi 11390 |
Extend class notation to include the constant pi, = 3.14159....
|
![pi pi](pi.gif) |
|
Definition | df-ef 11391* |
Define the exponential function. Its value at the complex number
is ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![A A](_ca.gif) and is called the "exponential of "; see
efval 11404. (Contributed by NM, 14-Mar-2005.)
|
![( (](lp.gif) ![sum_ sum_](csigma.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![^ ^](uparrow.gif) ![k
k](_k.gif) ![( (](lp.gif) ![! !](bang.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-e 11392 |
Define Euler's constant = 2.71828.... (Contributed by NM,
14-Mar-2005.)
|
![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Definition | df-sin 11393 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![_i _i](rmi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-cos 11394 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-tan 11395 |
Define the tangent function. We define it this way for cmpt 3997,
which
requires the form ![( (](lp.gif) ![B B](_cb.gif) .
(Contributed by Mario
Carneiro, 14-Mar-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![cos cos](_cos.gif) ![" "](backquote.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![0 0](0.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-pi 11396 |
Define the constant pi, = 3.14159..., which is the smallest
positive number whose sine is zero. Definition of in [Gleason]
p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV,
14-Sep-2020.)
|
inf![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![sin sin](_sin.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![0 0](0.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | eftcl 11397 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![K K](_ck.gif) ![( (](lp.gif) ![! !](bang.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | reeftcl 11398 |
The terms of the series expansion of the exponential function at a real
number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![K K](_ck.gif) ![( (](lp.gif) ![! !](bang.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | eftabs 11399 |
The absolute value of a term in the series expansion of the exponential
function. (Contributed by Paul Chapman, 23-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![K K](_ck.gif) ![( (](lp.gif) ![! !](bang.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![K K](_ck.gif) ![( (](lp.gif) ![! !](bang.gif) ![` `](backtick.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eftvalcn 11400* |
The value of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![n n](_n.gif) ![( (](lp.gif) ![! !](bang.gif) ![` `](backtick.gif) ![n n](_n.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![N N](_cn.gif)
![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif) ![( (](lp.gif) ![! !](bang.gif) ![` `](backtick.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |