P. 137 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13601-13700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	telfsum2 13601*	Sum of a telescoping series. (Contributed by Mario Carneiro, 15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|- ( k = j -> A = B )   &    |- ( k = ( j + 1 ) -> A = C )   &    |- ( k = M -> A = D )   &    |- ( k = ( N + 1 ) -> A = E )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   =>    |- ( ph -> sum_ j e. ( M ... N ) ( C - B ) = ( E - D ) )
Theorem	fsumparts 13602*	Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( k = j -> ( A = B /\ V = W ) )   &    |- ( k = ( j + 1 ) -> ( A = C /\ V = X ) )   &    |- ( k = M -> ( A = D /\ V = Y ) )   &    |- ( k = N -> ( A = E /\ V = Z ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> V e. CC )   =>    |- ( ph -> sum_ j e. ( M..^ N ) ( B x. ( X - W ) ) = ( ( ( E x. Z ) - ( D x. Y ) ) - sum_ j e. ( M..^ N ) ( ( C - B ) x. X ) ) )
Theorem	fsumrelem 13603*	Lemma for fsumre 13604, fsumim 13605, and fsumcj 13606. (Contributed by Mario Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- F : CC --> CC   &    |- ( ( x e. CC /\ y e. CC ) -> ( F ` ( x + y ) ) = ( ( F ` x ) + ( F ` y ) ) )   =>    |- ( ph -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) )
Theorem	fsumre 13604*	The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( Re ` sum_ k e. A B ) = sum_ k e. A ( Re ` B ) )
Theorem	fsumim 13605*	The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( Im ` sum_ k e. A B ) = sum_ k e. A ( Im ` B ) )
Theorem	fsumcj 13606*	The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( * ` sum_ k e. A B ) = sum_ k e. A ( * ` B ) )
Theorem	fsumrlim 13607*	Limit of a finite sum of converging sequences. Note that C ( k ) is a collection of functions with implicit parameter k, each of which converges to D ( k ) as n ~~> +oo. (Contributed by Mario Carneiro, 22-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )   &    |- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) ~~> r D )   =>    |- ( ph -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D )
Theorem	fsumo1 13608*	The finite sum of eventually bounded functions (where the index set B does not depend on x) is eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 22-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )   &    |- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> sum_ k e. B C ) e. O(1) )
Theorem	o1fsum 13609*	If A ( k ) is O(1), then sum_ k <_ x , A ( k ) is O( x). (Contributed by Mario Carneiro, 23-May-2016.)
|- ( ( ph /\ k e. NN ) -> A e. V )   &    |- ( ph -> ( k e. NN |-> A ) e. O(1) )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) e. O(1) )
Theorem	seqabs 13610*	Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by Mario Carneiro, 26-Mar-2014.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> ( abs ` ( seq M ( + , F ) ` N ) ) <_ ( seq M ( + , G ) ` N ) )
Theorem	iserabs 13611*	Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 27-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ph -> seq M ( + , G ) ~~> B )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> ( abs ` A ) <_ B )
Theorem	cvgcmp 13612*	A comparison test for convergence of a real infinite series. Exercise 3 of [Gleason] p. 182. (Contributed by NM, 1-May-2005.) (Revised by Mario Carneiro, 24-Mar-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( G ` k ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( G ` k ) <_ ( F ` k ) )   =>    |- ( ph -> seq M ( + , G ) e. dom ~~> )
Theorem	cvgcmpub 13613*	An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. (Contributed by Mario Carneiro, 24-Mar-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ph -> seq M ( + , G ) ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )   =>    |- ( ph -> B <_ A )
Theorem	cvgcmpce 13614*	A comparison test for convergence of a complex infinite series. (Contributed by NM, 25-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( abs ` ( G ` k ) ) <_ ( C x. ( F ` k ) ) )   =>    |- ( ph -> seq M ( + , G ) e. dom ~~> )
Theorem	abscvgcvg 13615*	An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( abs ` ( G ` k ) ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> seq M ( + , G ) e. dom ~~> )
Theorem	climfsum 13616*	Limit of a finite sum of converging sequences. Note that F ( k ) is a collection of functions with implicit parameter k, each of which converges to B ( k ) as n ~~> +oo. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Mario Carneiro, 22-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> F ~~> B )   &    |- ( ph -> H e. W )   &    |- ( ( ph /\ ( k e. A /\ n e. Z ) ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ n e. Z ) -> ( H ` n ) = sum_ k e. A ( F ` n ) )   =>    |- ( ph -> H ~~> sum_ k e. A B )
Theorem	fsumiun 13617*	Sum over a disjoint indexed union. (Contributed by Mario Carneiro, 1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. Fin )   &    |- ( ph -> Disj x e. A B )   &    |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> sum_ k e. U_ x e. A B C = sum_ x e. A sum_ k e. B C )
Theorem	hashiun 13618*	The cardinality of a disjoint indexed union. (Contributed by Mario Carneiro, 24-Jan-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. Fin )   &    |- ( ph -> Disj x e. A B )   =>    |- ( ph -> ( # ` U_ x e. A B ) = sum_ x e. A ( # ` B ) )
Theorem	hashrabrex 13619*	The number of elements in a class abstraction with a restricted existential quantification. (Contributed by Alexander van der Vekens, 29-Jul-2018.)
|- ( ph -> Y e. Fin )   &    |- ( ( ph /\ y e. Y ) -> { x e. X | ps } e. Fin )   &    |- ( ph -> Disj y e. Y { x e. X | ps } )   =>    |- ( ph -> ( # ` { x e. X | E. y e. Y ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )
Theorem	hashuni 13620*	The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Fin )   &    |- ( ph -> Disj x e. A x )   =>    |- ( ph -> ( # ` U. A ) = sum_ x e. A ( # ` x ) )
Theorem	qshash 13621*	The cardinality of a set with an equivalence relation is the sum of the cardinalities of its equivalence classes. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( ph -> .~ Er A )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> ( # ` A ) = sum_ x e. ( A /. .~ ) ( # ` x ) )
Theorem	ackbijnn 13622*	Translate the Ackermann bijection ackbij1 8621 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- F = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ y e. x ( 2 ^ y ) )   =>    |- F : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
5.9.4  The binomial theorem
Theorem	binomlem 13623*	Lemma for binom 13624 (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ps -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( A + B ) ^ ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
Theorem	binom 13624*	The binomial theorem: ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ). Theorem 15-2.8 of [Gleason] p. 296. This part of the proof sets up the induction and does the base case, with the bulk of the work (the induction step) in binomlem 13623. This is Metamath 100 proof #44. (Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
Theorem	binom1p 13625*	Special case of the binomial theorem for ( 1 + A ) ^ N. (Contributed by Paul Chapman, 10-May-2007.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( 1 + A ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( A ^ k ) ) )
Theorem	binom11 13626*	Special case of the binomial theorem for 2 ^ N. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN0 -> ( 2 ^ N ) = sum_ k e. ( 0 ... N ) ( N _C k ) )
Theorem	binom1dif 13627*	A summation for the difference between ( ( A + 1 ) ^ N ) and ( A ^ N ). (Contributed by Scott Fenton, 9-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( ( A + 1 ) ^ N ) - ( A ^ N ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) )
Theorem	bcxmaslem1 13628	Lemma for bcxmas 13629. (Contributed by Paul Chapman, 18-May-2007.)
|- ( A = B -> ( ( N + A ) _C A ) = ( ( N + B ) _C B ) )
Theorem	bcxmas 13629*	Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( N + 1 ) + M ) _C M ) = sum_ j e. ( 0 ... M ) ( ( N + j ) _C j ) )
5.9.5  The inclusion/exclusion principle
Theorem	incexclem 13630*	Lemma for incexc 13631. (Contributed by Mario Carneiro, 7-Aug-2017.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` B ) - ( # ` ( B i^i U. A ) ) ) = sum_ s e. ~P A ( ( -u 1 ^ ( # ` s ) ) x. ( # ` ( B i^i |^| s ) ) ) )
Theorem	incexc 13631*	The inclusion/exclusion principle for counting the elements of a finite union of finite sets. This is Metamath 100 proof #96. (Contributed by Mario Carneiro, 7-Aug-2017.)
|- ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ s e. ( ~P A \ { (/) } ) ( ( -u 1 ^ ( ( # ` s ) - 1 ) ) x. ( # ` |^| s ) ) )
Theorem	incexc2 13632*	The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.)
|- ( ( A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ n e. ( 1 ... ( # ` A ) ) ( ( -u 1 ^ ( n - 1 ) ) x. sum_ s e. { k e. ~P A | ( # ` k ) = n } ( # ` |^| s ) ) )
5.9.6  Infinite sums (cont.)
Theorem	isumshft 13633*	Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` ( M + K ) )   &    |- ( j = ( K + k ) -> A = B )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ j e. W ) -> A e. CC )   =>    |- ( ph -> sum_ j e. W A = sum_ k e. Z B )
Theorem	isumsplit 13634*	Split off the first N terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A = ( sum_ k e. ( M ... ( N - 1 ) ) A + sum_ k e. W A ) )
Theorem	isum1p 13635*	The infinite sum of a converging infinite series equals the first term plus the infinite sum of the rest of it. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A = ( ( F ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) A ) )
Theorem	isumnn0nn 13636*	Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- ( k = 0 -> A = B )   &    |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. NN0 ) -> A e. CC )   &    |- ( ph -> seq 0 ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. NN0 A = ( B + sum_ k e. NN A ) )
Theorem	isumrpcl 13637*	The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR+ )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. W A e. RR+ )
Theorem	isumle 13638*	Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. RR )   &    |- ( ( ph /\ k e. Z ) -> A <_ B )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   &    |- ( ph -> seq M ( + , G ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z A <_ sum_ k e. Z B )
Theorem	isumless 13639*	A finite sum of nonnegative numbers is less or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ B )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. A B <_ sum_ k e. Z B )
Theorem	isumsup2 13640*	An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.)
|- Z = ( ZZ>= ` M )   &    |- G = seq M ( + , F )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ A )   &    |- ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )   =>    |- ( ph -> G ~~> sup ( ran G , RR , < ) )
Theorem	isumsup 13641*	An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.)
|- Z = ( ZZ>= ` M )   &    |- G = seq M ( + , F )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ A )   &    |- ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )   =>    |- ( ph -> sum_ k e. Z A = sup ( ran G , RR , < ) )
Theorem	isumltss 13642*	A partial sum of a series with positive terms is less than the infinite sum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. RR+ )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. A B < sum_ k e. Z B )
Theorem	climcndslem1 13643*	Lemma for climcnds 13645: bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )   =>    |- ( ( ph /\ N e. NN0 ) -> ( seq 1 ( + , F ) ` ( ( 2 ^ ( N + 1 ) ) - 1 ) ) <_ ( seq 0 ( + , G ) ` N ) )
Theorem	climcndslem2 13644*	Lemma for climcnds 13645: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )   =>    |- ( ( ph /\ N e. NN ) -> ( seq 1 ( + , G ) ` N ) <_ ( 2 x. ( seq 1 ( + , F ) ` ( 2 ^ N ) ) ) )
Theorem	climcnds 13645*	The Cauchy condensation test. If a ( k ) is a decreasing sequence of nonnegative terms, then sum_ k e. NN a ( k ) converges iff sum_ n e. NN0 2 ^ n x. a ( 2 ^ n ) converges. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( F ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ( ph /\ n e. NN0 ) -> ( G ` n ) = ( ( 2 ^ n ) x. ( F ` ( 2 ^ n ) ) ) )   =>    |- ( ph -> ( seq 1 ( + , F ) e. dom ~~> <-> seq 0 ( + , G ) e. dom ~~> ) )
5.9.7  Miscellaneous converging and diverging sequences
Theorem	divrcnv 13646*	The sequence of reciprocals of real numbers, multiplied by the factor A, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. CC -> ( n e. RR+ |-> ( A / n ) ) ~~> r 0 )
Theorem	divcnv 13647*	The sequence of reciprocals of positive integers, multiplied by the factor A, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 18-Sep-2014.)
|- ( A e. CC -> ( n e. NN |-> ( A / n ) ) ~~> 0 )
Theorem	flo1 13648	The floor function satisfies |_ ( x ) = x + O(1). (Contributed by Mario Carneiro, 21-May-2016.)
|- ( x e. RR |-> ( x - ( |_ ` x ) ) ) e. O(1)
Theorem	supcvg 13649*	Extract a sequence f in X such that the image of the points in the bounded set A converges to the supremum S of the set. Similar to Equation 4 of [Kreyszig] p. 144. The proof uses countable choice ax-cc 8818. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
|- X e. _V   &    |- S = sup ( A , RR , < )   &    |- R = ( n e. NN |-> ( S - ( 1 / n ) ) )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> F : X -onto-> A )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   =>    |- ( ph -> E. f ( f : NN --> X /\ ( F o. f ) ~~> S ) )
Theorem	infcvgaux1i 13650*	Auxiliary theorem for applications of supcvg 13649. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.)
|- R = { x | E. y e. X x = -u A }   &    |- ( y e. X -> A e. RR )   &    |- Z e. X   &    |- E. z e. RR A. w e. R w <_ z   =>    |- ( R C_ RR /\ R =/= (/) /\ E. z e. RR A. w e. R w <_ z )
Theorem	infcvgaux2i 13651*	Auxiliary theorem for applications of supcvg 13649. (Contributed by NM, 4-Mar-2008.)
|- R = { x | E. y e. X x = -u A }   &    |- ( y e. X -> A e. RR )   &    |- Z e. X   &    |- E. z e. RR A. w e. R w <_ z   &    |- S = -u sup ( R , RR , < )   &    |- ( y = C -> A = B )   =>    |- ( C e. X -> S <_ B )
Theorem	harmonic 13652	The harmonic series H diverges. This fact follows from the stronger emcl 23310, which establishes that the harmonic series grows as log n + gamma + o(1), but this uses a more elementary method, attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof #34. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( 1 / n ) )   &    |- H = seq 1 ( + , F )   =>    |- -. H e. dom ~~>
5.9.8  Arithmetic series
Theorem	arisum 13653*	Arithmetic series sum of the first N positive integers. This is Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 22-May-2014.)
|- ( N e. NN0 -> sum_ k e. ( 1 ... N ) k = ( ( ( N ^ 2 ) + N ) / 2 ) )
Theorem	arisum2 13654*	Arithmetic series sum of the first N nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
Theorem	trireciplem 13655	Lemma for trirecip 13656. Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|- F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )   =>    |- seq 1 ( + , F ) ~~> 1
Theorem	trirecip 13656	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_ k e. NN ( 2 / ( k x. ( k + 1 ) ) ) = 2
5.9.9  Geometric series
Theorem	expcnv 13657*	A sequence of powers of a complex number A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   =>    |- ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
Theorem	explecnv 13658*	A sequence of terms converges to zero when it is less than powers of a number A whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> ( abs ` A ) < 1 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( abs ` ( F ` k ) ) <_ ( A ^ k ) )   =>    |- ( ph -> F ~~> 0 )
Theorem	geoserg 13659*	The value of the finite geometric series A ^ M + A ^ ( M + 1 ) +... + A ^ ( N - 1 ). (Contributed by Mario Carneiro, 2-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 1 )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> sum_ k e. ( M..^ N ) ( A ^ k ) = ( ( ( A ^ M ) - ( A ^ N ) ) / ( 1 - A ) ) )
Theorem	geoser 13660*	The value of the finite geometric series 1 + A ^ 1 + A ^ 2 +... + A ^ ( N - 1 ). This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Proof shortened by Mario Carneiro, 15-Jun-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 1 )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) )
Theorem	geolim 13661*	The partial sums in the infinite series 1 + A ^ 1 + A ^ 2... converge to ( 1 / ( 1 - A ) ). (Contributed by NM, 15-May-2006.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   &    |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( A ^ k ) )   =>    |- ( ph -> seq 0 ( + , F ) ~~> ( 1 / ( 1 - A ) ) )
Theorem	geolim2 13662*	The partial sums in the geometric series A ^ M + A ^ ( M + 1 )... converge to ( ( A ^ M ) / ( 1 - A ) ). (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) < 1 )   &    |- ( ph -> M e. NN0 )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( A ^ k ) )   =>    |- ( ph -> seq M ( + , F ) ~~> ( ( A ^ M ) / ( 1 - A ) ) )
Theorem	georeclim 13663*	The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> 1 < ( abs ` A ) )   &    |- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( 1 / A ) ^ k ) )   =>    |- ( ph -> seq 0 ( + , F ) ~~> ( A / ( A - 1 ) ) )
Theorem	geo2sum 13664*	The value of the finite geometric series 2 ^ -u 1 + 2 ^ -u 2 +... + 2 ^ -u N, multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( N e. NN /\ A e. CC ) -> sum_ k e. ( 1 ... N ) ( A / ( 2 ^ k ) ) = ( A - ( A / ( 2 ^ N ) ) ) )
Theorem	geo2sum2 13665*	The value of the finite geometric series 1 + 2 + 4 + 8 +... + 2 ^ ( N - 1 ). (Contributed by Mario Carneiro, 7-Sep-2016.)
|- ( N e. NN0 -> sum_ k e. ( 0..^ N ) ( 2 ^ k ) = ( ( 2 ^ N ) - 1 ) )
Theorem	geo2lim 13666*	The value of the infinite geometric series 2 ^ -u 1 + 2 ^ -u 2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- F = ( k e. NN |-> ( A / ( 2 ^ k ) ) )   =>    |- ( A e. CC -> seq 1 ( + , F ) ~~> A )
Theorem	geomulcvg 13667*	The geometric series converges even if it is multiplied by k to result in the larger series k x. A ^ k. (Contributed by Mario Carneiro, 27-Mar-2015.)
|- F = ( k e. NN0 |-> ( k x. ( A ^ k ) ) )   =>    |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , F ) e. dom ~~> )
Theorem	geoisum 13668*	The infinite sum of 1 + A ^ 1 + A ^ 2... is ( 1 / ( 1 - A ) ). (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN0 ( A ^ k ) = ( 1 / ( 1 - A ) ) )
Theorem	geoisumr 13669*	The infinite sum of reciprocals 1 + ( 1 / A ) ^ 1 + ( 1 / A ) ^ 2... is A / ( A - 1 ). (Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ 1 < ( abs ` A ) ) -> sum_ k e. NN0 ( ( 1 / A ) ^ k ) = ( A / ( A - 1 ) ) )
Theorem	geoisum1 13670*	The infinite sum of A ^ 1 + A ^ 2... is ( A / ( 1 - A ) ). (Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN ( A ^ k ) = ( A / ( 1 - A ) ) )
Theorem	geoisum1c 13671*	The infinite sum of A x. ( R ^ 1 ) + A x. ( R ^ 2 )... is ( A x. R ) / ( 1 - R ). (Contributed by NM, 2-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> sum_ k e. NN ( A x. ( R ^ k ) ) = ( ( A x. R ) / ( 1 - R ) ) )
Theorem	0.999... 13672	The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 10 ^ 1 + 9 / 10 ^ 2 + 9 / 10 ^ 3 + ..., is exactly equal to 1, according to ZF set theory. Interestingly, about 40% of the people responding to a poll at http://forum.physorg.com/index.php?showtopic=13177 disagree. (Contributed by NM, 2-Nov-2007.)
|- sum_ k e. NN ( 9 / ( 10 ^ k ) ) = 1
Theorem	geoihalfsum 13673	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 13670. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 13672 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.)
|- sum_ k e. NN ( 1 / ( 2 ^ k ) ) = 1
5.9.10  Ratio test for infinite series convergence
Theorem	cvgrat 13674*	Ratio test for convergence of a complex infinite series. If the ratio A of the absolute values of successive terms in an infinite sequence F is less than 1 for all terms beyond some index B, then the infinite sum of the terms of F converges to a complex number. Equivalent to first part of Exercise 4 of [Gleason] p. 182. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 27-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> A e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. W ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )   =>    |- ( ph -> seq M ( + , F ) e. dom ~~> )
5.9.11  Mertens' theorem
Theorem	mertenslem1 13675*	Lemma for mertens 13677. (Contributed by Mario Carneiro, 29-Apr-2014.)
|- ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )   &    |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )   &    |- ( ( ph /\ j e. NN0 ) -> A e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. NN0 ) -> B e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )   &    |- ( ph -> seq 0 ( + , K ) e. dom ~~> )   &    |- ( ph -> seq 0 ( + , G ) e. dom ~~> )   &    |- ( ph -> E e. RR+ )   &    |- T = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }   &    |- ( ps <-> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )   &    |- ( ph -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )   &    |- ( ph -> ( 0 <_ sup ( T , RR , < ) /\ ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) ) )   =>    |- ( ph -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
Theorem	mertenslem2 13676*	Lemma for mertens 13677. (Contributed by Mario Carneiro, 28-Apr-2014.)
|- ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )   &    |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )   &    |- ( ( ph /\ j e. NN0 ) -> A e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. NN0 ) -> B e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )   &    |- ( ph -> seq 0 ( + , K ) e. dom ~~> )   &    |- ( ph -> seq 0 ( + , G ) e. dom ~~> )   &    |- ( ph -> E e. RR+ )   &    |- T = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }   &    |- ( ps <-> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )   =>    |- ( ph -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
Theorem	mertens 13677*	Mertens' theorem. If A ( j ) is an absolutely convergent series and B ( k ) is convergent, then ( sum_ j e. NN0 A ( j ) x. sum_ k e. NN0 B ( k ) ) = sum_ k e. NN0 sum_ j e. ( 0 ... k ) ( A ( j ) x. B ( k - j ) ) (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.)
|- ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )   &    |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )   &    |- ( ( ph /\ j e. NN0 ) -> A e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. NN0 ) -> B e. CC )   &    |- ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )   &    |- ( ph -> seq 0 ( + , K ) e. dom ~~> )   &    |- ( ph -> seq 0 ( + , G ) e. dom ~~> )   =>    |- ( ph -> seq 0 ( + , H ) ~~> ( sum_ j e. NN0 A x. sum_ k e. NN0 B ) )
5.9.12  Finite and infinite products
5.9.12.1  Product sequences
Theorem	prodf 13678*	An infinite product of complex terms is a function from an upper set of integers to CC. (Contributed by Scott Fenton, 4-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> seq M ( x. , F ) : Z --> CC )
Theorem	clim2prod 13679*	The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq ( N + 1 ) ( x. , F ) ~~> A )   =>    |- ( ph -> seq M ( x. , F ) ~~> ( ( seq M ( x. , F ) ` N ) x. A ) )
Theorem	clim2div 13680*	The limit of an infinite product with an initial segment removed. (Contributed by Scott Fenton, 20-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq M ( x. , F ) ~~> A )   &    |- ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )   =>    |- ( ph -> seq ( N + 1 ) ( x. , F ) ~~> ( A / ( seq M ( x. , F ) ` N ) ) )
Theorem	prodfmul 13681*	The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) x. ( seq M ( x. , G ) ` N ) ) )
Theorem	prodf1 13682	The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> ( seq M ( x. , ( Z X. { 1 } ) ) ` N ) = 1 )
Theorem	prodf1f 13683	A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) = ( Z X. { 1 } ) )
Theorem	prodfclim1 13684	The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )
Theorem	prodfn0 13685*	No term of a non-zero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )   =>    |- ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )
Theorem	prodfrec 13686*	The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( 1 / ( F ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) )
Theorem	prodfdiv 13687*	The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) =/= 0 )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) / ( seq M ( x. , G ) ` N ) ) )
5.9.12.2  Non-trivial convergence
Theorem	ntrivcvg 13688*	A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> seq M ( x. , F ) e. dom ~~> )
Theorem	ntrivcvgn0 13689*	A product that converges to a non-zero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
Theorem	ntrivcvgfvn0 13690*	Any value of a product sequence that converges to a non-zero value is itself non-zero. (Contributed by Scott Fenton, 20-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ph -> X =/= 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )
Theorem	ntrivcvgtail 13691*	A tail of a non-trivially convergent sequence converges non-trivially. (Contributed by Scott Fenton, 20-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> seq M ( x. , F ) ~~> X )   &    |- ( ph -> X =/= 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) )
Theorem	ntrivcvgmullem 13692*	Lemma for ntrivcvgmul 13693. (Contributed by Scott Fenton, 19-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> P e. Z )   &    |- ( ph -> X =/= 0 )   &    |- ( ph -> Y =/= 0 )   &    |- ( ph -> seq N ( x. , F ) ~~> X )   &    |- ( ph -> seq P ( x. , G ) ~~> Y )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ph -> N <_ P )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> E. q e. Z E. w ( w =/= 0 /\ seq q ( x. , H ) ~~> w ) )
Theorem	ntrivcvgmul 13693*	The product of two non-trivially converging products converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) )
5.9.12.3  Complex products
Syntax	cprod 13694	Extend class notation to include complex products.
class prod_ k e. A B
Definition	df-prod 13695*	Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sum 13491 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a non-zero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.)
|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
Theorem	prodex 13696	A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.)
|- prod_ k e. A B e. _V
Theorem	prodeq1f 13697	Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
|- F/_ k A   &    |- F/_ k B   =>    |- ( A = B -> prod_ k e. A C = prod_ k e. B C )
Theorem	prodeq1 13698*	Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
|- ( A = B -> prod_ k e. A C = prod_ k e. B C )
Theorem	nfcprod1 13699*	Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.)
|- F/_ k A   =>    |- F/_ k prod_ k e. A B
Theorem	nfcprod 13700*	Bound-variable hypothesis builder for product: if x is (effectively) not free in A and B, it is not free in prod_ k e. A B. (Contributed by Scott Fenton, 1-Dec-2017.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x prod_ k e. A B