P. 161 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16001-16100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	plycolemc 16001*	Lemma for plyco 16002. The result expressed as a sum, with a degree and coefficients for F specified as hypotheses. (Contributed by Jim Kingdon, 20-Sep-2025.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) )   =>    |- ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( G ` z ) ^ k ) ) ) e. (Poly ` S ) )
Theorem	plyco 16002*	The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   =>    |- ( ph -> ( F o. G ) e. (Poly ` S ) )
Theorem	plycjlemc 16003*	Lemma for plycj 16004. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.)
|- ( ph -> N e. NN0 )   &    |- G = ( ( * o. F ) o. * )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> F e. (Poly ` S ) )   =>    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )
Theorem	plycj 16004*	The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on ( * ` z ) independently of z.) (Contributed by Mario Carneiro, 24-Jul-2014.)
|- G = ( ( * o. F ) o. * )   &    |- ( ( ph /\ x e. S ) -> ( * ` x ) e. S )   &    |- ( ph -> F e. (Poly ` S ) )   =>    |- ( ph -> G e. (Poly ` S ) )
Theorem	plycn 16005	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8308. (Revised by GG, 16-Mar-2025.)
|- ( F e. (Poly ` S ) -> F e. ( CC -cn-> CC ) )
Theorem	plyrecj 16006	A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ( F e. (Poly ` RR ) /\ A e. CC ) -> ( * ` ( F ` A ) ) = ( F ` ( * ` A ) ) )
Theorem	plyreres 16007	Real-coefficient polynomials restrict to real functions. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( F e. (Poly ` RR ) -> ( F |` RR ) : RR --> RR )
Theorem	dvply1 16008*	Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- B = ( k e. NN0 |-> ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( CC _D F ) = G )
Theorem	dvply2g 16009	The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017.) (Revised by GG, 30-Apr-2025.)
|- ( ( S e. (SubRing ` ℂfld ) /\ F e. (Poly ` S ) ) -> ( CC _D F ) e. (Poly ` S ) )
Theorem	dvply2 16010	The derivative of a polynomial is a polynomial. (Contributed by Stefan O'Rear, 14-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|- ( F e. (Poly ` S ) -> ( CC _D F ) e. (Poly ` CC ) )
11.2  Basic trigonometry
11.2.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 16011	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 16012	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- sin e. ( CC -cn-> CC )
Theorem	coscn 16013	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
|- cos e. ( CC -cn-> CC )
Theorem	reeff1olem 16014*	Lemma for reeff1o 16016. (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	reeff1oleme 16015*	Lemma for reeff1o 16016. (Contributed by Jim Kingdon, 15-May-2024.)
|- ( U e. ( 0 (,) _e ) -> E. x e. RR ( exp ` x ) = U )
Theorem	reeff1o 16016	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	efltlemlt 16017	Lemma for eflt 16018. The converse of efltim 12489 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( exp ` A ) < ( exp ` B ) )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> ( ( abs ` ( A - B ) ) < D -> ( abs ` ( ( exp ` A ) - ( exp ` B ) ) ) < ( ( exp ` B ) - ( exp ` A ) ) ) )   =>    |- ( ph -> A < B )
Theorem	eflt 16018	The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( exp ` A ) < ( exp ` B ) ) )
Theorem	efle 16019	The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( exp ` A ) <_ ( exp ` B ) ) )
Theorem	reefiso 16020	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	reapef 16021	Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.)
|- ( ( A e. RR /\ B e. RR ) -> ( A # B <-> ( exp ` A ) # ( exp ` B ) ) )
Theorem	efap1p 16022	If the exponential of a number is apart from one plus that number, the number is apart from zero. To some extent can be thought of as the converse of efgt1p 12487. (Contributed by Jim Kingdon, 13-Aug-2026.)
|- ( ( A e. RR /\ ( 1 + A ) # ( exp ` A ) ) -> A # 0 )
11.2.2  Properties of pi = 3.14159...
Theorem	pilem1 16023	Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 9-May-2014.)
|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
Theorem	cosz12 16024	Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.)
|- E. p e. ( 1 (,) 2 ) ( cos ` p ) = 0
Theorem	sin0pilem1 16025*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
|- E. p e. ( 1 (,) 2 ) ( ( cos ` p ) = 0 /\ A. x e. ( p (,) ( 2 x. p ) ) 0 < ( sin ` x ) )
Theorem	sin0pilem2 16026*	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
|- E. q e. ( 2 (,) 4 ) ( ( sin ` q ) = 0 /\ A. x e. ( 0 (,) q ) 0 < ( sin ` x ) )
Theorem	pilem3 16027	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pigt2lt4 16028	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 16029	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 16030	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 16031	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 16032	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 16033	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 16034	-u pi is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 16035	Lemma for sinhalfpi 16040 and coshalfpi 16041. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 16036	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 16037	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 16038	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 16039	Adding pi / 2 to itself gives pi. See 2halves 9545. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 16040	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 16041	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 16042	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 16043	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 16044	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 16045	The exponential of _i x. pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( exp ` ( _i x. pi ) ) = -u 1
Theorem	eulerid 16046	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 16047	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 16048	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 16049	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 16050	If K is an integer, then 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 16051	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 16052	Lemma for sinper 16053 and cosper 16054. (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 16053	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 16054	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 16055	If K is an integer, then 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 16056	If K is an integer, then 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 16057	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 16058	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 16059	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 16060	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 16061	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )
Theorem	cosppi 16062	Cosine of a number plus pi. (Contributed by NM, 18-Aug-2008.)
|- ( A e. CC -> ( cos ` ( A + pi ) ) = -u ( cos ` A ) )
Theorem	efimpi 16063	The exponential function at _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 16064	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 16065	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 16066	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 16067	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 16068	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 12535, 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 16069	Lemma for sincosq1sgn 16070. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( ( A e. RR /\ 0 < A /\ A < ( pi / 2 ) ) -> 0 < ( sin ` A ) )
Theorem	sincosq1sgn 16070	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 16071	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 16072	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 16073	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	sinq12gt0 16074	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	sinq34lt0t 16075	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 16076	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	cosq23lt0 16077	The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.)
|- ( A e. ( ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ) -> ( cos ` A ) < 0 )
Theorem	coseq0q4123 16078	Location of the zeroes of cosine in ( -u ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ). (Contributed by Jim Kingdon, 14-Mar-2024.)
|- ( A e. ( -u ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ) -> ( ( cos ` A ) = 0 <-> A = ( pi / 2 ) ) )
Theorem	coseq00topi 16079	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 16080	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 16081	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 16082	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	sincosq1eq 16083	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 16084	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 16085	The tangent of pi / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( tan ` ( pi / 4 ) ) = 1
Theorem	sincos6thpi 16086	The sine and cosine of pi / 6. (Contributed by Paul Chapman, 25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.)
|- ( ( sin ` ( pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( pi / 6 ) ) = ( ( sqr ` 3 ) / 2 ) )
Theorem	sincos3rdpi 16087	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	pigt3 16088	pi is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
|- 3 < pi
Theorem	pige3 16089	pi is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
|- 3 <_ pi
Theorem	abssinper 16090	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 16091	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 16092	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	sineq0re 16093	A complex number whose sine is zero is real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.) (Revised by Jim Kingdon, 23-Sep-2026.)
|- ( ( A e. CC /\ ( sin ` A ) = 0 ) -> A e. RR )
Theorem	cosordlem 16094	Cosine is decreasing over the closed interval from 0 to pi. (Contributed by Mario Carneiro, 10-May-2014.)
|- ( ph -> A e. ( 0 [,] pi ) )   &    |- ( ph -> B e. ( 0 [,] pi ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( cos ` B ) < ( cos ` A ) )
Theorem	cosq34lt1 16095	Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.)
|- ( A e. ( pi [,) ( 2 x. pi ) ) -> ( cos ` A ) < 1 )
Theorem	cos02pilt1 16096	Cosine is less than one between zero and 2 x. pi. (Contributed by Jim Kingdon, 19-Mar-2024.)
|- ( A e. ( 0 (,) ( 2 x. pi ) ) -> ( cos ` A ) < 1 )
Theorem	cos0pilt1 16097	Cosine is between minus one and one on the open interval between zero and pi. (Contributed by Jim Kingdon, 7-May-2024.)
|- ( A e. ( 0 (,) pi ) -> ( cos ` A ) e. ( -u 1 (,) 1 ) )
Theorem	cos11 16098	Cosine is one-to-one over the closed interval from 0 to pi. (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Jim Kingdon, 6-May-2024.)
|- ( ( A e. ( 0 [,] pi ) /\ B e. ( 0 [,] pi ) ) -> ( A = B <-> ( cos ` A ) = ( cos ` B ) ) )
Theorem	ioocosf1o 16099	The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Jim Kingdon, 7-May-2024.)
|- ( cos |` ( 0 (,) pi ) ) : ( 0 (,) pi ) -1-1-onto-> ( -u 1 (,) 1 )
Theorem	negpitopissre 16100	The interval ( -u pi (,] pi ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
|- ( -u pi (,] pi ) C_ RR