Theorem List for Intuitionistic Logic Explorer - 12901-13000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | reeff1oleme 12901* |
Lemma for reeff1o 12902. (Contributed by Jim Kingdon, 15-May-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![(,) (,)](_ioo.gif) ![_e _e](rme.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![U U](_cu.gif) ![) )](rp.gif) |
|
Theorem | reeff1o 12902 |
The real exponential function is one-to-one onto. (Contributed by Paul
Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) ![: :](colon.gif) ![RR RR](bbr.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![RR+ RR+](_bbrplus.gif) |
|
Theorem | efltlemlt 12903 |
Lemma for eflt 12904. The converse of efltim 11441 plus the epsilon-delta
setup. (Contributed by Jim Kingdon, 22-May-2024.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![B B](_cb.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | eflt 12904 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
21-May-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | efle 12905 |
The exponential function on the reals is nondecreasing. (Contributed by
Mario Carneiro, 11-Mar-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reefiso 12906 |
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.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
|
Theorem | reapef 12907 |
Apartness and the exponential function for reals. (Contributed by Jim
Kingdon, 11-Jul-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) # ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![A A](_ca.gif) # ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
9.1.2 Properties of pi =
3.14159...
|
|
Theorem | pilem1 12908 |
Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro,
9-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![sin sin](_sin.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![0 0](0.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![0 0](0.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | cosz12 12909 |
Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and
Jim Kingdon, 7-Mar-2024.)
|
![E.
E.](exists.gif) ![( (](lp.gif) ![1
1](1.gif) ![(,) (,)](_ioo.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![p p](_p.gif) ![0 0](0.gif) |
|
Theorem | sin0pilem1 12910* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
![E.
E.](exists.gif) ![( (](lp.gif) ![1
1](1.gif) ![(,) (,)](_ioo.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![p p](_p.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![p p](_p.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![p p](_p.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sin0pilem2 12911* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
![E.
E.](exists.gif) ![( (](lp.gif) ![2
2](2.gif) ![(,) (,)](_ioo.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![q q](_q.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![q q](_q.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pilem3 12912 |
Lemma for pi related theorems. (Contributed by Jim Kingdon,
9-Mar-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![(,) (,)](_ioo.gif) ![4 4](4.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![`
`](backtick.gif) ![pi pi](pi.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | pigt2lt4 12913 |
is between 2 and 4.
(Contributed by Paul Chapman, 23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
![( (](lp.gif)
![4 4](4.gif) ![) )](rp.gif) |
|
Theorem | sinpi 12914 |
The sine of is 0.
(Contributed by Paul Chapman, 23-Jan-2008.)
|
![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![pi pi](pi.gif)
![0 0](0.gif) |
|
Theorem | pire 12915 |
is a real number.
(Contributed by Paul Chapman, 23-Jan-2008.)
|
![RR RR](bbr.gif) |
|
Theorem | picn 12916 |
is a complex number.
(Contributed by David A. Wheeler,
6-Dec-2018.)
|
![CC CC](bbc.gif) |
|
Theorem | pipos 12917 |
is positive.
(Contributed by Paul Chapman, 23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
![pi pi](pi.gif) |
|
Theorem | pirp 12918 |
is a positive real.
(Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
![RR+ RR+](_bbrplus.gif) |
|
Theorem | negpicn 12919 |
![-u -u](shortminus.gif) is a real number.
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
![-u -u](shortminus.gif) ![CC CC](bbc.gif) |
|
Theorem | sinhalfpilem 12920 |
Lemma for sinhalfpi 12925 and coshalfpi 12926. (Contributed by Paul Chapman,
23-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | halfpire 12921 |
is real. (Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) |
|
Theorem | neghalfpire 12922 |
![-u -u](shortminus.gif) is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) |
|
Theorem | neghalfpirx 12923 |
![-u -u](shortminus.gif) is an extended real. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![RR* RR*](_bbrast.gif) |
|
Theorem | pidiv2halves 12924 |
Adding to itself gives . See 2halves 8973.
(Contributed by David A. Wheeler, 8-Dec-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![pi pi](pi.gif) |
|
Theorem | sinhalfpi 12925 |
The sine of is 1. (Contributed by Paul Chapman,
23-Jan-2008.)
|
![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) |
|
Theorem | coshalfpi 12926 |
The cosine of is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![0 0](0.gif) |
|
Theorem | cosneghalfpi 12927 |
The cosine of ![-u -u](shortminus.gif) is zero. (Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![0 0](0.gif) |
|
Theorem | efhalfpi 12928 |
The exponential of ![_i _i](rmi.gif) is . (Contributed by Mario
Carneiro, 9-May-2014.)
|
![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![_i _i](rmi.gif) |
|
Theorem | cospi 12929 |
The cosine of is
![-u -u](shortminus.gif) . (Contributed by Paul
Chapman,
23-Jan-2008.)
|
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![pi pi](pi.gif)
![-u -u](shortminus.gif) ![1 1](1.gif) |
|
Theorem | efipi 12930 |
The exponential of
is ![-u -u](shortminus.gif) . (Contributed by Paul
Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) |
|
Theorem | eulerid 12931 |
Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised
by Mario Carneiro, 9-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | sin2pi 12932 |
The sine of ![2 2](2.gif) is 0. (Contributed by
Paul Chapman,
23-Jan-2008.)
|
![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![0 0](0.gif) |
|
Theorem | cos2pi 12933 |
The cosine of ![2 2](2.gif) is 1. (Contributed by
Paul Chapman,
23-Jan-2008.)
|
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![1 1](1.gif) |
|
Theorem | ef2pi 12934 |
The exponential of ![2 2](2.gif) ![pi pi](pi.gif) is . (Contributed by Mario
Carneiro, 9-May-2014.)
|
![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![1 1](1.gif) |
|
Theorem | ef2kpi 12935 |
If is an integer,
then the exponential of ![2 2](2.gif) ![K K](_ck.gif) ![pi pi](pi.gif) is .
(Contributed by Mario Carneiro, 9-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | efper 12936 |
The exponential function is periodic. (Contributed by Paul Chapman,
21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinperlem 12937 |
Lemma for sinper 12938 and cosper 12939. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![O O](_co.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![O O](_co.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinper 12938 |
The sine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cosper 12939 |
The cosine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sin2kpi 12940 |
If is an integer,
then the sine of ![2 2](2.gif) ![K K](_ck.gif) is 0. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | cos2kpi 12941 |
If is an integer,
then the cosine of ![2 2](2.gif) ![K K](_ck.gif) is 1. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | sin2pim 12942 |
Sine of a number subtracted from . (Contributed by Paul
Chapman, 15-Mar-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![pi pi](pi.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cos2pim 12943 |
Cosine of a number subtracted from . (Contributed by Paul
Chapman, 15-Mar-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![pi pi](pi.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinmpi 12944 |
Sine of a number less . (Contributed by Paul Chapman,
15-Mar-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cosmpi 12945 |
Cosine of a number less . (Contributed by Paul Chapman,
15-Mar-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinppi 12946 |
Sine of a number plus . (Contributed by NM, 10-Aug-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif)
![pi pi](pi.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cosppi 12947 |
Cosine of a number plus . (Contributed by NM, 18-Aug-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif)
![pi pi](pi.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | efimpi 12948 |
The exponential function at times a real number less .
(Contributed by Paul Chapman, 15-Mar-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinhalfpip 12949 |
The sine of plus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinhalfpim 12950 |
The sine of minus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | coshalfpip 12951 |
The cosine of plus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | coshalfpim 12952 |
The cosine of minus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ptolemy 12953 |
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 11487, 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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![sin sin](_sin.gif) ![`
`](backtick.gif) ![C C](_cc.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sincosq1lem 12954 |
Lemma for sincosq1sgn 12955. (Contributed by Paul Chapman,
24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sincosq1sgn 12955 |
The signs of the sine and cosine functions in the first quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sincosq2sgn 12956 |
The signs of the sine and cosine functions in the second quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![(,) (,)](_ioo.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sincosq3sgn 12957 |
The signs of the sine and cosine functions in the third quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0
0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sincosq4sgn 12958 |
The signs of the sine and cosine functions in the fourth quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinq12gt0 12959 |
The sine of a number strictly between and is
positive.
(Contributed by Paul Chapman, 15-Mar-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![(,) (,)](_ioo.gif) ![pi pi](pi.gif)
![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinq34lt0t 12960 |
The sine of a number strictly between and is
negative. (Contributed by NM, 17-Aug-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | cosq14gt0 12961 |
The cosine of a number strictly between ![-u -u](shortminus.gif) and is
positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cosq23lt0 12962 |
The cosine of a number in the second and third quadrants is negative.
(Contributed by Jim Kingdon, 14-Mar-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | coseq0q4123 12963 |
Location of the zeroes of cosine in
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) . (Contributed by Jim
Kingdon, 14-Mar-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | coseq00topi 12964 |
Location of the zeroes of cosine in ![(
(](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif) . (Contributed by
David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | coseq0negpitopi 12965 |
Location of the zeroes of cosine in ![(
(](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) . (Contributed
by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | tanrpcl 12966 |
Positive real closure of the tangent function. (Contributed by Mario
Carneiro, 29-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![tan tan](_tan.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
|
Theorem | tangtx 12967 |
The tangent function is greater than its argument on positive reals in its
principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![tan tan](_tan.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sincosq1eq 12968 |
Complementarity of the sine and cosine functions in the first quadrant.
(Contributed by Paul Chapman, 25-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![1 1](1.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sincos4thpi 12969 |
The sine and cosine of . (Contributed by Paul
Chapman,
25-Jan-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sqr sqr](surd.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sqr sqr](surd.gif) ![` `](backtick.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | tan4thpi 12970 |
The tangent of . (Contributed by Mario Carneiro,
5-Apr-2015.)
|
![( (](lp.gif) ![tan tan](_tan.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) |
|
Theorem | sincos6thpi 12971 |
The sine and cosine of . (Contributed by Paul
Chapman,
25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![6 6](6.gif) ![) )](rp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![6
6](6.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sqr sqr](surd.gif) ![` `](backtick.gif) ![3 3](3.gif)
![2 2](2.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | sincos3rdpi 12972 |
The sine and cosine of . (Contributed by Mario
Carneiro,
21-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sqr sqr](surd.gif) ![` `](backtick.gif) ![3 3](3.gif) ![2 2](2.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pigt3 12973 |
is greater than 3.
(Contributed by Brendan Leahy,
21-Aug-2020.)
|
![pi pi](pi.gif) |
|
Theorem | pige3 12974 |
is greater than or
equal to 3. (Contributed by Mario Carneiro,
21-May-2016.)
|
![pi pi](pi.gif) |
|
Theorem | abssinper 12975 |
The absolute value of sine has period . (Contributed by NM,
17-Aug-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif)
![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sinkpi 12976 |
The sine of an integer multiple of is 0. (Contributed by NM,
11-Aug-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | coskpi 12977 |
The absolute value of the cosine of an integer multiple of is 1.
(Contributed by NM, 19-Aug-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | cosordlem 12978 |
Cosine is decreasing over the closed interval from to .
(Contributed by Mario Carneiro, 10-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![pi
pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | cosq34lt1 12979 |
Cosine is less than one in the third and fourth quadrants. (Contributed
by Jim Kingdon, 19-Mar-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![[,) [,)](_ico.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | cos02pilt1 12980 |
Cosine is less than one between zero and
. (Contributed by
Jim Kingdon, 19-Mar-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | cos0pilt1 12981 |
Cosine is between minus one and one on the open interval between zero and
. (Contributed
by Jim Kingdon, 7-May-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![(,) (,)](_ioo.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![(,) (,)](_ioo.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | cos11 12982 |
Cosine is one-to-one over the closed interval from to .
(Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Jim Kingdon,
6-May-2024.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![0
0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ioocosf1o 12983 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![pi
pi](pi.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![1 1](1.gif) ![(,) (,)](_ioo.gif) ![1 1](1.gif) ![)
)](rp.gif) |
|
Theorem | negpitopissre 12984 |
The interval ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) is a subset
of the reals.
(Contributed by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![RR RR](bbr.gif) |
|
9.1.3 The natural logarithm on complex
numbers
|
|
Syntax | clog 12985 |
Extend class notation with the natural logarithm function on complex
numbers.
|
![log log](_log.gif) |
|
Syntax | ccxp 12986 |
Extend class notation with the complex power function.
|
![^ ^](uparrow.gif) ![c c](subc.gif) |
|
Definition | df-relog 12987 |
Define the natural logarithm function. Defining the logarithm on complex
numbers is similar to square root - there are ways to define it but they
tend to make use of excluded middle. Therefore, we merely define
logarithms on positive reals. See
http://en.wikipedia.org/wiki/Natural_logarithm
and
https://en.wikipedia.org/wiki/Complex_logarithm.
(Contributed by Jim
Kingdon, 14-May-2024.)
|
![`' `'](_cnv.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Definition | df-rpcxp 12988* |
Define the power function on complex numbers. Because df-relog 12987 is
only defined on positive reals, this definition only allows for a base
which is a positive real. (Contributed by Jim Kingdon, 12-Jun-2024.)
|
![^
^](uparrow.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dfrelog 12989 |
The natural logarithm function on the positive reals in terms of the real
exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|
![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | relogf1o 12990 |
The natural logarithm function maps the positive reals one-to-one onto the
real numbers. (Contributed by Paul Chapman, 21-Apr-2008.)
|
![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) ![: :](colon.gif) ![RR+ RR+](_bbrplus.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![RR RR](bbr.gif) |
|
Theorem | relogcl 12991 |
Closure of the natural logarithm function on positive reals. (Contributed
by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | reeflog 12992 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | relogef 12993 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | relogeftb 12994 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![B B](_cb.gif)
![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | log1 12995 |
The natural logarithm of . One case of Property 1a of [Cohen]
p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | loge 12996 |
The natural logarithm of . One case of Property 1b of [Cohen]
p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![_e _e](rme.gif)
![1 1](1.gif) |
|
Theorem | relogoprlem 12997 |
Lemma for relogmul 12998 and relogdiv 12999. Remark of [Cohen] p. 301 ("The
proof of Property 3 is quite similar to the proof given for Property
2"). (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![B B](_cb.gif)
![CC CC](bbc.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![log log](_log.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![log log](_log.gif) ![`
`](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![log log](_log.gif) ![`
`](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | relogmul 12998 |
The natural logarithm of the product of two positive real numbers is the
sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to
natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | relogdiv 12999 |
The natural logarithm of the quotient of two positive real numbers is the
difference of natural logarithms. Exercise 72(a) and Property 3 of
[Cohen] p. 301, restricted to natural
logarithms. (Contributed by Steve
Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reexplog 13000 |
Exponentiation of a positive real number to an integer power.
(Contributed by Steve Rodriguez, 25-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![A A](_ca.gif) ![^ ^](uparrow.gif) ![N N](_cn.gif)
![( (](lp.gif) ![exp exp](_exp.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![log log](_log.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |