avewright/proofwiki-math huggingface dataset:
Theorem: Arithmetic iff Compact Subset form Lattice in Algebraic Lattice

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.
Then:
:$L$ is arithmetic
{{iff}}:
:$\struct {\map K L, \precsim}$ is a lattice
where $\map K L$ denotes the compact subset of $L$:
:$\mathord \precsim = \mathord \preceq \cap \paren {\map K L \times \map K L}$

Proof:
=== Sufficient Condition ===
Define $K = \struct {\map K L, \precsim}$.
Let $x, y \in \map K L$.
By Compact Subset is Join Subsemilattice:
:$x \vee_L y \in \map K L$
We will prove that
:$x \vee_L y$ is upper bound for $\set {x, y}$ in $K$
Let $z \in \set {x, y}$.
By Join Succeeds Operands:
:$z \preceq x \vee_L y$
By definition of $\precsim$:
:$z \precsim v \vee_L y$
{{qed|lemma}}
We will prove that
:$\forall z \in \map K L: z$ is upper bound for $\set {x, y}$ in $K \implies x \vee_L y \precsim z$
Let $z \in \map K L$ such that
:$z$ is upper bound for $\set {x, y}$ in $K$.
Then by definition of $\precsim$:
:$z$ is upper bound for $\set {x, y}$ in $L$.
By definition of supremum:
:$x \vee_L y \preceq z$
By definition of $\precsim$:
:$x \vee_L y \precsim z$
{{qed|lemma}}
Thus by definition of supremum:
:$\set {x, y}$ admits a supremum in $K$.
Thus analogically:
:$\set {x, y}$ admits an infimum in $K$.
Hence $K$ is lattice.
{{qed|lemma}}
Theorem: Four Kepler-Poinsot Polyhedra

There exist exactly four Kepler-Poinsot polyhedra:
{{begin-itemize}}
{{item|(1):|the small stellated dodecahedron}}
{{item|(2):|the great stellated dodecahedron}}
{{item|(3):|the great dodecahedron}}
{{item|(4):|the great icosahedron.}}
{{end-itemize}}

Proof:
{{ProofWanted|needs considerable vision}}
Theorem: Feuerbach's Theorem

Let $\triangle ABC$ be a triangle.
The Feuerbach circle of $\triangle ABC$ is tangent to:
:the incircle of $\triangle ABC$
and:
:the $3$ excircles of $\triangle ABC$.
:800px

Proof:
Recall the Third Fontené Theorem:
:the pedal circle of a point $P$ is tangent to the nine point circle
{{iff}}:
:$P$ and its isogonal conjugate $P^{-1}$ lie on a line through the circumcenter.
Let $P$ be either the incenter or an excenter of $\triangle ABC$.
By Isogonal Conjugate of Incenter or Excenter is Itself, we have $P = P^{-1}$.
As $P$ and $P^{-1}$ are the same point, they both trivially lie on a straight line through the circumcenter of $\triangle ABC$.
Hence by the Third Fontené Theorem the pedal circle of $P$ is tangent to the nine point circle.
Then from: 
:Pedal Circle of Incenter is Incircle
:Pedal Circle of Excenter is Excircle
the result follows. 
{{qed}}
Theorem: Round Peg fits in Square Hole better than Square Peg fits in Round Hole

A round peg fits better in a square hole than a square peg fits in a round hole.
:600px

Proof:
The situation is modelled by considering the ratios of the areas of:
:a square to the circle in which it is inscribed
:a square to the circle around which it has been circumscribed.
Let a square $S$ be inscribed in a circle $C$ of radius $r$.
Let $A_c$ and $A_s$ be the areas of $C$ and $S$ respectively.
From Area of Circle:
:$A_c = \pi r^2$
The diameter of $S$ is $2 r$.
Thus from Pythagoras's Theorem its side is of length $r \sqrt 2$.
From Area of Square:
:$A_s = 2 r^2$
Thus:
:$\dfrac {A_s} {A_c} = \dfrac {2 r^2} {\pi r^2} = \dfrac 2 \pi \approx 0.6366 \ldots$
{{qed|lemma}}
Let a square $S$ be circumscribed around a circle $C$ of radius $r$.
Let $A_c$ and $A_s$ be the areas of $C$ and $S$ respectively.
From Area of Circle:
:$A_c = \pi r^2$
The side of $S$ is of length $2 r$.
From Area of Square:
:$A_s = 4 r^2$
Thus:
:$\dfrac {A_c} {A_s} = \dfrac {\pi r^2} {4 r^2} = \dfrac \pi 4 \approx 0.7853 \ldots$
{{qed|lemma}}
Thus a round peg takes up more space ($0.7853 \ldots$) of a square hole than a square peg takes up ($0.6366 \ldots$) of a round hole.
{{qed}}
Theorem: Ratios of Sizes of Mutually Inscribed Multidimensional Cubes and Spheres

Consider:
: a cube $C_n$ of $n$ dimensions inscribed within a sphere $S_n$ of $n$ dimensions
: a sphere $S'_n$ of $n$ dimensions  inscribed within a cube $C'_n$ of $n$ dimensions.
Let:
: $A_{cn}$ be the $n$ dimensional volume of $C_n$
: $A_{sn}$ be the $n$ dimensional volume of $S_n$
: $A'_{cn}$ be the $n$ dimensional volume of $C'_n$
: $A'_{sn}$ be the $n$ dimensional volume of $S'_n$.
For $n < 9$:
:$\dfrac {S_n} {C_n} > \dfrac {C'_n} {S'_n}$
but for $n \ge 9$:
:$\dfrac {S_n} {C_n} < \dfrac {C'_n} {S'_n}$
That is, for dimension $n$ less than $9$, the $n$ dimensional round peg fits better into an $n$ dimensional square hole than an $n$ dimensional square peg fits into an $n$ dimensional round hole, but for $9$ and higher dimensions, the situation is reversed.

Proof:
{{ProofWanted|Formulae for the volumes of $n$ dimensional squares and circles need to be established first.}}
Theorem: Pseudoprime Element is Prime in Arithmetic Lattice

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below arithmetic lattice.
Let $p \in S$.
Then if $p$ is pseudoprime element, then $p$ is prime element.

Proof:
By Arithmetic iff Way Below Relation is Multiplicative in Algebraic Lattice:
:$\ll$ is a multiplicative relation.
Thus by Way Below Relation is Multiplicative implies Pseudoprime Element is Prime:
:the result holds.
{{qed}}
Theorem: Every Pseudoprime Element is Prime implies Lattice is Arithmetic

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below algebraic distributive lattice.
Assume that
:for every element $p$ of $S$ if $p$ is pseudoprime element, then $p$ is prime element.
Then $L$ is arithmetic.

Proof:
By If Every Element Pseudoprime is Prime then Way Below Relation is Multiplicative:
:$\ll$ is a multiplicative relation.
where $\ll$ denotes the way below relation.
Thus by Arithmetic iff Way Below Relation is Multiplicative in Algebraic Lattice:
:the result holds.
{{qed}}
Theorem: General Periodicity Property/Corollary

Let $f: \R \to \R$ be a real function.
Then $L$ is a periodic element of $f$ {{iff}}:
:$\forall x \in \R: \map f {x \bmod L} = \map f x$
where $x \bmod L$ is the modulo operation.

Proof:
=== Necessary Condition ===
Let $f: \R \to \R$ be a real function with a periodic element $L$.
Then:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f {n L + r} \quad 0 < r < \size L
      | c = {{Defof|Quotient (Integer Division)/Real|Quotient}}
}}
{{eqn | r = \map f r
      | c = General Periodicity Property
}}
{{eqn | r = \map f {x \bmod L}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Characterization of Euler's Number by Inequality

Let $a$ be a (strictly) positive real number.
Then:
:$a = e \iff \forall x \in \R: a^x \ge x + 1$
where $e$ denotes Euler's number.

Proof:
=== Forward Implication ===
Proved in Exponential Function Inequality.
{{qed|lemma}}
Theorem: 3 Configurations of 9 Lines with 3 Intersection Points on each Line

There exist exactly $3$ essentially different configurations of $9$ straight lines each of which has exactly $3$ points of intersection.
This is one: there are two others.
:400px

Proof:
{{ProofWanted|The precise meaning of the term "essentially different" needs to be established, for a start}}
Theorem: Power of Positive Real Number is Positive/Real Number

Let $x \in \R_{>0}$ be a (strictly) positive real number.
Let $r \in \R$ be a real number.
Then:
:$x^r > 0$
where $x^r$ denotes the $x$ to the power of $r$.

Proof:
From the definition of $x$ to the power of $r$:
:$x^r = \map \exp {r \ln x}$
The result follows from Exponential of Real Number is Strictly Positive.
{{qed}}
Category:Power of Positive Real Number is Positive
h0m8t9tu4wm2hmo6bal3kzgkd208761
Theorem: Element is Finite iff Element is Compact in Lattice of Power Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be a lattice of power set.
Let $x \in \powerset X$.
Then $x$ is a finite set {{iff}} $x$ is a compact element.

Proof:
=== Sufficient Condition when Empty ===
The case when $x = \O$
By Empty Set is Bottom of Lattice of Power Set:
:$x = \bot$
where $\bot$ denotes the bottom of $L$.
By Bottom is Way Below Any Element:
:$x \ll x$
where $\ll$ denotes the way below relation.
Thus by definition
:$x$ is a finite set {{iff}} $x$ is a compact element.
{{qed|lemma}}
Theorem: Function with Limit at Infinity of Exponential Order Zero

Let $f: \hointr 0 \to \to \R$ be a real function.
Let $f$ be continuous everywhere on their domains, except possibly for some finite number of discontinuities of the first kind in every finite subinterval of $\hointr 0 \to$.
{{explain|Establish whether it is "finite subinterval" that is needed here, or what we have already defined as "Definition:Finite Subdivision". Also get the correct instance of "continuous".}}
Let $f$ have a (finite) limit at infinity.
Then $f$ is of exponential order $0$.

Proof:
Denote $\ds L = \lim_{t \mathop \to +\infty} \map f t$.
Define the constant mapping:
:$\map C t = - L$
Further define:
:$\map g t = \map f t + \map C t$
From:
:Constant Function is of Exponential Order Zero,
:Sum of Functions of Exponential Order,
it is sufficient to prove that $g$ is of exponential order $0$.
Fix $\epsilon > 0$ arbitrarily small.
By definition of limit at infinity, there exists $c \in \R$ such that:
:$\forall t > c: \size {\map f t - L} < \epsilon$
Therefore:
{{begin-eqn}}
{{eqn | q = \forall t \ge c + 1
      | l = \size {\map g t}
      | r = \size {\map f t + \map C t}
}}
{{eqn | r = \size {\map f t - L}
}}
{{eqn | o = <
      | r = \epsilon
}}
{{eqn | r = \epsilon \cdot e^0
      | c = Exponential of Zero
}}
{{end-eqn}}
The result follows from the definition of exponential order, with $M = c + 1$, $K = \epsilon$, and $a = 0$.
{{qed}}
Category:Exponential Order
as7he8bhikq7f7c2gqav5k162ywjvjf
Theorem: Bounded Function is of Exponential Order Zero

Let $f: \hointr 0 \to \to \mathbb F$ be a function, where $\mathbb F \in \set {\R, \C}$.
Let $f$ be continuous everywhere on its domain, except possibly for some finite number of discontinuities of the first kind in every finite subinterval of $\hointr 0 \to$.
{{explain|Establish whether it is "finite subinterval" that is needed here, or what we have already defined as "Definition:Finite Subdivision".}}
{{explain|Pin down a specific page on which the relevant definition of "Continuous" can be found for this context.}}
Let $f$ be bounded.
Then $f$ is of exponential order $0$.

Proof:
Let $U$ be an upper bound of $f$.
Let $L$ be a lower bound of $f$.
Let $K > \max \set {\size U, \size L}$.
Then: 
{{begin-eqn}}
{{eqn | q = \forall t \ge 1
      | l = \size {\map f t}
      | o = <
      | r = K
      | c = {{Defof|Bounded Mapping}}
}}
{{eqn | r = K e^{0 t}
      | c = Exponential of Zero
}}
{{end-eqn}}
The result follows from the definition of exponential order with $M = 1$, $K = K$, and $a = 0$.
{{qed}}
Theorem: Arctangent is of Exponential Order Zero

Let $\arctan: \R \to \openint {-\dfrac \pi 2} {\dfrac \pi 2}$ be the real arctangent.
Then $\arctan$ is of exponential order $0$.

Proof:
Follows from Function with Limit at Infinity of Exponential Order Zero.
{{qed}}
Category:Arctangent Function
Category:Exponential Order
Category:Limits of Real Functions
fn6s7w3ymg5h2cf712ycea4qix5bgia
Theorem: Arccotangent is of Exponential Order Zero

Let $\arccot: \R \to \openint 0 \pi$ be the real arccotangent.
Then $\arccot$ is of exponential order $0$.

Proof:
Follows from Function with Limit at Infinity of Exponential Order Zero.
{{qed}}
{{MissingLinks|limit of $\arccot$}}
Category:Exponential Order
ri29ldq9urkxmn6a26kq9sxapo9m553
Theorem: Limit at Infinity of Sine Integral Function

Let $\Si: \R \to \R$ denote the sine integral function.
Then $\Si$ has a (finite) limit at infinity:
:$\ds \lim_{x \mathop \to +\infty} \map \Si x = \frac \pi 2$

Proof:
The limit:
:$\ds \lim_{x \mathop \to +\infty} \map \Si x = \lim_{x \mathop \to +\infty} \int_{t \mathop \to 0}^{t \mathop = x} \frac {\sin t} t \rd t$
is the Dirichlet Integral.
{{qed}}
Theorem: Natural Number Power is of Exponential Order Epsilon

Let $n \in \N$ be a natural number.
Then: 
:$t \mapsto t^n$
is of exponential order $\epsilon$ for any $\epsilon > 0$ arbitrarily small in magnitude.

Proof:
The proof proceeds by induction on $n$, where $n$ is the degree of the polynomial.
Theorem: Raising Exponential Order

Let $\map f t: \R \to \mathbb F$ a function, where $\mathbb F \in \set {\R, \C}$.
Let $f$ be continuous on the real interval $\hointr 0 \to$, except possibly for some finite number of discontinuities of the first kind in every finite subinterval of $\hointr 0 \to$.
{{explain|Establish whether it is "finite subinterval" that is needed here, or what we have already defined as "Definition:Finite Subdivision".}}
{{explain|Pin down a specific page on which the relevant definition of "Continuous" can be found for this context.}}
Let $f$ be of exponential order $a$.
Let $b > a$.
Then $f$ is of exponential order $b$.

Proof:
From the definition of exponential order, there exist strictly positive real numbers $M$ and $K$ such that:
:$\forall t \ge M: \size {\map f t} < K e^{a t}$
From Exponential is Strictly Increasing, we have:
:$K e^{a t} < K e^{b t}$
Therefore:
:$\forall t \ge M: \size {\map f t} < K e^{b t}$
The result follows from the definition of exponential order.
{{qed}}
Category:Exponential Order
a3cg99grb6mk3m8fwjljixt9ee4q53j
Theorem: Factorial is not of Exponential Order

Let $\Gamma$ denote the gamma function.
Let $\map f t = \map \Gamma {t + 1} = t!$.
Then:
:$f$ is not of exponential order.
That is, it grows faster than any exponential.

Proof:
From Gamma Function is Continuous on Positive Reals, $f$ is continuous for $t \ge 0$.
Set $t > 0$.
From Stirling's Formula:
:$t! \sim \sqrt {2 \pi t} \paren {\dfrac t e}^t$
where $\sim$ denotes asymptotic equality.
That is, 
{{begin-eqn}}
{{eqn | l = t!
      | o = \sim
      | r = \sqrt {2 \pi t} \paren {\frac t e}^t
}}
{{eqn | o = >
      | r = t^t \, e^{-t}
}}
{{end-eqn}}
{{AimForCont}} $t^t \, e^{-t}$ is of exponential order $a$. 
Then, for $t$ sufficiently large, there exists a $K > 0$ such that:
{{begin-eqn}}
{{eqn | l =  t^t \, e^{-t}
      | o = < 
      | r = K e^{a t}
}}
{{eqn | ll= \leadsto
      | l = t^t
      | o = <
      | r = K e^{\paren {a + 1} t}
}}
{{end-eqn}}
This implies that $t^t$ is of exponential order, which is false.
From this contradiction it follows that $t!$ is also not of exponential order.
{{qed}}
Category:Gamma Function
Category:Exponential Order
6oo7etdhp9wwb2wpshpoqe5wjg8ox9g
Theorem: X to the x is not of Exponential Order

Let $f: \R_{>0} \to \R$ be definedas:
:$\forall x \in \R_{>0}: \map f x = x^x$.
Then:
:$f$ is not of exponential order.
That is, it grows faster than any exponential.

Proof:
=== Lemma ===
{{:X to the x is not of Exponential Order/Lemma}}{{qed|lemma}}
By the definition of power:
:$\map f t = \map \exp {t \ln t}$ 
The theorem is equivalent to that there do not exist strictly positive real constants $M$, $K$, $a$ such that:
:$\forall t \ge M: \size {\map f t} < K e^{a t}$
{{AimForCont}} such constants $M$, $K$ and $a$ exist.
From the lemma, there exists a constant $C$ such that:
:$\forall t > C: \size {\map f t} > K e^{a t}$
For any $M$ chosen, $M + C > C$, thus from the lemma:
:$\size {\map f {M + C} } > K e^{a t}$
However, $M + C > M$, thus from the assumption:
:$\size {\map f {M + C} } < K e^{a t}$
Thus a contradiction has arisen.
It follows by Proof by Contradiction that our assumption was false.
Hence the result.
{{qed}}
Category:Exponential Order
2003ke53rfl9vsvwqpf2lz6q275hze7
Theorem: Empty Set is Bottom of Lattice of Power Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be the lattice of the power set of $X$.
Then:
:$\O = \bot$
where $\bot$ denotes the bottom of $L$.

Proof:
By Empty Set is Subset of All Sets:
:$\forall S \in \powerset X: \O \subseteq S$
By Empty Set is Element of Power Set:
:$\O \in \powerset X$
Thus by definition of the smallest element:
:$\O = \bot$
{{qed}}
Theorem: Limit of x to the x

Let $f: \R_{>0} \to \R$ be defined as:
:$\forall x \in \R_{>0}: \map f x = x^x$
Then:
:$\ds \lim_{x \mathop \to 0^+} x^x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0^+} x^x
      | r = \lim_{x \mathop \to 0^+} \map \exp {x \ln x}
      | c = {{Defof|Power (Algebra)|Power|subdef = Real Number|index = 1}}
}}
{{eqn | r = \map \exp {\lim_{x \mathop \to 0^+} x \ln x}
      | c = Exponential Function is Continuous
}}
{{eqn | r = \map \exp {\lim_{x \mathop \to 0^+} \frac {\ln x} {\frac 1 x} }
}}
{{eqn | r = \map \exp {\lim_{x \mathop \to 0^+} \frac {\frac 1 x} {\frac {-1} {x^2} } }
      | c = L'Hôpital's Rule
}}
{{eqn | r = \map \exp {\lim_{x \mathop \to 0^+} \frac {-x^2} x}
}}
{{eqn | r = \exp 0
}}
{{eqn | r = 1
      | c = Exponential of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of x to the x

Let $f: \R_{>0} \to \R$ be defined as:
:$\forall x \in \R_{>0}: \map f x = x^x$
Then:
:$\ds \lim_{x \mathop \to 0^+} x^x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0^+} x^x
      | r = \lim_{x \mathop \to 0^+} \map \exp {x \ln x}
      | c = {{Defof|Power (Algebra)|Power|subdef = Real Number|index = 1|disp}}
}}
{{eqn | r = \map \exp {\lim_{x \mathop \to 0^+} x \ln x}
      | c = Exponential Function is Continuous
}}
{{eqn | r = \exp 0
      | c = {{Corollary|Limit of Power of x by Absolute Value of Power of Logarithm of x|disp = Limit of Power of $x$ by Absolute Value of Power of Logarithm of $x$}}
}}
{{eqn | r = 1
      | c = Exponential of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Hermite-Lindemann-Weierstrass Theorem/Weaker

Let $a$ be a non-zero algebraic number (possibly complex).
Then:
:$e^a$ is transcendental
where $e$ is Euler's number.

Proof:
This follows trivially from Hermite-Lindemann-Weierstrass Theorem by taking $n = 1$.
{{qed}}
{{Namedfor|Charles Hermite|name2 = Carl Louis Ferdinand von Lindemann|name3 = Karl Theodor Wilhelm Weierstrass}}
Category:Hermite-Lindemann-Weierstrass Theorem
dc6lltdyk5rumubw9fjpblyf7pt2x9p
Theorem: Schanuel's Conjecture Implies Transcendence of Log Pi

Let Schanuel's Conjecture be true.
Then the logarithm of $\pi$ (pi):
:$\ln \pi$
is transcendental.

Proof:
Assume the truth of Schanuel's Conjecture.
From Schanuel's Conjecture Implies Algebraic Independence of Pi and Log of Pi over the Rationals, $\ln \pi$ and $\pi$ are algebraically independent over the rational numbers $\Q$.
Therefore, if Schanuel's Conjecture holds, $\ln \pi$ must be transcendental.
{{qed}}
Category:Transcendental Numbers
Category:Pi
Category:Logarithms
Category:Schanuel's Conjecture
mrrbpogcvdpyxo7t1dygcbazwaircyy
Theorem: Schanuel's Conjecture Implies Transcendence of Pi by Euler's Number

Let Schanuel's Conjecture be true.
Then $\pi \times e$ is transcendental.

Proof:
Assume the truth of Schanuel's Conjecture.
By Schanuel's Conjecture Implies Algebraic Independence of Pi and Euler's Number over the Rationals, $\pi$ and $e$ are algebraically independent over the rational numbers $\Q$.
That is, no non-trivial polynomials $\map f {x, y}$ with rational coefficients satisfy:
:$\map f {\pi, e} = 0$
{{AimForCont}} $\pi \times e$ is algebraic.
Then there would be a non-trivial polynomial $\map g z$ with rational coefficients satisfying:
:$\map g {\pi \times e} = 0$
However, $\map f {x, y} := \map g {x \times y}$ would be a non-trivial polynomial with rational coefficients satisfying:
:$\map f {\pi, e} = 0$
which contradicts the earlier statement that no such polynomials exist.
Therefore, if Schanuel's Conjecture holds, $\pi \times e$ is transcendental.
{{qed}}
Category:Transcendental Numbers
Category:Pi
Category:Euler's Number
Category:Schanuel's Conjecture
mvuajogd9vg72l5c5ibnbbdt67oty2s
Theorem: Schanuel's Conjecture Implies Transcendence of Pi plus Euler's Number

Let Schanuel's Conjecture be true.
Then $\pi + e$ is transcendental.

Proof:
Assume the truth of Schanuel's Conjecture.
By Schanuel's Conjecture Implies Algebraic Independence of Pi and Euler's Number over the Rationals, $\pi$ and $e$ are algebraically independent over the rational numbers $\Q$.
That is, no non-trivial polynomials $\map f {x, y}$ with rational coefficients satisfy:
:$\map f {\pi, e} = 0$
{{AimForCont}} $\pi + e$ is algebraic.
Then there would be a non-trivial polynomial $\map g z$ with rational coefficients satisfying:
:$\map g {\pi + e} = 0$
However, $\map f {x, y} := \map g {x + y}$ would be a non-trivial polynomial with rational coefficients satisfying:
:$\map f {\pi, e} = 0$
which contradicts the earlier statement that no such polynomials exist.
Therefore, if Schanuel's Conjecture holds, $\pi + e$ is transcendental.
{{qed}}
Category:Transcendental Numbers
Category:Pi
Category:Euler's Number
Category:Schanuel's Conjecture
aowdcvwj0okwfdcove95p30qj98qlre
Theorem: Transcendence of Sum or Product of Transcendentals

Let $a$ and $b$ be two transcendental numbers.
Then at least one of $a + b$ and $a \times b$ is transcendental.

Proof:
Proof by Contradiction:
{{AimForCont}} $a + b$ and $a \times b$ are both not transcendental.
Hence by definition, they are both algebraic.
Hence, $\left({z - a}\right) \left({z - b}\right)$ is a polynomial with algebraic coefficients.
Therefore, $a$ and $b$ must both be algebraic.
However, this contradicts with the assumption that $a$ and $b$ are both transcendental.
Hence by Proof by Contradiction it must follow that at least one of $a + b$ and $a \times b$ is transcendental.
{{qed}}
Category:Transcendental Numbers
q034nv8hp89erw2p8k2vyzxhde00y19
Theorem: Schanuel's Conjecture Implies Algebraic Independence of Pi and Euler's Number over the Rationals

Let Schanuel's Conjecture be true.
Then $\pi$ (pi) and $e$ (Euler's number) are algebraically independent over the rational numbers $\Q$.

Proof:
Assume the truth of Schanuel's Conjecture.
Let $z_1 = 1$ and $z_2 = i \pi$.
Note that $z_1$ is wholly real and $z_2$ is wholly imaginary.
Hence, by Wholly Real Number and Wholly Imaginary Number are Linearly Independent over the Rationals, they are linearly independent over $\Q$.
By Schanuel's Conjecture, the extension field $\map \Q {z_1, z_2, e^{z_1}, e^{z_2} }$ has transcendence degree at least $2$ over $\Q$.
That is, the extension field $\map \Q {1, i \pi, e, -1}$ has transcendence degree at least $2$ over $\Q$.
However, $1$ and $-1$ are algebraic.
Therefore $i \pi$ and $e$ must be algebraically independent over $\Q$.
{{AimForCont}} $\pi$ and $e$ are not algebraically independent over $\Q$.
Then, then there would be a non-trivial polynomial $\map g {x, y}$ with rational coefficients satisfying:
:$\map g {\pi, e} = 0$
Then, one can construct a non-trivial polynomial $\map f {x, y} = \map g {i x, y} \map g {-i x, y}$ with rational coefficients satisfying:
:$\map f {i \pi, e} = 0$
which is contradictory to the previous statement that no such polynomials exist.
Therefore, if Schanuel's Conjecture is true, then $\pi$ and $e$ are algebraically independent over $\Q$.
{{qed}}
Category:Transcendental Numbers
Category:Pi
Category:Euler's Number
Category:Schanuel's Conjecture
bca5qabvbylpy9qfnt7qhdjk2dw6izw
Theorem: Image of Mapping from Finite Set is Finite

Let $X, Y$ be sets.
Let $f: X \to Y$ be a mapping.
Let $X$ be a finite set.
Then $f \sqbrk X$ is a finite set.

Proof:
By definition of surjection:
:$f: X \to f \sqbrk X$ is a surjection.
The case when $X \ne \O$:
By Surjection iff Cardinal Inequality:
:$\card {f \sqbrk X} \le \card X$
Thus by Set of Cardinality not Greater than Cardinality of Finite Set is Finite:
:$f \sqbrk X$ is finite.
{{qed|lemma}}
The case when $X = \O$:
By {{Corollary|Image of Empty Set is Empty Set|1}}:
:$f \sqbrk X = \O$
Thus the result holds.
{{qed}}
Theorem: Magic Constant of Order 3 Magic Square

The magic constant of the order $3$ magic square is $15$.

Proof:
Let $M_3$ denote the order $3$ magic square
By Sum of Terms of Magic Square, the total of all the entries in $M_3$ is given by:
:$T_3 = \dfrac {3^2 \left({3^2 + 1}\right)} 2 = \dfrac {9 \times 10} 2 = 45$
As there are $3$ rows of $M_3$, the magic constant of $M_3$ is given by:
:$S_3 = \dfrac {45} 3 = 15$
{{qed}}
Theorem: Magic Constant of Order 3 Magic Square

The magic constant of the order $3$ magic square is $15$.

Proof:
Let $M_n$ denote the magic square of order $n$.
By Magic Constant of Magic Square, the magic constant of $M_n$ is given by:
:$S_n = \dfrac {n \left({n^2 + 1}\right)} 2$
Setting $n = 3$:
:$S_3 = \dfrac {3 \times 10} 2 = 15$
{{qed}}