P. 230 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvradcnv 22901*	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 22902*	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 22903*	Since by pserulm 22902 the series converges uniformly, it is also continuous by ulmcn 22879. (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 22904*	Lemma for psercn 22906. (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 22905*	Lemma for psercn 22906. (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 22906*	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 22907*	Lemma for pserdv 22909. (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 22908*	Lemma for pserdv 22909. (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 22909*	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 22910*	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 22911*	Lemma for abelth 22921. (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 22912*	Lemma for abelth 22921. 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 22913*	Lemma for abelth 22921. (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 22914*	Lemma for abelth 22921. (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 22915*	Lemma for abelth 22921. (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 22916*	Lemma for abelth 22921. (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 22917*	Lemma for abelth 22921. (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 22918*	Lemma for abelth 22921. (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 22919*	Lemma for abelth 22921. (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 22920*	Lemma for abelth 22921. 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 22921*	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 22906.) (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 22922*	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 22923	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 22924	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- sin e. ( CC -cn-> CC )
Theorem	coscn 22925	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- cos e. ( CC -cn-> CC )
Theorem	reeff1olem 22926*	Lemma for reeff1o 22927. (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 22927	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 22928	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 22929	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 22930	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 22931	Lemma for pire 22936, pigt2lt4 22934 and sinpi 22935. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
Theorem	pilem2 22932	Lemma for pire 22936, pigt2lt4 22934 and sinpi 22935. (Contributed by Mario Carneiro, 12-Jun-2014.)
|- ( 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 22933	Lemma for pire 22936, pigt2lt4 22934 and sinpi 22935. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pigt2lt4 22934	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 22935	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 22936	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 22937	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 22938	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 22939	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 22940	-u pi is a real number (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 22941	Lemma for sinhalfpi 22946 and coshalfpi 22947. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 22942	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 22943	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 22944	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 22945	Adding pi / 2 to itself is pi (common case). See 2halves 10684. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 22946	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 22947	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 22948	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 22949	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 22950	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 22951	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 22952	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 22953	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 22954	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 22955	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 22956	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 22957	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 22958	Lemma for sinper 22959 and cosper 22960. (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 22959	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 22960	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 22961	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 22962	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 22963	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 22964	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 22965	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 22966	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 22967	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )
Theorem	cosppi 22968	Cosine of a complex number plus pi. (Contributed by NM, 18-Aug-2008.)
|- ( A e. CC -> ( cos ` ( A + pi ) ) = -u ( cos ` A ) )
Theorem	efimpi 22969	The exponential function of _i times a real number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( exp ` ( _i x. ( A - pi ) ) ) = -u ( exp ` ( _i x. A ) ) )
Theorem	sinhalfpip 22970	The sine of pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( sin ` ( ( pi / 2 ) + A ) ) = ( cos ` A ) )
Theorem	sinhalfpim 22971	The sine of pi / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( sin ` ( ( pi / 2 ) - A ) ) = ( cos ` A ) )
Theorem	coshalfpip 22972	The cosine of pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( ( pi / 2 ) + A ) ) = -u ( sin ` A ) )
Theorem	coshalfpim 22973	The cosine of pi / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( ( pi / 2 ) - A ) ) = ( sin ` A ) )
Theorem	ptolemy 22974	Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 13909, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ ( ( A + B ) + ( C + D ) ) = pi ) -> ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` C ) x. ( sin ` D ) ) ) = ( ( sin ` ( B + C ) ) x. ( sin ` ( A + C ) ) ) )
Theorem	sincosq1lem 22975	Lemma for sincosq1sgn 22976. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( ( A e. RR /\ 0 < A /\ A < ( pi / 2 ) ) -> 0 < ( sin ` A ) )
Theorem	sincosq1sgn 22976	The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
Theorem	sincosq2sgn 22977	The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( ( pi / 2 ) (,) pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )
Theorem	sincosq3sgn 22978	The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( pi (,) ( 3 x. ( pi / 2 ) ) ) -> ( ( sin ` A ) < 0 /\ ( cos ` A ) < 0 ) )
Theorem	sincosq4sgn 22979	The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( ( 3 x. ( pi / 2 ) ) (,) ( 2 x. pi ) ) -> ( ( sin ` A ) < 0 /\ 0 < ( cos ` A ) ) )
Theorem	coseq00topi 22980	Location of the zeroes of cosine in ( 0 [,] pi ). (Contributed by David Moews, 28-Feb-2017.)
|- ( A e. ( 0 [,] pi ) -> ( ( cos ` A ) = 0 <-> A = ( pi / 2 ) ) )
Theorem	coseq0negpitopi 22981	Location of the zeroes of cosine in ( -u pi (,] pi ). (Contributed by David Moews, 28-Feb-2017.)
|- ( A e. ( -u pi (,] pi ) -> ( ( cos ` A ) = 0 <-> A e. { ( pi / 2 ) , -u ( pi / 2 ) } ) )
Theorem	tanrpcl 22982	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> ( tan ` A ) e. RR+ )
Theorem	tangtx 22983	The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> A < ( tan ` A ) )
Theorem	tanabsge 22984	The tangent function is greater than or equal to its argument in absolute value. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( A e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) -> ( abs ` A ) <_ ( abs ` ( tan ` A ) ) )
Theorem	sinq12gt0 22985	The sine of a number strictly between 0 and pi is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. ( 0 (,) pi ) -> 0 < ( sin ` A ) )
Theorem	sinq12ge0 22986	The sine of a number between 0 and pi is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
|- ( A e. ( 0 [,] pi ) -> 0 <_ ( sin ` A ) )
Theorem	sinq34lt0t 22987	The sine of a number strictly between pi and 2 x. pi is negative. (Contributed by NM, 17-Aug-2008.)
|- ( A e. ( pi (,) ( 2 x. pi ) ) -> ( sin ` A ) < 0 )
Theorem	cosq14gt0 22988	The cosine of a number strictly between -u pi / 2 and pi / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( A e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) -> 0 < ( cos ` A ) )
Theorem	cosq14ge0 22989	The cosine of a number between -u pi / 2 and pi / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
|- ( A e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) -> 0 <_ ( cos ` A ) )
Theorem	sincosq1eq 22990	Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( sin ` ( A x. ( pi / 2 ) ) ) = ( cos ` ( B x. ( pi / 2 ) ) ) )
Theorem	sincos4thpi 22991	The sine and cosine of pi / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( sin ` ( pi / 4 ) ) = ( 1 / ( sqr ` 2 ) ) /\ ( cos ` ( pi / 4 ) ) = ( 1 / ( sqr ` 2 ) ) )
Theorem	tan4thpi 22992	The tangent of pi / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( tan ` ( pi / 4 ) ) = 1
Theorem	sincos6thpi 22993	The sine and cosine of pi / 6. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( sin ` ( pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( pi / 6 ) ) = ( ( sqr ` 3 ) / 2 ) )
Theorem	sincos3rdpi 22994	The sine and cosine of pi / 3. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( ( sin ` ( pi / 3 ) ) = ( ( sqr ` 3 ) / 2 ) /\ ( cos ` ( pi / 3 ) ) = ( 1 / 2 ) )
Theorem	pige3 22995	pi is greater or equal to 3. This proof is based on the geometric observation that a hexagon of unit side length has perimeter 6, which is less than the unit-radius circumcircle, of perimeter 2 pi. We translate this to algebra by looking at the function _e ^ ( _i x ) as x goes from 0 to pi / 3; it moves at unit speed and travels distance 1, hence 1 <_ pi / 3. (Contributed by Mario Carneiro, 21-May-2016.)
|- 3 <_ pi
Theorem	abssinper 22996	The absolute value of sine has period pi. (Contributed by NM, 17-Aug-2008.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. pi ) ) ) ) = ( abs ` ( sin ` A ) ) )
Theorem	sinkpi 22997	The sine of an integer multiple of pi is 0. (Contributed by NM, 11-Aug-2008.)
|- ( K e. ZZ -> ( sin ` ( K x. pi ) ) = 0 )
Theorem	coskpi 22998	The absolute value of the cosine of an integer multiple of pi is 1. (Contributed by NM, 19-Aug-2008.)
|- ( K e. ZZ -> ( abs ` ( cos ` ( K x. pi ) ) ) = 1 )
Theorem	sineq0 22999	A complex number whose sine is zero is an integer multiple of pi. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( ( sin ` A ) = 0 <-> ( A / pi ) e. ZZ ) )
Theorem	coseq1 23000	A complex number whose cosine is one is an integer multiple of 2 pi. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. CC -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. pi ) ) e. ZZ ) )