P. 235 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ulmshft 23401*	A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` ( M + K ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   &    |- ( ph -> H = ( n e. W |-> ( F ` ( n - K ) ) ) )   =>    |- ( ph -> ( F ( ~~> u ` S ) G <-> H ( ~~> u ` S ) G ) )
Theorem	ulm0 23402	Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   &    |- ( ph -> G : S --> CC )   =>    |- ( ( ph /\ S = (/) ) -> F ( ~~> u ` S ) G )
Theorem	ulmuni 23403	An sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.)
|- ( ( F ( ~~> u ` S ) G /\ F ( ~~> u ` S ) H ) -> G = H )
Theorem	ulmdm 23404	Two ways to express that a function has a limit. (The expression ( ( ~~> u ` S ) ` F ) is sometimes useful as a shorthand for "the unique limit of the function F"). (Contributed by Mario Carneiro, 5-Jul-2017.)
|- ( F e. dom ( ~~> u ` S ) <-> F ( ~~> u ` S ) ( ( ~~> u ` S ) ` F ) )
Theorem	ulmcaulem 23405*	Lemma for ulmcau 23406 and ulmcau2 23407: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 13473. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   =>    |- ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
Theorem	ulmcau 23406*	A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k the functions F ( k ) and F ( j ) are uniformly within x of each other on S. This is the four-quantifier version, see ulmcau2 23407 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   =>    |- ( ph -> ( F e. dom ( ~~> u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
Theorem	ulmcau2 23407*	A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k , m the functions F ( k ) and F ( m ) are uniformly within x of each other on S. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   =>    |- ( ph -> ( F e. dom ( ~~> u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
Theorem	ulmss 23408*	A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> T C_ S )   &    |- ( ( ph /\ x e. Z ) -> A e. W )   &    |- ( ph -> ( x e. Z |-> A ) ( ~~> u ` S ) G )   =>    |- ( ph -> ( x e. Z |-> ( A |` T ) ) ( ~~> u ` T ) ( G |` T ) )
Theorem	ulmbdd 23409*	A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   &    |- ( ( ph /\ k e. Z ) -> E. x e. RR A. z e. S ( abs ` ( ( F ` k ) ` z ) ) <_ x )   &    |- ( ph -> F ( ~~> u ` S ) G )   =>    |- ( ph -> E. x e. RR A. z e. S ( abs ` ( G ` z ) ) <_ x )
Theorem	ulmcn 23410	A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> ( S -cn-> CC ) )   &    |- ( ph -> F ( ~~> u ` S ) G )   =>    |- ( ph -> G e. ( S -cn-> CC ) )
Theorem	ulmdvlem1 23411*	Lemma for ulmdv 23414. (Contributed by Mario Carneiro, 3-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> ( CC ^m X ) )   &    |- ( ph -> G : X --> CC )   &    |- ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )   &    |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H )   &    |- ( ( ph /\ ps ) -> C e. X )   &    |- ( ( ph /\ ps ) -> R e. RR+ )   &    |- ( ( ph /\ ps ) -> U e. RR+ )   &    |- ( ( ph /\ ps ) -> W e. RR+ )   &    |- ( ( ph /\ ps ) -> U < W )   &    |- ( ( ph /\ ps ) -> ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) C_ X )   &    |- ( ( ph /\ ps ) -> ( abs ` ( Y - C ) ) < U )   &    |- ( ( ph /\ ps ) -> N e. Z )   &    |- ( ( ph /\ ps ) -> A. m e. ( ZZ>= ` N ) A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) )   &    |- ( ( ph /\ ps ) -> ( abs ` ( ( ( S _D ( F ` N ) ) ` C ) - ( H ` C ) ) ) < ( R / 2 ) )   &    |- ( ( ph /\ ps ) -> Y e. X )   &    |- ( ( ph /\ ps ) -> Y =/= C )   &    |- ( ( ph /\ ps ) -> ( ( abs ` ( Y - C ) ) < W -> ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) < ( ( R / 2 ) / 2 ) ) )   =>    |- ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( H ` C ) ) ) < R )
Theorem	ulmdvlem2 23412*	Lemma for ulmdv 23414. (Contributed by Mario Carneiro, 8-May-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> ( CC ^m X ) )   &    |- ( ph -> G : X --> CC )   &    |- ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )   &    |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H )   =>    |- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )
Theorem	ulmdvlem3 23413*	Lemma for ulmdv 23414. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> ( CC ^m X ) )   &    |- ( ph -> G : X --> CC )   &    |- ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )   &    |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H )   =>    |- ( ( ph /\ z e. X ) -> z ( S _D G ) ( H ` z ) )
Theorem	ulmdv 23414*	If F is a sequence of differentiable functions on X which converge pointwise to G, and the derivatives of F ( n ) converge uniformly to H, then G is differentiable with derivative H. (Contributed by Mario Carneiro, 27-Feb-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> ( CC ^m X ) )   &    |- ( ph -> G : X --> CC )   &    |- ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )   &    |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H )   =>    |- ( ph -> ( S _D G ) = H )
Theorem	mtest 23415*	The Weierstrass M-test. If F is a sequence of functions which are uniformly bounded by the convergent sequence M ( k ), then the series generated by the sequence F converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015.)
|- Z = ( ZZ>= ` N )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   &    |- ( ph -> M e. W )   &    |- ( ( ph /\ k e. Z ) -> ( M ` k ) e. RR )   &    |- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )   &    |- ( ph -> seq N ( + , M ) e. dom ~~> )   =>    |- ( ph -> seq N ( oF + , F ) e. dom ( ~~> u ` S ) )
Theorem	mtestbdd 23416*	Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017.)
|- Z = ( ZZ>= ` N )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ph -> F : Z --> ( CC ^m S ) )   &    |- ( ph -> M e. W )   &    |- ( ( ph /\ k e. Z ) -> ( M ` k ) e. RR )   &    |- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )   &    |- ( ph -> seq N ( + , M ) e. dom ~~> )   &    |- ( ph -> seq N ( oF + , F ) ( ~~> u ` S ) T )   =>    |- ( ph -> E. x e. RR A. z e. S ( abs ` ( T ` z ) ) <_ x )
Theorem	mbfulm 23417	A uniform limit of measurable functions is measurable. (This is just a corollary of the fact that a pointwise limit of measurable functions is measurable, see mbflim 22682.) (Contributed by Mario Carneiro, 18-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z -->MblFn )   &    |- ( ph -> F ( ~~> u ` S ) G )   =>    |- ( ph -> G e. MblFn )
Theorem	iblulm 23418	A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> L^1 )   &    |- ( ph -> F ( ~~> u ` S ) G )   &    |- ( ph -> ( vol ` S ) e. RR )   =>    |- ( ph -> G e. L^1 )
Theorem	itgulm 23419*	A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> L^1 )   &    |- ( ph -> F ( ~~> u ` S ) G )   &    |- ( ph -> ( vol ` S ) e. RR )   =>    |- ( ph -> ( k e. Z |-> S. S ( ( F ` k ) ` x ) _d x ) ~~> S. S ( G ` x ) _d x )
Theorem	itgulm2 23420*	A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) e. ( S -cn-> CC ) )   &    |- ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) e. L^1 )   &    |- ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) ( ~~> u ` S ) ( x e. S |-> B ) )   &    |- ( ph -> ( vol ` S ) e. RR )   =>    |- ( ph -> ( ( x e. S |-> B ) e. L^1 /\ ( k e. Z |-> S. S A _d x ) ~~> S. S B _d x ) )
14.2.3  Power series
Theorem	pserval 23421*	Value of the function G that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   =>    |- ( X e. CC -> ( G ` X ) = ( m e. NN0 |-> ( ( A ` m ) x. ( X ^ m ) ) ) )
Theorem	pserval2 23422*	Value of the function G that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   =>    |- ( ( X e. CC /\ N e. NN0 ) -> ( ( G ` X ) ` N ) = ( ( A ` N ) x. ( X ^ N ) ) )
Theorem	psergf 23423*	The sequence of terms in the infinite sequence defining a power series for fixed X. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> X e. CC )   =>    |- ( ph -> ( G ` X ) : NN0 --> CC )
Theorem	radcnvlem1 23424*	Lemma for radcnvlt1 23429, radcnvle 23431. If X is a point closer to zero than Y and the power series converges at Y, then it converges absolutely at X, even if the terms in the sequence are multiplied by n. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> Y e. CC )   &    |- ( ph -> ( abs ` X ) < ( abs ` Y ) )   &    |- ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> )   &    |- H = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )   =>    |- ( ph -> seq 0 ( + , H ) e. dom ~~> )
Theorem	radcnvlem2 23425*	Lemma for radcnvlt1 23429, radcnvle 23431. If X is a point closer to zero than Y and the power series converges at Y, then it converges absolutely at X. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> Y e. CC )   &    |- ( ph -> ( abs ` X ) < ( abs ` Y ) )   &    |- ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> )   =>    |- ( ph -> seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> )
Theorem	radcnvlem3 23426*	Lemma for radcnvlt1 23429, radcnvle 23431. If X is a point closer to zero than Y and the power series converges at Y, then it converges at X. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> Y e. CC )   &    |- ( ph -> ( abs ` X ) < ( abs ` Y ) )   &    |- ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> )   =>    |- ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
Theorem	radcnv0 23427*	Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   =>    |- ( ph -> 0 e. { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
Theorem	radcnvcl 23428*	The radius of convergence R of an infinite series is a nonnegative extended real number. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   =>    |- ( ph -> R e. ( 0 [,] +oo ) )
Theorem	radcnvlt1 23429*	If X is within the open disk of radius R centered at zero, then the infinite series converges absolutely at X, and also converges when the series is multiplied by n. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- ( ph -> X e. CC )   &    |- ( ph -> ( abs ` X ) < R )   &    |- H = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )   =>    |- ( ph -> ( seq 0 ( + , H ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) )
Theorem	radcnvlt2 23430*	If X is within the open disk of radius R centered at zero, then the infinite series converges at X. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- ( ph -> X e. CC )   &    |- ( ph -> ( abs ` X ) < R )   =>    |- ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
Theorem	radcnvle 23431*	If X is a convergent point of the infinite series, then X is within the closed disk of radius R centered at zero. Or, by contraposition, the series diverges at any point strictly more than R from the origin. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- ( ph -> X e. CC )   &    |- ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )   =>    |- ( ph -> ( abs ` X ) <_ R )
Theorem	dvradcnv 23432*	The radius of convergence of the (formal) derivative H of the power series G is at least as large as the radius of convergence of G. (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- H = ( n e. NN0 |-> ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( X ^ n ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> ( abs ` X ) < R )   =>    |- ( ph -> seq 0 ( + , H ) e. dom ~~> )
Theorem	pserulm 23433*	If S is a region contained in a circle of radius M < R, then the sequence of partial sums of the infinite series converges uniformly on S. (Contributed by Mario Carneiro, 26-Feb-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- H = ( i e. NN0 |-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )   &    |- ( ph -> M e. RR )   &    |- ( ph -> M < R )   &    |- ( ph -> S C_ ( `' abs " ( 0 [,] M ) ) )   =>    |- ( ph -> H ( ~~> u ` S ) F )
Theorem	psercn2 23434*	Since by pserulm 23433 the series converges uniformly, it is also continuous by ulmcn 23410. (Contributed by Mario Carneiro, 3-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- H = ( i e. NN0 |-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )   &    |- ( ph -> M e. RR )   &    |- ( ph -> M < R )   &    |- ( ph -> S C_ ( `' abs " ( 0 [,] M ) ) )   =>    |- ( ph -> F e. ( S -cn-> CC ) )
Theorem	psercnlem2 23435*	Lemma for psercn 23437. (Contributed by Mario Carneiro, 18-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- S = ( `' abs " ( 0 [,) R ) )   &    |- ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )   =>    |- ( ( ph /\ a e. S ) -> ( a e. ( 0 ( ball ` ( abs o. - ) ) M ) /\ ( 0 ( ball ` ( abs o. - ) ) M ) C_ ( `' abs " ( 0 [,] M ) ) /\ ( `' abs " ( 0 [,] M ) ) C_ S ) )
Theorem	psercnlem1 23436*	Lemma for psercn 23437. (Contributed by Mario Carneiro, 18-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- S = ( `' abs " ( 0 [,) R ) )   &    |- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )   =>    |- ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )
Theorem	psercn 23437*	An infinite series converges to a continuous function on the open disk of radius R, where R is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- S = ( `' abs " ( 0 [,) R ) )   &    |- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )   =>    |- ( ph -> F e. ( S -cn-> CC ) )
Theorem	pserdvlem1 23438*	Lemma for pserdv 23440. (Contributed by Mario Carneiro, 7-May-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- S = ( `' abs " ( 0 [,) R ) )   &    |- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )   =>    |- ( ( ph /\ a e. S ) -> ( ( ( ( abs ` a ) + M ) / 2 ) e. RR+ /\ ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) /\ ( ( ( abs ` a ) + M ) / 2 ) < R ) )
Theorem	pserdvlem2 23439*	Lemma for pserdv 23440. (Contributed by Mario Carneiro, 7-May-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- S = ( `' abs " ( 0 [,) R ) )   &    |- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )   &    |- B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )   =>    |- ( ( ph /\ a e. S ) -> ( CC _D ( F |` B ) ) = ( y e. B |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
Theorem	pserdv 23440*	The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- S = ( `' abs " ( 0 [,) R ) )   &    |- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )   &    |- B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )   =>    |- ( ph -> ( CC _D F ) = ( y e. S |-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
Theorem	pserdv2 23441*	The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- S = ( `' abs " ( 0 [,) R ) )   &    |- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )   &    |- B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )   =>    |- ( ph -> ( CC _D F ) = ( y e. S |-> sum_ k e. NN ( ( k x. ( A ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) )
Theorem	abelthlem1 23442*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   =>    |- ( ph -> 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
Theorem	abelthlem2 23443*	Lemma for abelth 23452. The peculiar region S, known as a Stolz angle , is a teardrop-shaped subset of the closed unit ball containing 1. Indeed, except for 1 itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   =>    |- ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
Theorem	abelthlem3 23444*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   =>    |- ( ( ph /\ X e. S ) -> seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) e. dom ~~> )
Theorem	abelthlem4 23445*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   =>    |- ( ph -> F : S --> CC )
Theorem	abelthlem5 23446*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   &    |- ( ph -> seq 0 ( + , A ) ~~> 0 )   =>    |- ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> seq 0 ( + , ( k e. NN0 |-> ( ( seq 0 ( + , A ) ` k ) x. ( X ^ k ) ) ) ) e. dom ~~> )
Theorem	abelthlem6 23447*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   &    |- ( ph -> seq 0 ( + , A ) ~~> 0 )   &    |- ( ph -> X e. ( S \ { 1 } ) )   =>    |- ( ph -> ( F ` X ) = ( ( 1 - X ) x. sum_ n e. NN0 ( ( seq 0 ( + , A ) ` n ) x. ( X ^ n ) ) ) )
Theorem	abelthlem7a 23448*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 8-May-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   &    |- ( ph -> seq 0 ( + , A ) ~~> 0 )   &    |- ( ph -> X e. ( S \ { 1 } ) )   =>    |- ( ph -> ( X e. CC /\ ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) ) )
Theorem	abelthlem7 23449*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   &    |- ( ph -> seq 0 ( + , A ) ~~> 0 )   &    |- ( ph -> X e. ( S \ { 1 } ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A. k e. ( ZZ>= ` N ) ( abs ` ( seq 0 ( + , A ) ` k ) ) < R )   &    |- ( ph -> ( abs ` ( 1 - X ) ) < ( R / ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( seq 0 ( + , A ) ` n ) ) + 1 ) ) )   =>    |- ( ph -> ( abs ` ( F ` X ) ) < ( ( M + 1 ) x. R ) )
Theorem	abelthlem8 23450*	Lemma for abelth 23452. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   &    |- ( ph -> seq 0 ( + , A ) ~~> 0 )   =>    |- ( ( ph /\ R e. RR+ ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )
Theorem	abelthlem9 23451*	Lemma for abelth 23452. By adjusting the constant term, we can assume that the entire series converges to 0. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   =>    |- ( ( ph /\ R e. RR+ ) -> E. w e. RR+ A. y e. S ( ( abs ` ( 1 - y ) ) < w -> ( abs ` ( ( F ` 1 ) - ( F ` y ) ) ) < R ) )
Theorem	abelth 23452*	Abel's theorem. If the power series sum_ n e. NN0 A ( n ) ( x ^ n ) is convergent at 1, then it is equal to the limit from "below", along a Stolz angle S (note that the M = 1 case of a Stolz angle is the real line [ 0 , 1 ]). (Continuity on S \ { 1 } follows more generally from psercn 23437.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- ( ph -> M e. RR )   &    |- ( ph -> 0 <_ M )   &    |- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }   &    |- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   =>    |- ( ph -> F e. ( S -cn-> CC ) )
Theorem	abelth2 23453*	Abel's theorem, restricted to the [ 0 , 1 ] interval. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ph -> A : NN0 --> CC )   &    |- ( ph -> seq 0 ( + , A ) e. dom ~~> )   &    |- F = ( x e. ( 0 [,] 1 ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )   =>    |- ( ph -> F e. ( ( 0 [,] 1 ) -cn-> CC ) )
14.3  Basic trigonometry
14.3.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 23454	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
|- exp e. ( CC -cn-> CC )
Theorem	sincn 23455	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- sin e. ( CC -cn-> CC )
Theorem	coscn 23456	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- cos e. ( CC -cn-> CC )
Theorem	reeff1olem 23457*	Lemma for reeff1o 23458. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( ( U e. RR /\ 1 < U ) -> E. x e. RR ( exp ` x ) = U )
Theorem	reeff1o 23458	The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( exp |` RR ) : RR -1-1-onto-> RR+
Theorem	reefiso 23459	The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
|- ( exp |` RR ) Isom < , < ( RR , RR+ )
Theorem	efcvx 23460	The exponential function on the reals is a strictly convex function. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( exp ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < ( ( T x. ( exp ` A ) ) + ( ( 1 - T ) x. ( exp ` B ) ) ) )
Theorem	reefgim 23461	The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.)
|- P = ( (mulGrp ` ℂfld ) ↾s RR+ )   =>    |- ( exp |` RR ) e. (RRfld GrpIso P )
14.3.2  Properties of pi = 3.14159...
Theorem	pilem1 23462	Lemma for pire 23469, pigt2lt4 23467 and sinpi 23468. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
Theorem	pilem2 23463	Lemma for pire 23469, pigt2lt4 23467 and sinpi 23468. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
|- ( ph -> A e. ( 2 (,) 4 ) )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> ( sin ` A ) = 0 )   &    |- ( ph -> ( sin ` B ) = 0 )   &    |- ( ph -> pi < A )   =>    |- ( ph -> ( ( pi + A ) / 2 ) <_ B )
Theorem	pilem2OLD 23464	Lemma for pire 23469, pigt2lt4 23467 and sinpi 23468. (Contributed by Mario Carneiro, 12-Jun-2014.) Obsolete version of pilem2 23463 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A e. ( 2 (,) 4 ) )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> ( sin ` A ) = 0 )   &    |- ( ph -> ( sin ` B ) = 0 )   &    |- ( ph -> pi < A )   =>    |- ( ph -> ( ( pi + A ) / 2 ) <_ B )
Theorem	pilem3 23465	Lemma for pire 23469, pigt2lt4 23467 and sinpi 23468. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pilem3OLD 23466	Lemma for pire 23469, pigt2lt4 23467 and sinpi 23468. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) Obsolete version of pilem3 23465 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pigt2lt4 23467	pi is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( 2 < pi /\ pi < 4 )
Theorem	sinpi 23468	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 23469	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 23470	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 23471	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 23472	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 23473	-u pi is a real number (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 23474	Lemma for sinhalfpi 23479 and coshalfpi 23480. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 23475	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 23476	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 23477	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 23478	Adding pi / 2 to itself is pi (common case). See 2halves 10875. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 23479	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 23480	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 23481	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 23482	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 23483	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 23484	The exponential of _i x. pi. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( exp ` ( _i x. pi ) ) = -u 1
Theorem	eulerid 23485	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( ( exp ` ( _i x. pi ) ) + 1 ) = 0
Theorem	sin2pi 23486	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 23487	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 23488	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 23489	The exponential of 2 K pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. pi ) ) x. K ) ) = 1 )
Theorem	efper 23490	The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. pi ) ) x. K ) ) ) = ( exp ` A ) )
Theorem	sinperlem 23491	Lemma for sinper 23492 and cosper 23493. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )   &    |- ( ( A + ( K x. ( 2 x. pi ) ) ) e. CC -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) ) / D ) )   =>    |- ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( F ` A ) )
Theorem	sinper 23492	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( sin ` A ) )
Theorem	cosper 23493	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( cos ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( cos ` A ) )
Theorem	sin2kpi 23494	If K is an integer, the sine of 2 K pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( sin ` ( K x. ( 2 x. pi ) ) ) = 0 )
Theorem	cos2kpi 23495	If K is an integer, the cosine of 2 K pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( cos ` ( K x. ( 2 x. pi ) ) ) = 1 )
Theorem	sin2pim 23496	Sine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( ( 2 x. pi ) - A ) ) = -u ( sin ` A ) )
Theorem	cos2pim 23497	Cosine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( ( 2 x. pi ) - A ) ) = ( cos ` A ) )
Theorem	sinmpi 23498	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 23499	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 23500	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )