avewright/proofwiki-math huggingface dataset:
Theorem: Ratios of Fractions in Lowest Terms

Let $a, b, c, d \in \Z_{>0}$ be positive integers.
Let $\dfrac a b$ be in canonical form.
Let $\dfrac a b = \dfrac c d$.
Then:
:$a \divides c$
and:
:$b \divides d$
where $\divides$ denotes divisibility.
{{:Euclid:Proposition/VII/20}}

Proof:
Let $CD, EF$ be the least (natural) numbers of those which have the same ratio with $A, B$.
We need to show that $CD$ measures $A$ the same number of times that $EF$ measures $B$.
:250px
Suppose $CD$ is an aliquant part of $A$.
Then from {{EuclidPropLink|book = VII|prop = 13|title = Proportional Numbers are Proportional Alternately}} and {{EuclidDefLink|VII|20|Proportional}}, $EF$ is also the same aliquant part of $B$ that $CD$ is of $A$.
Therefore as many aliquant parts of $A$ as there are in $CD$, so many aliquant parts of $B$ are there also in $EF$.
Let $CD$ be divided into the aliquant parts of $A$, namely $CG, GD$ and $EF$ into the aliquant parts of $B$, namely $EH, HF$.
Thus the multitude of $CG, GD$ will be equal to the multitude of $EH, HF$.
We have that the numbers $CG, GD$ are equal to one another, and the numbers $EH, HF$ are also equal to one another, 
Therefore $CG : EH = GD : HF$.
So from {{EuclidPropLink|book = VII|prop = 12|title = Ratios of Numbers is Distributive over Addition}}, as one of the antecedents is to one of the consequents, so will all the antecedents be to all the consequents.
Therefore $CG : EH = CD : EF$.
Therefore $CG, EH$ are in the same ratio with $CD, EF$ being less than they.
This is impossible, for by hypothesis $CD, EF$ are the least numbers of those which have the same ratio with them.
So $CD$ is not an aliquant part of $A$.
Therefore from {{EuclidPropLink|book = VII|prop = 4|title = Natural Number Divisor or Multiple of Divisor of Another}}, $CD$ is an aliquot part of $A$.
Also, from {{EuclidPropLink|book = VII|prop = 13|title = Proportional Numbers are Proportional Alternately}} and {{EuclidDefLink|VII|20|Proportional}}, $EF$ is the same aliquot part of $B$ that $CD$ is of $A$.
Therefore $CD$ measures $A$ the same number of times that $EF$ measures $B$.
{{Qed}}
{{Euclid Note|20|VII}}
Theorem: Gelfond-Schneider Theorem

Let $\alpha$ and $\beta$ be algebraic numbers (possibly complex) such that $\alpha \notin \set {0, 1}$.
Let $\beta$ be irrational, that is:
:$\beta \notin \Q$
This includes $\beta$ being imaginary or complex.
Then any value of $\alpha^\beta$ is transcendental.

Proof:
Let $\alpha$ be an algebraic number such that $\alpha \ne 0$ and $\alpha \ne 1$.
Let $\beta$ be an algebraic number such that some value of $\alpha^\beta$ is algebraic.
The result will follow if we can show that $\beta \in \Q$.
We treat only the special case that $\alpha, \beta \in \R$ and $\alpha > 0$, assuming that $\map \exp {\beta \ln \alpha}$ is algebraic for the real value of $\ln \alpha$.
Observe that $\alpha^{s_1 + s_2 \beta}$ is an algebraic number for all integers $s_1$ and $s_2$.
To establish the result, it is enough to show that there are two distinct pairs of integers $\tuple {s_1, s_2}$ and $\tuple {s'_1, s'_2}$ for which:
:$s_1 + s_2 \beta = s'_1 + s'_2 \beta$ 
since that implies:
:$\beta = \dfrac{s_1 - s'_1} {s'_2 - s_2} \in \Q$
We will choose $S$ sufficiently large and show such pairs exist with $0 \le s_1, s_2, s'_1, s'_2 < S$.
Theorem: Norm of Unit of Normed Division Algebra

Let $\struct {A_F, \oplus}$ be a normed division algebra.
Let the unit of $\struct {A_F, \oplus}$ be $1_A$.
Then:
:$\norm {1_A} = 1$
where $\norm {1_A}$ denotes the norm of $1_A$.

Proof:
By definition:
:$\forall a, b \in A_F: \norm {a \oplus b} = \norm a \norm b$
So:
:$\norm {1_A} = \norm {1_A \oplus 1_A} = \norm {1_A} \norm {1_A}$
So $\norm {1_A} \in \R$ is idempotent under real multiplication.
From Idempotent Elements of Ring with No Proper Zero Divisors, only $0 \in \R$ and $1 \in \R$ fit that bill.
But $\norm {1_A}$ can not be $0$ as that would make:
:$\forall a \in A_F: \norm a = \norm {1_A \oplus a} = \norm {1_A} \norm a = 0 \norm a = 0$
which contradicts the definition of the norm.
Hence the result.
{{Qed}}
Theorem: Commutator on Algebra is Alternating Bilinear Mapping

Let $\struct {A_R, \oplus}$ be an algebra over a ring.
Then the commutator on $\struct {A_R, \oplus}$ is an alternating bilinear mapping:
:$\forall a, b \in A_R: \sqbrk {a, b} = -\sqbrk {b, a}$

Proof:
{{begin-eqn}}
{{eqn | l = \sqbrk {a, b}
      | r = a \oplus b - b \oplus a
      | c = 
}}
{{eqn | r = -b \oplus a + a \oplus b
      | c = 
}}
{{eqn | r = -b \oplus a - \paren {-\paren {a \oplus b} }
      | c = 
}}
{{eqn | r = -\paren {b \oplus a - a \oplus b}
      | c = 
}}
{{eqn | r = -\sqbrk {b, a}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Multiplicative Inverse in Nicely Normed Star-Algebra

Let $A = \struct {A_F, \oplus}$ be a nicely normed $*$-algebra whose conjugation is denoted $*$.
Let $a \in A$.
Then the multiplicative inverse of $a$ is given by:
:$a^{-1} = \dfrac {a^*} {\norm a^2}$
where:
:$a^*$ is the conjugate of $a$
:$\norm a$ is the norm of $a$.

Proof:
For the result to hold, we need to show that $a \oplus \dfrac {a^*} {\norm a^2} = 1 = \dfrac {a^*} {\norm a^2} \oplus a$.
{{begin-eqn}}
{{eqn | o = 
      | r = a \oplus \dfrac {a^*} {\norm a^2}
      | c = 
}}
{{eqn | r = a \oplus a^* \cdot \dfrac 1 {\norm a^2}
      | c = 
}}
{{eqn | r = \norm a^2 \cdot \dfrac 1 {\norm a^2}
      | c = {{Defof|Nicely Normed Star-Algebra}}
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | r = \dfrac 1 {\norm a^2} \cdot \norm a^2
      | c = 
}}
{{eqn | r = \dfrac 1 {\norm a^2} \cdot a^* \oplus a
      | c = {{Defof|Nicely Normed Star-Algebra}}
}}
{{eqn | r = \dfrac {a^*} {\norm a^2}\oplus a
      | c = 
}}
{{end-eqn}}
{{qed}}
Note that this construction works whether $\oplus$ is associative or not.
Theorem: Nicely Normed Alternative Algebra is Normed Division Algebra

$A = \struct {A_F, \oplus}$ be a nicely normed $*$-algebra which is also an alternative algebra.
Then $A$ is a normed division algebra.

Proof:
Let $a, b \in A$.
Then all of $a, b, a^*, b^*$ can be generated by $\map \Im a$ and $\map \Im b$.
{{explain|Prove the above statement.}}
So as $A$ is an alternative algebra, it follows that $\oplus$ is associative for $a, b, a^*, b^*$.
So:
{{begin-eqn}}
{{eqn | l = \norm {a b}^2
      | r = \paren {a \oplus b} \oplus \paren {a \oplus b}^*
      | c = {{Defof|Norm on Vector Space|Norm}} in Nicely Normed $*$-Algebra
}}
{{eqn | r = a \oplus b \oplus \paren {b^* \oplus a^*}
      | c = {{Defof|Conjugate (Algebra)|Conjugate}}
}}
{{eqn | r = a \oplus \paren {b \oplus b^*} \oplus a^*
      | c = Associativity of $\oplus$ (from above)
}}
{{eqn | r = \norm a^2 \norm b^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Artin's Theorem on Alternative Algebras

Let $A = \struct {A_R, \oplus}$ be an algebra over the ring $R$ such that $A$ is ''not'' a boolean algebra.
Then $A$ is alternative {{iff}}:
:$\forall a, b \in A: \paren {a \oplus a} \oplus b = a \oplus \paren {a \oplus b}$
:$\forall a, b \in A: \paren {b \oplus a} \oplus a = b \oplus \paren {a \oplus a}$

Proof:
When $A$ is 
So suppose that:
:$\forall a, b \in A: \paren {a \oplus a} \oplus b = a \oplus \paren {a \oplus b}$
:$\forall a, b \in A: \paren {b \oplus a} \oplus a = b \oplus \paren {a \oplus a}$
Then:
:$\sqbrk {a, a, b} = 0$
:$\sqbrk {b, a, a} = 0$
where $\sqbrk {a, a, b}$ denotes the associator of $a, b \in A_R$.
Now let us compute, using the linearity of $\oplus$ and the two suppositions:
{{begin-eqn}}
{{eqn | l = \paren {a - b} \oplus \paren {\paren {a - b} \oplus a}
      | r = a \oplus \paren {\paren {a - b} \oplus a} - b \oplus \paren {\paren {a - b} \oplus a}
}}
{{eqn | r = a \oplus \paren {a \oplus a} - a \oplus \paren {b \oplus a} - b \oplus \paren {a \oplus a} + b \oplus \paren {b \oplus a}
}}
{{eqn | l = \paren {\paren {a - b} \oplus \paren {a - b} } \oplus a
      | r = \paren {a \oplus a} \oplus a - \paren {a \oplus b} \oplus a - \paren {b \oplus a} \oplus a + \paren {b \oplus b} \oplus a
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = \sqbrk {a - b, a - b, a}
}}
{{eqn | r = \sqbrk {a, a, a} - \sqbrk {a, b, a} - \sqbrk {b, a, a} + \sqbrk {b, b, a}
      | c = Subtract the two expressions
}}
{{eqn | r = \sqbrk {a, b, a}
}}
{{end-eqn}}
{{explain|This suffices, but why it does could do with explanation (although trivial). Also, where do I use that $A$ isn't Boolean? Maybe better use talk page}}
{{qed}}
{{Namedfor|Emil Artin|cat = Artin E}}
Theorem: Real Numbers form Algebra

The set of real numbers $\R$ forms an algebra over the field of real numbers.
This algebra is:
:$(1): \quad$ An associative algebra.
:$(2): \quad$ A commutative algebra.
:$(3): \quad$ A normed division algebra.
:$(4): \quad$ A nicely normed $*$-algebra whose $*$ operator is the identity mapping.
:$(5): \quad$ A real $*$-algebra.

Proof:
=== Construction of Algebra ===
From Real Numbers form Field, $\struct {\R, +, \times}$ is a field.
Let this be expressed as $\struct {\R, +_\R, \times_\R}$ in order to call attention to the precise scope of the operators.
From Real Numbers form Vector Space, we have that $\struct {\R^1, +, \cdot}_\R$ is a vector space, where:
:the field is $\struct {\R, +_\R, \times_\R}$
:the abelian group is $\struct {\R, +_G}$ where $+_G$ is real addition.
In Real Numbers form Vector Space, it is established that elements of $\struct {\R^1, +, \cdot}_\R$ are in fact just real numbers.
So, let $\times$ be the binary operation on $\struct {\R^1, +, \cdot}_\R$ defined as:
:$\forall x, y \in \struct {\R^1, +, \cdot}_\R: x \times y = x \times_\R y$
where $\times_\R$ is real multiplication.
Theorem: Real Numbers form Vector Space

The set of real numbers $\R$, with the operations of addition and multiplication, forms a vector space.

Proof:
Let the field of real numbers be denoted $\struct {\R, +, \times}$.
From Real Vector Space is Vector Space, we have that $\struct {\R^n, +, \cdot}$ is a vector space, where:
:$\mathbf a + \mathbf b = \tuple {a_1 + b_1, a_2 + b_2, \ldots, a_n + b_n}$
:$\lambda \cdot \mathbf a = \tuple {\lambda \times a_1, \lambda \times a_2, \ldots, \lambda \times a_n}$
where:
:$\mathbf a, \mathbf b \in \R^n$
:$\lambda \in \R$
:$\mathbf a = \tuple {a_1, a_2, \ldots, a_n}$
:$\mathbf b = \tuple {b_1, b_2, \ldots, b_n}$
When $n = 1$, the vector space degenerates to:
:$\mathbf a + \mathbf b = \tuple {a + b}$
:$\lambda \cdot \mathbf a = \tuple {\lambda \times a}$
where:
:$\mathbf a, \mathbf b \in \R$
:$\lambda \in \R$
:$\mathbf a = \tuple a$
:$\mathbf b = \tuple b$
Thus it can be seen that the vector space $\struct {\R^1, +, \cdot}$ is identical with the field of real numbers denoted by $\struct {\R, +, \times}$.
{{qed}}
Theorem: Complex Numbers form Algebra

The set of complex numbers $\C$ forms an algebra over the field of real numbers.
This algebra is:
:$(1): \quad$ An associative algebra.
:$(2): \quad$ A commutative algebra.
:$(3): \quad$ A normed division algebra.
:$(4): \quad$ A nicely normed $*$-algebra.
However, $\C$ is not a real $*$-algebra.

Proof:
The complex numbers $\C$ are formed by the Cayley-Dickson Construction from the real numbers $\R$.
From Real Numbers form Algebra, we have that $\R$ forms:
:$(1): \quad$ An associative algebra.
:$(2): \quad$ A commutative algebra.
:$(3): \quad$ A normed division algebra.
:$(4): \quad$ A nicely normed $*$-algebra whose $*$ operator is the identity mapping.
:$(5): \quad$ A real $*$-algebra.
From Cayley-Dickson Construction forms Star-Algebra, $\C$ is a $*$-algebra.
From Cayley-Dickson Construction from Nicely Normed Algebra is Nicely Normed, $\C$ is a nicely normed $*$-algebra.
From Cayley-Dickson Construction from Real Star-Algebra is Commutative, $\C$ is a commutative algebra.
From Cayley-Dickson Construction from Commutative Associative Algebra is Associative, $\C$ is an associative algebra.
However, from Algebra from Cayley-Dickson Construction is not Real Star-Algebra, $\C$ is not a real $*$-algebra.
Theorem: Characterization of Class Membership

Let $A$ and $B$ be classes.
Then:
:$\forall A, B: \paren {A \in B \iff \exists x: \paren {A = x \land x \in B} }$
where $x$ is specifically a set.

Proof:
Let $V$ denote the universal class.
By Class is Subclass of Universal Class, $A \subseteq V$ and $B \subseteq V$.
By definition of universal class, every element of $V$ is a set.
Hence every element of $B$ is a set.
So if $A \in B$, then it follows that $A$ is itself a set.
Hence the result.
{{qed}}
Theorem: Equality implies Substitution

Let $\map P x$ denote a Well-Formed Formula which contains $x$ as a free variable.
Then the following are tautologies:
:$\forall x: \paren {\map P x \iff \exists y: \paren {y = x \land \map P y} }$
:$\forall x: \paren {\map P x \iff \forall y: \paren {y = x \implies \map P y} }$
Note that when $y$ is substituted for $x$ in either formula, it is false in general; compare Confusion of Bound Variables.

Proof:
{{questionable|Inelegant and unclear to the point of soliciting purging}}
By Universal Affirmative implies Particular Affirmative iff First Predicate is not Vacuous:
:$\paren {\exists y: y = x \land \forall y: \paren {y = x \implies \map P x} } \implies \exists y: \paren {y = x \land \map P x}$
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = x = x
      | c = Equality is Reflexive
}}
{{eqn | o = \leadsto
      | r = \exists y: y = x
      | c = Existential Generalisation
}}
{{eqn | o = \leadsto
      | r = \paren {\forall y: \paren {y = x \implies \map P x} \implies \exists y: \paren {y = x \land \map P x} }
      | c = Modus Ponendo Ponens
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \paren { y = x \land \map P y}
      | o = \implies
      | r = \map P x
      | c = Substitutivity of Equality
}}
{{eqn | n = 1
      | ll= \leadsto
      | q = \exists y
      | l = \paren {y = x \land \map P y}
      | o = \implies
      | r = \map P x
      | c = Universal Generalisation
}}
{{eqn | n = 2
      | ll= \leadsto
      | q = \forall y
      | l = \paren {y = x \implies \map P y}
      | o = \implies
      | r = \map P x
      | c = Hypothetical Syllogism with first lemma
}}
{{end-eqn}}
{{wtd|Theorem needs to connect the first implications.  Universal Generalisation is not sufficient.}}
{{qed|lemma}}
Similarly:
{{begin-eqn}}
{{eqn | o =
      | r = \map P x
}}
{{eqn | ll= \leadsto
      | l = y = x
      | o = \implies
      | r = \map P y
      | c = Substitutivity of Equality
}}
{{eqn | n = 3
      | ll= \leadsto
      | q = \forall y
      | l = y = x
      | o = \implies
      | r = \map P y
      | c = Universal Generalisation
}}
{{eqn | n = 4
      | ll= \leadsto
      | q = \exists y
      | l = y = x
      | o = \land
      | r = \map P y
      | c = First lemma
}}
{{end-eqn}}
The above two statements comprise the other direction of the biconditional assertions.
Together, $(1)$, $(2)$, $(3)$, and $(4)$ prove the two assertions.
{{qed}}
Theorem: Fundamental Law of Universal Class

:$\forall x: x \in \Bbb U$
where:
:$\Bbb U$ denotes the universal class
:$x$ denotes a set.

Proof:
From the definition of the universal class:
:$\Bbb U = \set {x: x = x}$
From this, it follows immediately that:
:$\forall x: \paren {x \in \Bbb U \iff x = x}$
From Equality is Reflexive, $x = x$ is a tautology.
Thus the asserted statement is also tautologous.
{{qed}}
Theorem: Cayley-Dickson Construction forms Star-Algebra

Let $A = \struct {A_F, \oplus}$ be a $*$-algebra.
Let $A' = \struct {A'_F, \oplus'} = \struct {A, \oplus}^2$ be the algebra formed from $A$ by the Cayley-Dickson construction.
Then $A'$ is also a $*$-algebra.

Proof:
=== Bilinearity of $\oplus'$ ===
First we need to show that $\oplus'$ is bilinear.
$(1): \quad$ Let $\tuple {a_1, b_1}, \tuple {a_2, b_2}, \tuple {c, d} \in A'$.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {\tuple {a_1, b_1} + \tuple {a_2, b_2} } \oplus' \tuple {c, d}
      | c = 
}}
{{eqn | r = \tuple {a_1 + a_2, b_1 + b_2} \oplus' \tuple {c, d}
      | c = 
}}
{{eqn | r = \tuple {\paren {a_1 + a_2} \oplus c - d \oplus \paren {b_1 + b_2}^*, \paren {a_1 + a_2}^* \oplus d + c \oplus \paren {b_1 + b_2} }
      | c = 
}}
{{eqn | r = \tuple {a_1 \oplus c + a_2 \oplus c - d \oplus b_1^* - d \oplus b_2^*, a_1^* \oplus d + a_2^* \oplus d + c \oplus b_1 + c \oplus b_2}
      | c = as $\oplus$ is bilinear
}}
{{eqn | r = \tuple {a_1 \oplus c - d \oplus b_1^*, a_1^* \oplus d + c \oplus b_1} + \tuple {a_2 \oplus c - d \oplus b_2^*, a_2^* \oplus d + c \oplus b_2}
      | c = 
}}
{{eqn | r = \paren {\tuple {a_1, b_1} \oplus' \tuple {c, d} } + \paren {\tuple {a_2, b_2} \oplus' \tuple {c, d} }
      | c = 
}}
{{end-eqn}}
Similarly (and equally tediously) we can show that:
:$\tuple {c, d} \oplus' \paren {\tuple {a_1, b_1} + \tuple {a_2, b_2}} = \paren {\tuple {c, d} \oplus' \tuple {a_1, b_1}} + \paren {\tuple {c, d} \oplus' \tuple {a_2, b_2}}$
$(2): \quad$ Let $\tuple {a, b}, \tuple {c, d} \in A'$ and $\alpha, \beta \in \R$.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {\alpha \tuple {a, b} } \oplus' \tuple {c, d}
      | c = 
}}
{{eqn | r = \tuple {\alpha a, \alpha b} \oplus' \tuple {c, d}
      | c = as $\oplus$ is bilinear
}}
{{eqn | r = \tuple {\alpha a \oplus c - d \oplus \alpha b^*, \alpha a^* \oplus d + c \oplus \alpha b}
      | c = 
}}
{{eqn | r = \alpha \tuple {a \oplus c - d \oplus b^*, a^* \oplus d + c \oplus b}
      | c = as $\oplus$ is bilinear
}}
{{eqn | r = \alpha \tuple {a, b} \oplus' \tuple {c, d}
      | c = 
}}
{{end-eqn}}
Similarly:
:$\tuple {a, b} \oplus' \paren {\tuple {c, d} \beta} = \tuple {a, b} \oplus' \tuple {c, d} \beta$
So $\oplus'$ has been shown to be a bilinear mapping.
Theorem: Empty Set is Small

:$\O \in U$
where $U$ is the universal class.

Proof:
{{begin-eqn}}
{{eqn | l = \exists x
      | o = :
      | r = \forall y: \paren {\neg \paren {y \in x} }
      | c = {{axiom-link|the Empty Set|Set Theory}}
}}
{{eqn | ll= \leadsto
      | l = \exists x
      | o = :
      | r = \forall y: \paren {y \in x \iff y \ne y}
      | c = Equality is Reflexive
}}
{{eqn | ll= \leadsto
      | l = \exists x
      | o = :
      | r = x = \set {y: y \ne y}
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = A \in U
      | o = \iff
      | r = \exists x: \paren {x = A \land x \in U}
      | c = Characterization of Class Membership
}}
{{eqn | l = x
      | o = \in
      | r = U
      | c = Fundamental Law of Universal Class
}}
{{eqn | ll= \leadsto
      | l = A \in U
      | o = \iff
      | r = \exists x: x = A
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Hence:
{{begin-eqn}}
{{eqn | l = \set {y: y \ne y}
      | o = \in
      | r = U
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \O
      | o = \in
      | r = U
      | c = {{Defof|Empty Set}}
}}
{{end-eqn}}
{{qed}}
Theorem: Algebra from Cayley-Dickson Construction is not Real Star-Algebra

Let $A$ be a $*$-algebra.
Let $A'$ be constructed from $A$ using the Cayley-Dickson construction.
Then $A'$ is not a real $*$-algebra.

Proof:
Let the conjugation operator on $A$ be $*$.
{{AimForCont}} $A'$ is a real $*$-algebra whose conjugation operator is $*'$.
Then by definition:
:$\forall a \in A': {a^*}' = a$
Let $a = \tuple {x, y} \in A'$.
Then by definition of the Cayley-Dickson construction:
:$x, y \in A$
By definition of the conjugation operator:
:${\tuple {x, y}^*}' = \tuple {x^*, -y}$
So for ${a^*}' = a$ it must be that $x = x^*$ and $y = -y$ from definition of Equality of Ordered Pairs.
That is, $y = 0$.
But $A'$ is a $*$-algebra, which is by definition a unitary division algebra.
So $\exists y \in A: y = 1 \ne 0$.
From that contradiction, it follows that $A'$ can not be a real $*$-algebra.
{{qed}}
Theorem: Cayley-Dickson Construction from Real Star-Algebra is Commutative

Let $A = \struct {A_F, \oplus}$ be a $*$-algebra.
Let $A' = \struct {A_F, \oplus'}$ be constructed from $A$ using the Cayley-Dickson construction.
Then $A$ is a real star-algebra {{iff}} $A'$ is a commutative algebra.

Proof:
Let the conjugation operator on $A$ be $*$.
Let $\tuple {a, b}, \tuple {c, d} \in A'$.
Let $A$ be a real star-algebra.
{{begin-eqn}}
{{eqn | l = \tuple {a, b} \oplus' \tuple {c, d}
      | r = \tuple {a \oplus c - d \oplus b^*, a^* \oplus d + c \oplus b}
      | c = 
}}
{{eqn | r = \tuple {a \oplus c - d \oplus b^*, a^* \oplus d + c \oplus b}
      | c = 
}}
{{eqn | r = \tuple {a \oplus c - d \oplus b, a \oplus d + c \oplus b}
      | c = {{Defof|Real Star-Algebra}}: $a = a^*$ and $b = b^*$
}}
{{eqn | r = \tuple {c \oplus a - b \oplus d, c \oplus b + a \oplus d}
      | c = Real Star-Algebra is Commutative, Real Addition is Commutative
}}
{{eqn | r = \tuple {c \oplus a - b \oplus d^*, c^* \oplus b + a \oplus d}
      | c = {{Defof|Real Star-Algebra}}: $d = d^*$ and $c = c^*$
}}
{{eqn | r = \tuple {c, d} \oplus' \tuple {a, b}
      | c = 
}}
{{end-eqn}}
So $A'$ is a commutative algebra.
{{qed|lemma}}
Let $A'$ be a commutative algebra.
By picking apart the above equations, it is clear that for $A'$ to be a commutative algebra it is necessary for $A$ to be both real and commutative.
Hence the result.
{{qed}}
Theorem: Cayley-Dickson Construction from Commutative Associative Algebra is Associative

Let $A = \struct {A_F, \oplus}$ be a $*$-algebra.
Let $A' = \struct {A_F, \oplus'}$ be constructed from $A$ using the Cayley-Dickson construction.
Then:
:$A'$ is an associative algebra
{{iff}}:
:$A$ is both a commutative algebra and an associative algebra.

Proof:
Let the conjugation operator on $A$ be $*$.
Let $\tuple {a, b}, \tuple {c, d}, \tuple {e, f} \in A'$.
In order to streamline notation, let $\oplus$ and $\oplus'$ both be denoted by product notation:
:$a \oplus b =: a b$
:$x \oplus' y =: x y$
The context will make it clear which is meant.
Suppose $A$ is commutative and associative.
Then:
{{begin-eqn}}
{{eqn | r = \paren {\tuple {a, b} \tuple {c, d} } \tuple {e, f}
      | o = 
      | c = 
}}
{{eqn | r = \tuple {a c - d b^*, a^* d + c b} \tuple {e, f}
      | c = {{Defof|Cayley-Dickson Construction}} for $\oplus$ 
}}
{{eqn | r = \tuple {\paren {a c - d b^*} e - f \paren {a^* d + c b}^*, \paren {a c - d b^*}^* f + e \paren {a^* d + c b} }
      | c = 
}}
{{eqn | r = \tuple {\paren {a c} e - \paren {d b^*} e - f \paren {a^* d}^* - f \paren {c b}^*, \paren {a c}^* f - \paren {d b^*}^* f + e \paren {a^* d} + e \paren {c b} }
      | c = 
}}
{{eqn | r = \tuple {\paren {a c} e - \paren {d b^*} e - f \paren {d^* a} - f \paren {b^* c^*}, \paren {c^* a^*} f - \paren {b d^*} f + e \paren {a^* d} + e \paren {c b} }
      | c = {{Defof|Conjugation on Algebra}}
}}
{{eqn | r = \tuple {a \paren {c e} - a \paren {f d^*} - \paren {c^* f} b^* - \paren {e d} b^*, a^* \paren {c^* f} + a^* \paren {e d} + \paren {c e} b - \paren {f d^*} b}
      | c = $A$ is commutative and associative
}}
{{eqn | r = \tuple {a \paren {c e - f d^*} - \paren {c^* f + e d} b^*, a^* \paren {c^* f + e d} + \paren {c e - f d^*} b}
      | c = 
}}
{{eqn | r = \tuple {a, b} \tuple {c e - f d^*, c^* f + e d}
      | c = 
}}
{{eqn | r = \tuple {a, b} \paren {\tuple {c, d} \tuple {e, f} }
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Now suppose $A'$ is an associative algebra.
By picking apart the above series of equations, it is clear that $A$ has to be both commutative and associative in order to assure the associativity of $A'$.
{{qed}}