HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-9063) |
Hilbert Space Explorer
(9064-10651) |
Users' Mathboxes
(10652-12230) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | efifolem7 9001 | Lemma for efifo 9002. |
| Theorem | efifo 9002 |
The exponential function of an imaginary number maps the closed-below,
open-above interval from  to    onto the unit circle.
(Contributed by Paul Chapman, 16-Mar-2008.)
|
      
     [,)         
     [,)  | ||
| Theorem | efif1lem1 9003 | Lemma for efif1 9010. |
| Theorem | efif1lem2 9004 | Lemma for efif1 9010. |
| Theorem | efif1lem3 9005 | Lemma for efif1 9010. |
| Theorem | efif1lem4 9006 | Lemma for efif1 9010. |
| Theorem | efif1lem5 9007 | Lemma for efif1 9010. |
| Theorem | efif1lem6 9008 | Lemma for efif1 9010. |
| Theorem | efif1lem7 9009 | Lemma for efif1 9010. |
| Theorem | efif1 9010 |
The exponential function of an imaginary number maps the closed-below,
open-above interval from to one-to-one to the unit
circle. (Contributed by Paul Chapman, 16-Mar-2008.)
|
[,)
[,)  | ||
| Theorem | efif1o 9011 |
The exponential function of an imaginary number maps the closed-below,
open-above interval from to one-to-one onto the unit
circle. (Contributed by Paul Chapman, 16-Mar-2008.)
|
[,)
[,)  | ||
| Theorem | efielcirc 9012 |
Membership of the exponential function of times a real number in
the unit circle. (Contributed by Paul Chapman, 25-Mar-2008.)
|
 
   | ||
| Theorem | circgrp 9013 |
The circle group  is an
Abelian group. (Contributed by Paul
Chapman, 25-Mar-2008.)
|
 Abel | ||
| Theorem | shftefif1olem 9014 | Lemma for shftefif1o 9015. |
| Theorem | shftefif1o 9015 |
The exponential function of times a real number maps any
closed-below, open-above real interval of length
one-to-one
onto the unit circle. (Contributed by Paul Chapman, 25-Mar-2008.)
|
 [,)   | ||
| Theorem | eff1lem 9016 | Lemma for eff1i 9017. |
| Theorem | eff1i 9017 |
The exponential function maps the set , of complex numbers with
imaginary part in a closed-below, open-above real interval of length
starting at , one-to-one to the nonzero complex
numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|
[,)
 | ||
| Theorem | effoi 9018 |
The exponential function maps the set , of complex numbers with
imaginary part in a closed-below, open-above real interval of length
starting at , onto the nonzero complex numbers.
(Contributed by Paul Chapman, 16-Apr-2008.)
|
| [,)
| ||
| Theorem | eff1oi 9019 |
The exponential function maps the set , of complex numbers with
imaginary part in a closed-below, open-above real interval of length
starting at , one-to-one onto the nonzero complex
numbers. would
normally be fixed at or
 ,
according to choice of principal domain for the exponential function.
(Contributed by Paul Chapman, 16-Apr-2008.)
|
| [,)
| ||
| Theorem | efper 9020 | The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) |
  | ||
| Theorem | eff1o 9021 | The exponential function restricted to its principal domain maps one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 21-Apr-2008.) |
|
[,)
[,) | ||
| The natural logarithm on complex numbers | ||
| Syntax | clog 9022 | Extend class notation with the natural logarithm function on complex numbers. |
  | ||
| Definition | df-log 9023 | Define the natural logarithm function on complex numbers. See http://en.wikipedia.org/wiki/Natural_logarithm ("The natural logarithm function can also be defined as the inverse function of the exponential function"). |
[,) | ||
| Theorem | logrn 9024 |
The range of the natural logarithm function, also the principal domain of
the exponential function. This allows us to write the longer class
abstraction as simply  .
(Contributed by Paul Chapman,
21-Apr-2008.)
|
|
[,) | ||
| Theorem | dflog2 9025 | The natural logarithm function in terms of the exponential function restricted to its principal domain. (Contributed by Paul Chapman, 21-Apr-2008.) |
|
| ||
| Theorem | resslogrn 9026 | The range of the natural logarithm function includes the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.) |
 | ||
| Theorem | eff1o2 9027 | The exponential function restricted to its principal domain maps one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 21-Apr-2008.) |
| | ||
| Theorem | logf1o 9028 | The natural logarithm function maps the nonzero complex numbers one-to-one onto its range. (Contributed by Paul Chapman, 21-Apr-2008.) |
| | ||
| Theorem | dfrelog 9029 | The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
 | ||
| Theorem | relogf1o 9030 | The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.) |
| | ||
| Theorem | logcl 9031 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
 | ||
| Theorem | relogcl 9032 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
|
| ||
| Theorem | eflog 9033 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
| | ||
| Theorem | reeflog 9034 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| | ||
| Theorem | logef 9035 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
| | ||
| Theorem | relogef 9036 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| | ||
| Theorem | logeftb 9037 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
 
| ||
| Theorem | relogeftb 9038 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
|
| ||
| Theorem | log1 9039 |
The natural logarithm of .
One case of Property 1a of [Cohen] p.
301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
|
| ||
| Theorem | loge 9040 |
The natural logarithm of  .
One case of Property 1b of [Cohen]
p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|
|
| ||
| Theorem | pilog 9041 |
Relationship between
and the natural logarithm function.
(Contributed by Paul Chapman, 21-Apr-2008.)
|
| | ||
| Theorem | relogoprlem 9042 | Lemma for relogmul 9043 and relogdiv 9044. Remark of [Cohen] p. 301 ("The proof of Property 3 is quite similar to the proof given for Property 2"). |
| Theorem | relogmul 9043 | 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 9044 | 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 | explog 9045 | Exponentiation of a nonzero complex number to a nonnegative integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
 
| ||
| Theorem | reexplog 9046 | Exponentiation of a positive real number to a nonnegative integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
|
| ||
| Theorem | relogexp 9047 |
The natural logarithm of positive raised to an nonnegative integer
power. Property 4 of [Cohen] p. 301-302,
restricted to natural logarithms
and nonnegative-integer powers . (Contributed by Steve Rodriguez,
25-Nov-2007.)
|
|
| ||
| Theorem | relogiso 9048 | 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 9049 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
|
| ||
| ZFC Set Theory plus the Tarksi-Grothendieck Axiom | ||
| Introduce the Tarksi-Grothendieck Axiom | ||
| Axiom | ax-groth 9050 |
The Tarksi-Grothendieck Axiom. For every set there is an
inaccessible cardinal such that is
not in . The
addition of this axiom to ZFC set theory provides a framework for
category theory, thus for all practical purposes giving us a complete
foundation for "all of mathematics." This version of the
axiom is used
by the Mizar project (http://www.mizar.org/JFM/Axiomatics/tarski.html
). Unlike the ZFC axioms, this axiom is very long when expressed in
terms of primitive symbols - see grothprim 9058. An open problem is
finding a shorter equivalent.
|
 
 | ||
| Theorem | axgroth2 9051 | Alternate version of the Tarksi-Grothendieck Axiom. |
 | ||
| Theorem | axgroth3 9052 | Alternate version of the Tarksi-Grothendieck Axiom. ax-ac 4891 is used to derive this version. |
|
| ||
| Theorem | axgroth4 9053 | Alternate version of the Tarksi-Grothendieck Axiom. ax-ac 4891 is used to derive this version. |
| ||
| Theorem | grothinf 9054 | The Tarksi-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 4773). Note that our proof does not depend on the Axiom of Infinity. |
  | ||
| Theorem | grothpw 9055 | Derive the Axiom of Power Sets ax-pow 2819 from the Tarksi-Grothendieck axiom ax-groth 9050. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 2819 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) |
| | ||
| Theorem | axgroth5 9056 | The Tarski-Grothendieck axiom using abbreviations. |
| ||
| Theorem | grothprimlem 9057 | Lemma for grothprim 9058. Expand the membership of an unordered pair into primitives. |
| Theorem | grothprim 9058 | The Tarksi-Grothendieck Axiom ax-groth 9050 expanded into set theory primitives using 163 symbols. An open problem is whether a shorter equivalent exists (when expanded to primitives). |
   
| ||
| Humor | ||
| April Fool's theorem | ||
| Theorem | avril1 9059 |
Poisson d'Avril's Theorem. This theorem is noted for its
Selbstdokumentieren property, which means, literally,
"self-documenting" and recalls the principle of quidquid
germanus
dictum sit, altum viditur, often used in set theory. Starting with
the
seemingly simple yet profound fact that any object equals itself
(proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we
demonstrate that the power set of the real numbers, as a relation on the
value of the imaginary unit, does not conjoin with an empty relation on
the product of the additive and multiplicative identity elements,
leading to this startling conclusion that has left even seasoned
professional mathematicians scratching their heads. (Contributed by
Prof. Loof Lirpa, 1-Apr-2005.)
A reply to skeptics can be found at http://us.metamath.org/mpegif/mmnotes.txt, under the 1-Apr-2006 entry. |
  | ||
| Theorem | 2bornot2b 9060 | The law of excluded middle. Act III, Theorem 1 of Shakespeare, Hamlet, Prince of Denmark (1602). Its author leaves its proof as an exercise for the reader - "To be, or not to be: that is the question" - starting a trend that has become standard in modern-day textbooks, serving to make the frustrated reader feel inferior, or in some cases to mask the fact that the author does not know its solution. (Contributed by Prof. Loof Lirpa, 1-Apr-2006.) |
|
| ||
| Theorem | helloworld 9061 | The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://www.roesler-ac.de/wolfram/hello.htm. However, for many years it eluded a proof that it is more than just a conjecture, even though a wily mathematician once claimed, "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." Using an IBM 709 mainframe, a team of mathematicians led by Prof. Loof Lirpa, at the New College of Tahiti, were finally able put it rest with a remarkably short proof only 4 lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007.) |
    | ||
| Theorem | 1p1e2 9062 | One plus one equals two. Using proof-shortening techniques pioneered by Mr. Mel O'Cat, along with the latest supercomputer technology, Prof. Loof Lirpa and colleagues were able to shorten Whitehead and Russell's 360-page proof that 1+1=2 in Principia Mathematica to this remarkable proof only two steps long, thus establishing a new world's record for this famous theorem. (Contributed by Prof. Loof Lirpa, 1-Apr-2008.) |
| | ||
| Theorem | eqid1 9063 |
Law of identity (reflexivity of class equality). Theorem 6.4 of
[Quine] p. 41.
This law is thought to have originated with Aristotle (Metaphysics, Book VII, Part 17). It is one of the three axioms of Ayn Rand's philosophy (Atlas Shrugged, Part Three, Chapter VII). While some have proposed extending Rand's axiomatization to include Compassion and Kindness, others fear that such an extension may flirt with logical inconsistency. (Thanks to Stefan Allan and Prof. Loof Lirpa for this information.) |
| | ||
| Hilbert Space Explorer | ||
| Syntax | chil 9064 | Extend class notation with Hilbert vector space. |
 | ||
| Syntax | cva 9065 |
Extend class notation with vector addition in Hilbert space. In
the literature, the subscript "v" is omitted, but we need it to
avoid ambiguity with complex number addition caddc 5392.
|
 | ||
| Syntax | csm 9066 | Extend class notation with scalar multiplication in Hilbert space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity. |
 | ||
| Syntax | c0v 9067 | Extend class notation with zero vector in Hilbert space. |
 | ||
| Syntax | cmv 9068 | Extend class notation with vector subtraction in Hilbert space. |
 | ||
| Syntax | csp 9069 |
Extend class notation with inner (scalar) product in Hilbert space.
In the literature, the inner product of and is usually
written but
our operation notation allows us to use
existing theorems about operations and also eliminates ambiguity with
the definition of an ordered pair df-op 2475.
|
 | ||
| Syntax | cno 9070 |
Extend class notation with the norm function in Hilbert space.
In the literature, the norm of is usually written "|| ||",
but we use function notation to take advantage of our existing theorems
about functions.
|
 | ||
| Syntax | ccau 9071 | Extend class notation with set of Cauchy sequences in Hilbert space. |
 | ||
| Syntax | chli 9072 | Extend class notation with convergence relation in Hilbert space. |
 | ||
| Syntax | csh 9073 | Extend class notation with set of subspaces of a Hilbert space. |
 | ||
| Syntax | cch 9074 | Extend class notation with set of closed subspaces of a Hilbert space. |
 | ||
| Syntax | cort 9075 |
Extend class notation with orthogonal complement in .
|
 | ||
| Syntax | cph 9076 |
Extend class notation with subspace sum in .
|
 | ||
| Syntax | cspn 9077 |
Extend class notation with subspace span in .
|
 | ||
| Syntax | chj 9078 |
Extend class notation with join in .
|
 | ||
| Syntax | chsup 9079 |
Extend class notation with supremum of a collection in .
|
 | ||
| Syntax | c0h 9080 |
Extend class notation with zero of .
|
 | ||
| Syntax | ccm 9081 | Extend class notation with the commutes relation on a Hilbert lattice. |
 | ||
| Syntax | cpj 9082 | Extend class notation with set of projections on a Hilbert space. |
| proj | ||
| Syntax | chos 9083 | Extend class notation with sum of Hilbert space operators. |
 | ||
| Syntax | chot 9084 | Extend class notation with scalar product of a Hilbert space operator. |
 | ||
| Syntax | chod 9085 | Extend class notation with difference of Hilbert space operators. |
 | ||
| Syntax | chfs 9086 | Extend class notation with sum of Hilbert space functionals. |
 | ||
| Syntax | chft 9087 | Extend class notation with scalar product of Hilbert space functional. |
 | ||
| Syntax | ch0o 9088 | Extend class notation with the Hilbert space zero operator. |
|
0hop | ||
| Syntax | chio 9089 | Extend class notation with Hilbert space identity operator. |
 | ||
| Syntax | cnop 9090 | Extend class notation with the operator norm function. |
|
normop | ||
| Syntax | cco 9091 | Extend class notation with set of continuous Hilbert space operators. |
| ConOp | ||
| Syntax | clo 9092 | Extend class notation with set of linear Hilbert space operators. |
| LinOp | ||
| Syntax | cbo 9093 | Extend class notation with set of bounded linear operators. |
| BndLinOp | ||
| Syntax | cuo 9094 | Extend class notation with set of unitary Hilbert space operators. |
| UniOp | ||
| Syntax | cho 9095 | Extend class notation with set of Hermitian Hilbert space operators. |
| HrmOp | ||
| Syntax | cnmf 9096 | Extend class notation with the functional norm function. |
|
normfn | ||
| Syntax | cnl 9097 | Extend class notation with the functional nullspace function. |
| null | ||
| Syntax | ccnf 9098 | Extend class notation with set of continuous Hilbert space functionals. |
| ConFn | ||
| Syntax | clf 9099 | Extend class notation with set of linear Hilbert space functionals. |
| LinFn | ||
| Syntax | cado 9100 | Extend class notation with Hilbert space adjoint function. |
|
adjh | ||
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |