Type | Label | Description |
Statement |
|
Theorem | reefiso 14201 |
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.)
|
      |
|
Theorem | reapef 14202 |
Apartness and the exponential function for reals. (Contributed by Jim
Kingdon, 11-Jul-2024.)
|
    #     #        |
|
10.1.2 Properties of pi =
3.14159...
|
|
Theorem | pilem1 14203 |
Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro,
9-May-2014.)
|
              
   |
|
Theorem | cosz12 14204 |
Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and
Jim Kingdon, 7-Mar-2024.)
|
           |
|
Theorem | sin0pilem1 14205* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
          
              |
|
Theorem | sin0pilem2 14206* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
                       |
|
Theorem | pilem3 14207 |
Lemma for pi related theorems. (Contributed by Jim Kingdon,
9-Mar-2024.)
|
           |
|
Theorem | pigt2lt4 14208 |
is between 2 and 4.
(Contributed by Paul Chapman, 23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|

  |
|
Theorem | sinpi 14209 |
The sine of is 0.
(Contributed by Paul Chapman, 23-Jan-2008.)
|
   
 |
|
Theorem | pire 14210 |
is a real number.
(Contributed by Paul Chapman, 23-Jan-2008.)
|
 |
|
Theorem | picn 14211 |
is a complex number.
(Contributed by David A. Wheeler,
6-Dec-2018.)
|
 |
|
Theorem | pipos 14212 |
is positive.
(Contributed by Paul Chapman, 23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
 |
|
Theorem | pirp 14213 |
is a positive real.
(Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
 |
|
Theorem | negpicn 14214 |
 is a real number.
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
  |
|
Theorem | sinhalfpilem 14215 |
Lemma for sinhalfpi 14220 and coshalfpi 14221. (Contributed by Paul Chapman,
23-Jan-2008.)
|
               |
|
Theorem | halfpire 14216 |
is real. (Contributed by David Moews,
28-Feb-2017.)
|
   |
|
Theorem | neghalfpire 14217 |
 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
    |
|
Theorem | neghalfpirx 14218 |
 is an extended real. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
    |
|
Theorem | pidiv2halves 14219 |
Adding to itself gives . See 2halves 9148.
(Contributed by David A. Wheeler, 8-Dec-2018.)
|
       |
|
Theorem | sinhalfpi 14220 |
The sine of is 1. (Contributed by Paul Chapman,
23-Jan-2008.)
|
       |
|
Theorem | coshalfpi 14221 |
The cosine of is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
       |
|
Theorem | cosneghalfpi 14222 |
The cosine of  is zero. (Contributed by David Moews,
28-Feb-2017.)
|
        |
|
Theorem | efhalfpi 14223 |
The exponential of  is . (Contributed by Mario
Carneiro, 9-May-2014.)
|
         |
|
Theorem | cospi 14224 |
The cosine of is
 . (Contributed by Paul
Chapman,
23-Jan-2008.)
|
   
  |
|
Theorem | efipi 14225 |
The exponential of
is  . (Contributed by Paul
Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
        |
|
Theorem | eulerid 14226 |
Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised
by Mario Carneiro, 9-May-2014.)
|
         |
|
Theorem | sin2pi 14227 |
The sine of  is 0. (Contributed by
Paul Chapman,
23-Jan-2008.)
|
       |
|
Theorem | cos2pi 14228 |
The cosine of  is 1. (Contributed by
Paul Chapman,
23-Jan-2008.)
|
       |
|
Theorem | ef2pi 14229 |
The exponential of   is . (Contributed by Mario
Carneiro, 9-May-2014.)
|
         |
|
Theorem | ef2kpi 14230 |
If is an integer,
then the exponential of    is .
(Contributed by Mario Carneiro, 9-May-2014.)
|
             |
|
Theorem | efper 14231 |
The exponential function is periodic. (Contributed by Paul Chapman,
21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|
      
              |
|
Theorem | sinperlem 14232 |
Lemma for sinper 14233 and cosper 14234. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
    
                              
             
                              
            |
|
Theorem | sinper 14233 |
The sine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
      
            |
|
Theorem | cosper 14234 |
The cosine function is periodic. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
      
            |
|
Theorem | sin2kpi 14235 |
If is an integer,
then the sine of   is 0. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
           |
|
Theorem | cos2kpi 14236 |
If is an integer,
then the cosine of   is 1. (Contributed
by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro,
10-May-2014.)
|
           |
|
Theorem | sin2pim 14237 |
Sine of a number subtracted from . (Contributed by Paul
Chapman, 15-Mar-2008.)
|
                |
|
Theorem | cos2pim 14238 |
Cosine of a number subtracted from . (Contributed by Paul
Chapman, 15-Mar-2008.)
|
               |
|
Theorem | sinmpi 14239 |
Sine of a number less . (Contributed by Paul Chapman,
15-Mar-2008.)
|
              |
|
Theorem | cosmpi 14240 |
Cosine of a number less . (Contributed by Paul Chapman,
15-Mar-2008.)
|
              |
|
Theorem | sinppi 14241 |
Sine of a number plus . (Contributed by NM, 10-Aug-2008.)
|
    
         |
|
Theorem | cosppi 14242 |
Cosine of a number plus . (Contributed by NM, 18-Aug-2008.)
|
    
         |
|
Theorem | efimpi 14243 |
The exponential function at times a real number less .
(Contributed by Paul Chapman, 15-Mar-2008.)
|
                  |
|
Theorem | sinhalfpip 14244 |
The sine of plus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
               |
|
Theorem | sinhalfpim 14245 |
The sine of minus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
               |
|
Theorem | coshalfpip 14246 |
The cosine of plus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
                |
|
Theorem | coshalfpim 14247 |
The cosine of minus a number. (Contributed by Paul
Chapman,
24-Jan-2008.)
|
               |
|
Theorem | ptolemy 14248 |
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 11752, 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.)
|
    
   
              
               
           |
|
Theorem | sincosq1lem 14249 |
Lemma for sincosq1sgn 14250. (Contributed by Paul Chapman,
24-Jan-2008.)
|
    
      |
|
Theorem | sincosq1sgn 14250 |
The signs of the sine and cosine functions in the first quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
                   |
|
Theorem | sincosq2sgn 14251 |
The signs of the sine and cosine functions in the second quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
                   |
|
Theorem | sincosq3sgn 14252 |
The signs of the sine and cosine functions in the third quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
                     |
|
Theorem | sincosq4sgn 14253 |
The signs of the sine and cosine functions in the fourth quadrant.
(Contributed by Paul Chapman, 24-Jan-2008.)
|
                       |
|
Theorem | sinq12gt0 14254 |
The sine of a number strictly between and is
positive.
(Contributed by Paul Chapman, 15-Mar-2008.)
|
    
      |
|
Theorem | sinq34lt0t 14255 |
The sine of a number strictly between and is
negative. (Contributed by NM, 17-Aug-2008.)
|
             |
|
Theorem | cosq14gt0 14256 |
The cosine of a number strictly between  and is
positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
|
         
      |
|
Theorem | cosq23lt0 14257 |
The cosine of a number in the second and third quadrants is negative.
(Contributed by Jim Kingdon, 14-Mar-2024.)
|
                 |
|
Theorem | coseq0q4123 14258 |
Location of the zeroes of cosine in
  
        . (Contributed by Jim
Kingdon, 14-Mar-2024.)
|
                
     |
|
Theorem | coseq00topi 14259 |
Location of the zeroes of cosine in   ![[,] [,]](_icc.gif)  . (Contributed by
David Moews, 28-Feb-2017.)
|
   ![[,] [,]](_icc.gif)      
     |
|
Theorem | coseq0negpitopi 14260 |
Location of the zeroes of cosine in    ![(,] (,]](_ioc.gif)  . (Contributed
by David Moews, 28-Feb-2017.)
|
    ![(,] (,]](_ioc.gif)      
           |
|
Theorem | tanrpcl 14261 |
Positive real closure of the tangent function. (Contributed by Mario
Carneiro, 29-Jul-2014.)
|
             |
|
Theorem | tangtx 14262 |
The tangent function is greater than its argument on positive reals in its
principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)
|
             |
|
Theorem | sincosq1eq 14263 |
Complementarity of the sine and cosine functions in the first quadrant.
(Contributed by Paul Chapman, 25-Jan-2008.)
|
   
                   |
|
Theorem | sincos4thpi 14264 |
The sine and cosine of . (Contributed by Paul
Chapman,
25-Jan-2008.)
|
            
              |
|
Theorem | tan4thpi 14265 |
The tangent of . (Contributed by Mario Carneiro,
5-Apr-2015.)
|
       |
|
Theorem | sincos6thpi 14266 |
The sine and cosine of . (Contributed by Paul
Chapman,
25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.)
|
                   
   |
|
Theorem | sincos3rdpi 14267 |
The sine and cosine of . (Contributed by Mario
Carneiro,
21-May-2016.)
|
            
          |
|
Theorem | pigt3 14268 |
is greater than 3.
(Contributed by Brendan Leahy,
21-Aug-2020.)
|
 |
|
Theorem | pige3 14269 |
is greater than or
equal to 3. (Contributed by Mario Carneiro,
21-May-2016.)
|
 |
|
Theorem | abssinper 14270 |
The absolute value of sine has period . (Contributed by NM,
17-Aug-2008.)
|
          
              |
|
Theorem | sinkpi 14271 |
The sine of an integer multiple of is 0. (Contributed by NM,
11-Aug-2008.)
|
         |
|
Theorem | coskpi 14272 |
The absolute value of the cosine of an integer multiple of is 1.
(Contributed by NM, 19-Aug-2008.)
|
             |
|
Theorem | cosordlem 14273 |
Cosine is decreasing over the closed interval from to .
(Contributed by Mario Carneiro, 10-May-2014.)
|
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                |
|
Theorem | cosq34lt1 14274 |
Cosine is less than one in the third and fourth quadrants. (Contributed
by Jim Kingdon, 19-Mar-2024.)
|
             |
|
Theorem | cos02pilt1 14275 |
Cosine is less than one between zero and
. (Contributed by
Jim Kingdon, 19-Mar-2024.)
|
             |
|
Theorem | cos0pilt1 14276 |
Cosine is between minus one and one on the open interval between zero and
. (Contributed
by Jim Kingdon, 7-May-2024.)
|
                |
|
Theorem | cos11 14277 |
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.)
|
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)               |
|
Theorem | ioocosf1o 14278 |
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.)
|
                    |
|
Theorem | negpitopissre 14279 |
The interval    ![(,] (,]](_ioc.gif)  is a subset
of the reals.
(Contributed by David Moews, 28-Feb-2017.)
|
   ![(,] (,]](_ioc.gif)   |
|
10.1.3 The natural logarithm on complex
numbers
|
|
Syntax | clog 14280 |
Extend class notation with the natural logarithm function on complex
numbers.
|
 |
|
Syntax | ccxp 14281 |
Extend class notation with the complex power function.
|
  |
|
Definition | df-relog 14282 |
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.)
|
    |
|
Definition | df-rpcxp 14283* |
Define the power function on complex numbers. Because df-relog 14282 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.)
|
               |
|
Theorem | dfrelog 14284 |
The natural logarithm function on the positive reals in terms of the real
exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|
      |
|
Theorem | relogf1o 14285 |
The natural logarithm function maps the positive reals one-to-one onto the
real numbers. (Contributed by Paul Chapman, 21-Apr-2008.)
|
       |
|
Theorem | relogcl 14286 |
Closure of the natural logarithm function on positive reals. (Contributed
by Steve Rodriguez, 25-Nov-2007.)
|
       |
|
Theorem | reeflog 14287 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
           |
|
Theorem | relogef 14288 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
           |
|
Theorem | relogeftb 14289 |
Relationship between the natural logarithm function and the exponential
function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
       
   
   |
|
Theorem | log1 14290 |
The natural logarithm of . One case of Property 1a of [Cohen]
p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
     |
|
Theorem | loge 14291 |
The natural logarithm of . One case of Property 1b of [Cohen]
p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
   
 |
|
Theorem | relogoprlem 14292 |
Lemma for relogmul 14293 and relogdiv 14294. 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.)
|
         
                                                                                       |
|
Theorem | relogmul 14293 |
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.)
|
                     |
|
Theorem | relogdiv 14294 |
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.)
|
                     |
|
Theorem | reexplog 14295 |
Exponentiation of a positive real number to an integer power.
(Contributed by Steve Rodriguez, 25-Nov-2007.)
|
      
            |
|
Theorem | relogexp 14296 |
The natural logarithm of positive raised to an integer power.
Property 4 of [Cohen] p. 301-302, restricted
to natural logarithms and
integer powers .
(Contributed by Steve Rodriguez, 25-Nov-2007.)
|
                   |
|
Theorem | relogiso 14297 |
The natural logarithm function on positive reals determines an isomorphism
from the positive reals onto the reals. (Contributed by Steve Rodriguez,
25-Nov-2007.)
|
      |
|
Theorem | logltb 14298 |
The natural logarithm function on positive reals is strictly monotonic.
(Contributed by Steve Rodriguez, 25-Nov-2007.)
|
               |
|
Theorem | logleb 14299 |
Natural logarithm preserves . (Contributed by Stefan O'Rear,
19-Sep-2014.)
|
               |
|
Theorem | logrpap0b 14300 |
The logarithm is apart from 0 if and only if its argument is apart from 1.
(Contributed by Jim Kingdon, 3-Jul-2024.)
|
  #
    #    |