avewright/proofwiki-math huggingface dataset:
Theorem: Irrationals are Everywhere Dense in Reals/Topology

Let $T = \struct {\R, \tau}$ denote the real number line with the usual (Euclidean) topology.
Let $\R \setminus \Q$ be the set of irrational numbers.
Then $\R \setminus \Q$ is everywhere dense in $T$.

Proof:
Let $x \in \R$.
Let $U \subseteq \R$ be an open set of $T$ such that $x \in U$.
From Basis for Euclidean Topology on Real Number Line, there exists an open interval $V_0 = \openint {x - \epsilon} {x + \epsilon} \subseteq U$ for some $\epsilon > 0$ such that $x \in V_0$.
From Between two Real Numbers exists Rational Number:
:$\exists p \in \Q: p \in \openint {x - \epsilon} {x + \epsilon}$
Thus, we can define the open interval $V_1 = \openint x p \subseteq V_0$.
Similarly:
:$\exists q \in \Q: q \in \openint x p$
We can then define an open interval $V_2 = \openint q p \subseteq V_1$.
We have $V_2 \subseteq V_1$, $V_1 \subseteq V_0$ and $V_0 \subseteq U$.
By successively applying Subset Relation is Transitive, it follows that $V_2 \subseteq U$.
Note that $x \notin V_2$, since $x < q < p < x + \epsilon$.
From Between two Rational Numbers exists Irrational Number, there exists $y \in \R \setminus \Q: y \in \openint q p = V_2$.
As $x \notin V_2$, it must be the case that $x \ne y$.
Since $V_2 \subseteq U$, $U$ is an open set of $T$ containing $x$ which also contains an element of $\R \setminus \Q$ other than $x$.
As $U$ is arbitrary, it follows that every open set of $T$ containing $x$ also contains an element of $\R \setminus \Q$ other than $x$.
That is, $x$ is by definition a limit point of $\R \setminus \Q$.
As $x$ is arbitrary, it follows that all elements of $\R$ are limit points of $\R \setminus \Q$.
The result follows from the definition of everywhere dense.
{{qed}}
Category:Real Analysis
Category:Real Number Line with Euclidean Topology
Category:Irrational Number Space
Category:Denseness
09xf05ij99hlu19r9bah8fmexbn8quc
Theorem: Irrationals are Everywhere Dense in Reals/Normed Vector Space

Let $\struct {\R, \size {\, \cdot \,} }$ be the normed vector space of real numbers.
Let $\R \setminus \Q$ be the set of irrational numbers.
Then $\R \setminus \Q$ is everywhere dense in $\struct {\R, \size {\, \cdot \,} }$

Proof:
Let $x \in \R$.
Let $\epsilon \in \R_{\mathop > 0}$
Either $x \in \Q$ or $x \in \R \setminus \Q$.
Suppose $x \in \R \setminus \Q$.
Let $y := x$.
Then:
:$\size {x - y} < \epsilon$
Suppose $x \in \Q$.
Let $n \in \N : n > \dfrac {\sqrt 2} \epsilon$
Let $y := x + \dfrac {\sqrt 2} n$
Then $y \in \R \setminus \Q$.
Furthermore:
{{begin-eqn}}
{{eqn | l = \size {x - y}
      | r = \size {\frac {\sqrt 2} n}
}}
{{eqn | o = <
     | r = \epsilon
}}
{{end-eqn}}
In both cases $x$ was arbitrary.
Hence:
:$\forall x \in \R : \exists \epsilon \in \R_{\mathop > 0} : \exists y \in \R \setminus \Q : \size {x - y} < \epsilon$
By definition, $\R \setminus \Q$ is dense in $\R$.
{{qed}}
Theorem: Real Number Subtracted from Itself leaves Zero

Let $x \in \R$ be a real number.
Then:
:$x - x = 0$
where $x - x$ denotes the operation of real subtraction.

Proof:
{{begin-eqn}}
{{eqn | l = x - x
      | r = x + \paren {-x}
      | c = {{Defof|Real Subtraction}}
}}
{{eqn | r = 0
      | c = Inverse for Real Addition
}}
{{end-eqn}}
{{qed}}
Theorem: Real Number Ordering is Compatible with Multiplication/Positive Factor/Corollary

:$\forall a, b, c, d \in \R: 0 < a < b \land 0 < c < d \implies a c < b d$

Proof:
{{begin-eqn}}
{{eqn | l = a < b
      | o = \implies
      | r = a \times c < b \times c
      | c = Real Number Ordering is Compatible with Multiplication: Positive Factor as $c > 0$
}}
{{eqn | l = c < d
      | o = \implies
      | r = b \times c < b \times d
      | c = Real Number Ordering is Compatible with Multiplication: Positive Factor as $b > 0$
}}
{{end-eqn}}
The result follows by the Transitive Law.
{{Qed}}
Theorem: Equivalence of Definitions of Matroid Base Axioms

Let $S$ be a finite set.
Let $\mathscr B$ be a non-empty set of subsets of $S$.
{{TFAE|axiom = Base Axiom (Matroid)|view = matroid base axiom}}
{{:Axiom:Base Axiom (Matroid)}}

Proof:
=== Formulation $1$ iff Formulation $2$ ===
Formulation $1$ holds {{iff}} formulation $2$ holds follows immediately from {{Corollary|Set Difference Then Union Equals Union Then Set Difference}}.
{{qed|lemma}}
Theorem: Number of Parameters of Moving Average Model

Let $S$ be a stochastic process based on an equispaced time series.
Let the values of $S$ at timestamps $t, t - 1, t - 2, \dotsc$ be $z_t, z_{t - 1}, z_{t - 2}, \dotsc$
Let $\tilde z_t$ be the deviation from a constant mean level $\mu$:
:$\tilde z_t = z_t - \mu$
Let $a_t, a_{t - 1}, a_{t - 2}, \dotsc$ be a sequence of independent shocks at timestamps $t, t - 1, t - 2, \dotsc$
Let $M$ be an '''moving average model''' on $S$ of order $q$:
:$\tilde z_t = a_t - \theta_1 a_{t - 1} - \theta_2 a_{t - 2} - \dotsb - \theta_q a_{t - q}$
Then $M$ has $q + 2$ parameters.
</onlyinclude>

Proof:
By definition of the parameters of $M$:
{{:Definition:Parameter of Moving Average Model}}
Thus:
:there are $q$ parameters of the form $\theta_j$
:$1$ parameter $\mu$
:$1$ parameter $\sigma_a^2$.
That is: $q + 1 + 1 = q + 2$ parameters.
{{qed}}
Theorem: Convergent Sequence is Cauchy Sequence/Metric Space

Let $M = \struct {A, d}$ be a metric space.
Every convergent sequence in $A$ is a Cauchy sequence.

Proof:
Let $\sequence {x_n}$ be a sequence in $A$ that converges to the limit $l \in A$.
Let $\epsilon > 0$. 
Then also $\dfrac \epsilon 2 > 0$.
Because $\sequence {x_n}$ converges to $l$ in $A$, we have:
:$\exists N_1 \in \R_{>0}: \forall n > N_1: \map d {x_n, l} < \dfrac \epsilon 2$
Because $\sequence {x_n}$ converges to $l$, there must also exist at least one sequence $\sequence {x_m}$ in $A$ that converges to the limit $l \in A$, for some $m \in \R_{>0}$.
We have:
:$\exists N_2 \in \R_{>0}: \forall m > N_2: \map d {x_m, l} < \dfrac \epsilon 2$
So if $N = \map \max {N_1, N_2}$, such that $m > N$ and $n > N$, then:
{{begin-eqn}}
{{eqn | l = \map d {x_n, x_m}
      | o = \le
      | r = \map d {x_n, l} + \map d {l, x_m}
      | c = {{Metric-space-axiom|2}}
}}
{{eqn | r = \map d {x_n, l} + \map d {x_m, l}
      | c = {{Metric-space-axiom|3}}
}}
{{eqn | o = <
      | r = \frac \epsilon 2 + \frac \epsilon 2
      | c = by choice of $N$
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
Thus $\sequence {x_n}$ is a Cauchy sequence.
{{qed}}
Theorem: Number of Parameters of ARMA Model

Let $S$ be a stochastic process based on an equispaced time series.
Let the values of $S$ at timestamps $t, t - 1, t - 2, \dotsc$ be $z_t, z_{t - 1}, z_{t - 2}, \dotsc$
Let $\tilde z_t, \tilde z_{t - 1}, \tilde z_{t - 2}, \dotsc$ be deviations from a constant mean level $\mu$:
:$\tilde z_t = z_t - \mu$
Let $a_t, a_{t - 1}, a_{t - 2}, \dotsc$ be a sequence of independent shocks at timestamps $t, t - 1, t - 2, \dotsc$
Let $M$ be an '''ARMA model''' on $S$ of order $p$:
:$\tilde z_t = \phi_1 \tilde z_{t - 1} + \phi_2 \tilde z_{t - 2} + \dotsb + \phi_p \tilde z_{t - p} + a_t - \theta_1 a_{t - 1} - \theta_2 a_{t - 2} - \dotsb - \theta_q a_{t - q}$
Then $M$ has $p + q + 2$ parameters.
</onlyinclude>

Proof:
By definition of the parameters of $M$:
{{:Definition:Parameter of ARMA Model}}
Thus:
:there are $p$ parameters of the form $\phi_i$
:there are $q$ parameters of the form $\theta_j$
:$1$ parameter $\mu$
:$1$ parameter $\sigma_a^2$.
That is: $p + q + 1 + 1 = p + q + 2$ parameters.
{{qed}}
Theorem: Characteristic of Field by Annihilator/Characteristic Zero

Suppose that:
:$\map {\mathrm {Ann} } F = \set 0$
That is, the annihilator of $F$ consists of the zero only.
Then:
:$\Char F = 0$
That is, the characteristic of $F$ is zero.

Proof:
Let the zero of $F$ be $0_F$ and the unity of $F$ be $1_F$.
By definition of characteristic, $\Char F = 0$ {{iff}}:
:$\not \exists n \in \Z, n > 0: \forall r \in F: n \cdot r = 0_F$
That is, there exists no $n \in \Z, n > 0$ such that $n \cdot r = 0_F$ for all $r \in F$.
But note that $\forall r \in F: 0 \cdot r = 0_F$ by definition of integral multiple.
{{AimForCont}} there exists a non-zero element of $\map {\mathrm {Ann} } F$.
From Non-Trivial Annihilator Contains Positive Integer, $\map {\mathrm {Ann} } F$ must contain a (strictly) positive integer.
But this would contradict the statement that $\Char F = 0$.
So it follows that:
:$\map {\mathrm {Ann} } F = \set 0 \iff \Char F = 0$
{{qed|lemma}}
Theorem: Characteristic of Field by Annihilator/Prime Characteristic

Suppose that:
:$\exists n \in \map {\mathrm {Ann} } F: n \ne 0$
That is, there exists (at least one) non-zero integer in the annihilator of $F$.
If this is the case, then the characteristic of $F$ is non-zero:
:$\Char F = p \ne 0$
and the annihilator of $F$ consists of the set of integer multiples of $p$:
:$\map {\mathrm {Ann} } F = p \Z$
where $p$ is a prime number.

Proof:
Let $A := \map {\mathrm {Ann} } F$.
We are told that:
:$\exists n \in A: n \ne 0$
Consider the set $A^+ \set {n \in A: n > 0}$.
From Non-Trivial Annihilator Contains Positive Integer we have that $A^+ \ne \O$.
As $A^+ \subseteq \N$ it follows from the well-ordering principle that $A^+$ has a least value $p$, say.
{{AimForCont}} $p$ is not a prime number.
Then $p$ can be expressed as $p = a b$ where $1 < a, b < p$.
{{begin-eqn}}
{{eqn | l = 0_R
      | r = p \cdot 1_F
      | c = {{Defof|Annihilator of Ring}}
}}
{{eqn | r = \paren {a b} \cdot 1_F
      | c = 
}}
{{eqn | r = \paren {a \cdot 1_F} \times \paren {b \cdot 1_F}
      | c = Product of Integral Multiples
}}
{{eqn | r = \paren {a \cdot 1_F} = 0_F \lor \paren {b \cdot 1_F} = 0_F
      | c = Field has no Proper Zero Divisors
}}
{{end-eqn}}
But then either $a \in A$ or $b \in A$, and so $p$ is not the minimal positive element of $A$ after all.
So from this contradiction it follows that $p$ is necessarily prime.
Next let $n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {n p} \cdot 1_F
      | r = n \cdot \paren {p \cdot 1_F}
      | c = Integral Multiple of Integral Multiple
}}
{{eqn | r = n \cdot 0_F
      | c = as $p$ is in the annihilator of $F$
}}
{{eqn | r = 0_F
      | c = {{Defof|Integral Multiple}}
}}
{{end-eqn}}
So all multiples of $p$ are in $A$.
Finally, suppose $k \in A$.
By the Division Theorem $k = q p + r$ where $0 \le r < p$.
Then:
{{begin-eqn}}
{{eqn | l = 0_F
      | r = k \cdot 0_F
      | c = {{Defof|Integral Multiple}}
}}
{{eqn | r = \paren {q p + r} \cdot 1_F
      | c = 
}}
{{eqn | r = \paren {q p} \cdot 1_F + r \cdot 1_F
      | c = Integral Multiple Distributes over Ring Addition
}}
{{eqn | r = 0_F + r \cdot 1_F
      | c = from above: $q p$ is a multiple of $p$
}}
{{eqn | r = r \cdot 1_F
      | c = {{Defof|Field Zero}}
}}
{{end-eqn}}
So $r \in A$ contradicting the stipulation that $p$ is the smallest positive element of $A$.
Hence all and only multiples of $p$ are in $A$.
{{qed}}
Theorem: Cauchy Sequence is Bounded/Metric Space

Let $M = \struct {A, d}$ be a metric space.
Then every Cauchy sequence in $M$ is bounded.

Proof:
Let $\sequence {x_n}$ be a Cauchy sequence in $M$.
By definition:
:$\forall \epsilon > 0: \exists N \in \N: \forall m, n > N: \map d {x_n, x_m} < \epsilon$
Particularly, setting $\epsilon = 1$:
:$\exists N_1: \forall m, n > N_1: \map d {x_n, x_m} < 1$
Note that since $N_1 \ge N_1$, this means that:
:$\forall n \ge N_1: \map d {x_n, x_{N_1} } < 1$
To show $\sequence {x_n}$ is bounded, we need to show that there exists $a \in A$ and $K \in \R$ such that $\map d {x_n, a} \le K$ for all $x_n \in \sequence {x_n}$.
Let $K'$ be the maximum distance from $x_{N_1}$ to any of the earlier terms in the sequence.
That is, $K' = \max \set {\map d {x_{N_1}, x_1}, \map d {x_{N_1},  x_2}, \ldots, \map d {x_{N_1}, x_{N_1 - 1} } }$
Then:
:Each $x_n$ for $n \ge N_1$ satisfies $\map d {x_{N_1}, x_n} \le 1$ by choice of $N_1$ as mentioned above
:Each $x_n$ for $n < N_1$ satisfies $\map d {x_{N_1}, x_n} \le K'$ by choice of $K'$.
Thus, taking $a = x_{N_1}$ and $K = \max \set {K', 1}$, we have shown that each $x_n$ satisfies $\map d {a, x_n} \le K$.
So, $\sequence {x_n}$ is bounded.
{{qed}}
Theorem: ARIMA Model subsumes ARMA Model

Let $S$ be a stochastic process based on an equispaced time series.
Let $M$ be an ARMA model for $S$.
Then $M$ is also an implementation of an ARIMA model.

Proof:
Let the values of $S$ at timestamps $t, t - 1, t - 2, \dotsc$ be $z_t, z_{t - 1}, z_{t - 2}, \dotsc$
Let $\tilde z_t, \tilde z_{t - 1}, \tilde z_{t - 2}, \dotsc$ be deviations from a constant mean level $\mu$:
:$\tilde z_t = z_t - \mu$
Let $a_t, a_{t - 1}, a_{t - 2}, \dotsc$ be a sequence of independent shocks at timestamps $t, t - 1, t - 2, \dotsc$
By definition of ARMA model, $M$ is implemented as:
:$(1): \quad \tilde z_t = \phi_1 \tilde z_{t - 1} + \phi_2 \tilde z_{t - 2} + \dotsb + \phi_p \tilde z_{t - p} + a_t - \theta_1 a_{t - 1} - \theta_2 a_{t - 2} - \dotsb - \theta_q a_{t - q}$
The general ARIMA model is implemented as:
:$w_t = \phi_1 w_{t - 1} + \phi_2 w_{t - 2} + \dotsb + \phi_p w_{t - p} + a_t - \theta_1 a_{t - 1} - \theta_2 a_{t - 2} - \dotsb - \theta_q a_{t - q}$
where:
:$w_t = \nabla^d z_t$
Letting $d = 0$ we have:
:$w_t = z_t$
Setting $w_t = z_t - \mu = \tilde z$, we recover $(1)$.
{{qed}}
Theorem: ARIMA Model subsumes Autoregressive Model

Let $S$ be a stochastic process based on an equispaced time series.
Let $M$ be an autoregressive model for $S$.
Then $M$ is also an implementation of an ARIMA model.

Proof:
Let the values of $S$ at timestamps $t, t - 1, t - 2, \dotsc$ be $z_t, z_{t - 1}, z_{t - 2}, \dotsc$
Let $\tilde z_t, \tilde z_{t - 1}, \tilde z_{t - 2}, \dotsc$ be deviations from a constant mean level $\mu$:
:$\tilde z_t = z_t - \mu$
Let $a_t, a_{t - 1}, a_{t - 2}, \dotsc$ be a sequence of independent shocks at timestamps $t, t - 1, t - 2, \dotsc$
By definition of autoregressive model, $M$ is implemented as:
:$(1): \quad \tilde z_t = \phi_1 \tilde z_{t - 1} + \phi_2 \tilde z_{t - 2} + \dotsb + \phi_p \tilde z_{t - p} + a_t$
The general ARIMA model is implemented as:
:$w_t = \phi_1 w_{t - 1} + \phi_2 w_{t - 2} + \dotsb + \phi_p w_{t - p} + a_t - \theta_1 a_{t - 1} - \theta_2 a_{t - 2} - \dotsb - \theta_q a_{t - q}$
where:
:$w_t = \nabla^d z_t$
Let $\theta_j = 0$ for all $j$.
Letting $d = 0$ we have:
:$w_t = z_t$
Setting $w_t = z_t - \mu = \tilde z$, we recover $(1)$.
{{qed}}
Theorem: ARIMA Model subsumes Moving Average Model

Let $S$ be a stochastic process based on an equispaced time series.
Let $M$ be a moving average model for $S$.
Then $M$ is also an implementation of an ARIMA model.

Proof:
Let the values of $S$ at timestamps $t, t - 1, t - 2, \dotsc$ be $z_t, z_{t - 1}, z_{t - 2}, \dotsc$
Let $\tilde z_t, \tilde z_{t - 1}, \tilde z_{t - 2}, \dotsc$ be deviations from a constant mean level $\mu$:
:$\tilde z_t = z_t - \mu$
Let $a_t, a_{t - 1}, a_{t - 2}, \dotsc$ be a sequence of independent shocks at timestamps $t, t - 1, t - 2, \dotsc$
By definition of moving average model, $M$ is implemented as:
:$(1): \quad \tilde z_t = a_t - \theta_1 a_{t - 1} - \theta_2 a_{t - 2} - \dotsb - \theta_q a_{t - q}$
The general ARIMA model is implemented as:
:$w_t = \phi_1 w_{t - 1} + \phi_2 w_{t - 2} + \dotsb + \phi_p w_{t - p} + a_t - \theta_1 a_{t - 1} - \theta_2 a_{t - 2} - \dotsb - \theta_q a_{t - q}$
where:
:$w_t = \nabla^d z_t$
Let $\phi_i = 0$ for all $i$.
Letting $d = 0$ we have:
:$w_t = z_t$
Setting $w_t = z_t - \mu = \tilde z$, we recover $(1)$.
{{qed}}
Theorem: Real Division is not Closed

The operation of division on the set of real numbers $\R$ is not closed.

Proof:
From Division by Zero, we have that for all $a \in \R$, the operation $\dfrac a 0$ is not defined.
{{qed}}
Theorem: Strictly Positive Real Numbers are not Closed under Subtraction

The set $\R_{>0}$ of strictly positive real numbers is not closed under subtraction.

Proof:
;Proof by Counterexample
Let $a = 1$ and $b = 2$.
Then:
:$a - b = -1$
but $-1$ is not a (strictly) positive real number.
{{qed}}
Theorem: Zero of Field is Unique

Let $\struct {F, +, \times}$ be a field.
The zero of $F$ is unique.

Proof:
By definition, a field is a ring whose ring product less zero is an abelian group.
The result follows from Ring Zero is Unique.
{{qed}}
Theorem: Zero of Field is Unique

Let $\struct {F, +, \times}$ be a field.
The zero of $F$ is unique.

Proof:
Let $0_1$ and $0_2$ both be elements of $F$ such that:
:$\forall a \in F: a + 0_1 = a$
:$\forall a \in F: a + 0_2 = a$
Then:
:$0_1 + 0_2 = 0_2$
because $0_1$ is a zero element
:$0_1 + 0_2 = 0_1$
because $0_2$ is a zero element
Hence:
:$0_1 = 0_2$
and the two zero elements are the same.
{{qed}}
Theorem: Negative of Element in Field is Unique

Let $\struct {F, +, \times}$ be a field.
Let $a \in F$.
Then the negative $-a$ of $a$ is unique.

Proof:
By definition, a field is a ring whose ring product less zero is an abelian group.
The result follows from Ring Negative is Unique.
{{qed}}
Theorem: Negative of Element in Field is Unique

Let $\struct {F, +, \times}$ be a field.
Let $a \in F$.
Then the negative $-a$ of $a$ is unique.

Proof:
Let $b, c \in F$ such that both $a + b = 0$ and $a + c = 0$.
Thus:
{{begin-eqn}}
{{eqn | l = b + \paren {a + c}
      | r = b + 0
      | c = as $c$ is a negative of $a$
}}
{{eqn | r = b
      | c = {{Defof|Field Zero}}
}}
{{end-eqn}}
But also:
{{begin-eqn}}
{{eqn | l = \paren {b + a} + c
      | r = \paren {a + b} + c
      | c = {{Field-axiom|A1}}
}}
{{eqn | r = 0 + c
      | c = as $b$ is a negative of $a$
}}
{{eqn | r = c
      | c = {{Defof|Field Zero}}
}}
{{end-eqn}}
So $b = c$ and the result follows.
{{qed}}
Theorem: Space of Bounded Sequences with Supremum Norm forms Banach Space

Let $\struct {\map {\ell^\infty} \R, \norm {\, \cdot \,}_\infty}$ be the normed vector space of bounded sequences on $\R$.
Then $\struct {\map {\ell^\infty} \R, \norm {\, \cdot \,}_\infty}$ is a Banach space.

Proof:
A Banach space is a normed vector space, where a Cauchy sequence converges {{WRT}} the supplied norm.
To prove the theorem, we need to show that a Cauchy sequence in $\struct {\map {\ell^\infty} \R, \norm {\,\cdot\,}_\infty}$ converges.
We take a Cauchy sequence $\sequence {x_n}_{n \mathop \in \N}$ in $\struct {\map {\ell^\infty} \R, \norm {\,\cdot\,}_\infty}$.
Then we consider the $k$th component and show, that a real Cauchy sequence $\sequence {x_n^{\paren k}}_{n \mathop \in \N}$ converges in $\struct {\R, \size {\, \cdot \,}}$ with the limit $x^{\paren k}$ and denote the entire set as $\mathbf x$.
Finally, we show that $\sequence {\mathbf x_n}_{n \in \N}$, composed of components $x_n^{\paren k},$ converges in $\struct {\map {\ell^\infty} \R, \norm {\,\cdot\,}_\infty}$ with the limit $\mathbf x$.
Let $\sequence {\mathbf x_n}_{n \mathop \in \N}$ be a Cauchy sequence in $\struct {\map {\ell^\infty} \R, \norm{\, \cdot \,}_\infty}$.
Denote the $k$th component of $\mathbf x_n$ by $x_n^{\paren k}$.
Theorem: Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom/Lemma 2

:$\forall B_1, B_2 \in \mathscr B : \card{B_1} = \card{B_2}$
where $\card{B_1}$ and $\card{B_2}$ denote the cardinality of the sets $B_1$ and $B_2$ respectively.

Proof:
{{AimForCont}}:
:$\exists B_1, B_2 \in \mathscr B : \card{B_1} \ne \card{B_2}$
{{WLOG}} and from Max Operation Equals an Operand let:
:$\card{B_1 \cap B_2} = \max \set{\card{C_1 \cap C_2} : C_1, C_2 \in \mathscr B : \card{C_1} \ne \card{C_2}}$
{{WLOG}} let:
:$\card{B_1} > \card{B_2}$
From Set Difference of Larger Set with Smaller is Not Empty:
:$\exists x \in B_1 \setminus B_2$
From base axiom $(\text B 1)$:
:$\exists y \in B_2 \setminus B_1 : \paren {B_1 \setminus \set x} \cup \set y \in \mathscr B$
Let $B_3 = \paren {B_1 \setminus \set x} \cup \set y$.
From Finite Set Formed by Substitution has Larger Intersection:
:$\card{B_3 \cap B_2} = \card{B_1 \cap B_2} + 1$
From Finite Set Formed by Substitution has Same Cardinality:
:$\card {B_3} = \card {B_1}$
Hence:
:$\card {B_3} \ne \card {B_2}$
This contradicts the choice of $B_1$ and $B_2$ as:
:$\card{B_1 \cap B_2} = \max \set{\card{C_1 \cap C_2} : C_1, C_2 \in \mathscr B : \card{C_1} \ne \card{C_2}}$
It follows that:
:$\forall B_1, B_2 \in \mathscr B : \card{B_1} = \card{B_2}$
{{qed}}
Category:Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom
4mc3ol8x12coim0gg62xgwn3l62ufl8
Theorem: Negative of Field Negative

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$.
Let $a \in F$ and let $-a$ be the field negative of $a$.
Then:
:$-\paren {-a} = a$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {-a} + a
      | r = a + \paren {-a}
      | c = {{Field-axiom|A2}}
}}
{{eqn | r = 0_F
      | c = {{Field-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = a
      | r = -\paren {-a}
      | c = {{Defof|Field Negative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Field Product with Zero

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$.
Let $a \in F$.
Then:
:$a \times 0_F = 0_F$

Proof:
{{begin-eqn}}
{{eqn | l = a
      | r = a \times 1_F
      | c = {{Field-axiom|M3}}: $1_F$ is the unity of $F$
}}
{{eqn | r = a \times \paren {0_F + 1_F}
      | c = {{Field-axiom|A3}}
}}
{{eqn | r = a \times 0_F + a \times 1_F
      | c = {{Field-axiom|D}}
}}
{{eqn | r = a \times 0_F + a
      | c = {{Field-axiom|M3}}
}}
{{eqn | ll= \leadsto
      | l = \paren {a \times 0_F + a} + \paren {-a}
      | r = a + \paren {-a}
      | c = adding $-a$ to both sides
}}
{{eqn | ll= \leadsto
      | l = a \times 0_F + \paren {a + \paren {-a} }
      | r = a + \paren {-a}
      | c = {{Field-axiom|A1}}
}}
{{eqn | ll= \leadsto
      | l = a \times 0_F + 0_F
      | r = 0_F
      | c = {{Field-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = a \times 0_F
      | r = 0_F
      | c = {{Field-axiom|A3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product with Field Negative

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $a, b \in F$.
Then:
:$-\paren {a \times b} = a \times \paren {-b} = \paren {-a} \times b$

Proof:
{{begin-eqn}}
{{eqn | l = a \times b + a \times \paren {-b}
      | r = a \times \paren {b + \paren {-b} }
      | c = {{Field-axiom|A1}}
}}
{{eqn | r = a \times 0_F
      | c = {{Field-axiom|A4}}
}}
{{eqn | r = 0_F
      | c = Field Product with Zero
}}
{{eqn | ll= \leadsto
      | l = -\paren {a \times b}
      | r = a \times \paren {-b}
      | c = {{Defof|Ring Negative}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = \paren {-a} \times b + a \times b
      | r = \paren {\paren {-a} + a} \times b
      | c = {{Field-axiom|A1}}
}}
{{eqn | r = 0_F \times a
      | c = {{Field-axiom|A4}}
}}
{{eqn | r = 0_F
      | c = Field Product with Zero
}}
{{eqn | ll= \leadsto
      | l = -\paren {a \times b}
      | r = \paren {-a} \times b
      | c = {{Defof|Ring Negative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product with Field Negative/Corollary

:$\paren {-1_F} \times a = \paren {-a}$

Proof:
{{begin-eqn}}
{{eqn | l = a + \paren {-1_F} \times a
      | r = 1_F \times a + \paren {-1_F} \times a
      | c = {{Field-axiom|M3}}
}}
{{eqn | r = \paren {1_F + \paren {-1_F} } \times a
      | c = {{Field-axiom|D}}
}}
{{eqn | r = 0_F \times a
      | c = {{Field-axiom|A4}}
}}
{{eqn | r = 0_F
      | c = Field Product with Zero
}}
{{eqn | ll= \leadsto
      | l = \paren {-a}
      | r = \paren {-1_F} \times a
      | c = {{Defof|Ring Negative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Condition for Division by Field Elements to be Unity

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $a, b \in F$.
Then:
:$\dfrac a b = 1_F$
{{iff}}:
:$a = b$
where $\dfrac a b$ denotes division.

Proof:
=== Necessary Condition ===
Let $a = b$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac a b
      | r = a \times b^{-1}
      | c = {{Defof|Division over Field}}
}}
{{eqn | r = b \times b^{-1}
      | c = as $a = b$
}}
{{eqn | r = 1_F
      | c = {{Field-axiom|M4}}
}}
{{end-eqn}}
{{qed|lemma}}