avewright/proofwiki-math huggingface dataset:
Theorem: Not Preceding implies Exists Completely Irreducible Element in Algebraic Lattice

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.
Let $x, y \in S$ such that
:$y \npreceq x$
Then
:$\exists p \in S: p$ is completely irreducible $\mathop \land x \preceq p \land y \npreceq p$

Proof:
By definition of algebraic:
:$\forall z \in S: z^\ll$ is directed
and
:$L$ satisfies the axiom of approximation.
By Axiom of Approximation in Up-Complete Semilattice:
:$\exists k \in S: k \ll y \land k \npreceq x$
By Algebraic iff Continuous and For Every Way Below Exists Compact Between:
:$\exists z \in \map K L: k \preceq z \preceq y$
By definition of transitivity:
:$z \npreceq x$
By definition of upper closure of element:
:$x \notin z^\succeq$
By definition of difference:
:$x \in S \setminus z^\succeq$
By definition of relative complement:
:$x \in \relcomp S {z^\succeq}$
By definition of compact subset:
:$z$ is a compact element.
By Upper Closure of Element is Way Below Open Filter iff Element is Compact:
:$z^\succeq$ is a way below open filter on $L$.
By Upper Way Below Open Subset Complement is Non Empty implies There Exists Maximal Element of Complement:
:$\exists p \in S: x \preceq p \land p = \max \relcomp S {z^\succeq}$
Thus by Maximal implies Completely Irreducible:
:$p$ is completely irreducible.
Thus:
:$x \preceq p$
{{AimForCont}}:
:$y \preceq p$
By definition of transitivity:
:$z \preceq p$
By definition of maximum element:
:$p \in \relcomp S {z^\succeq}$
By definition of relative complement:
:$p \notin z^\succeq$
Thus this contradicts $z \preceq p$ by definition of upper closure of element.
{{qed}}
Theorem: Set of All Completely Irreducible Elements is Smallest Order Generating

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.
Then $\map {\operatorname {Irr} } L$ is order generating and
:$\forall X \subseteq S: X$ is order generating $\implies \map {\operatorname {Irr} } L \subseteq X$
where $\map {\operatorname {Irr} } L$ denotes the set of all completely irreducible elements of $L$.

Proof:
By Not Preceding implies Exists Completely Irreducible Element in Algebraic Lattice:
:$\forall x, y \in S: y \npreceq x \implies \exists p \in \map {\operatorname {Irr} } L: p \preceq x \land p \npreceq y$
Thus by Order Generating iff Not Preceding implies There Exists Element Preceding and Not Preceding:
:$\map {\operatorname {Irr} } L$ is order generating.
Let $X \subseteq S$ such that
:$X$ is order generating.
Let $x \in \map {\operatorname {Irr} } L$.
By definition of $\operatorname {Irr}$:
:$x$ is completely irreducible.
Thus by Order Generating Subset Includes Completely Irreducible Elements:
:$x \in X$
{{qed}}
Theorem: Completely Irreducible Element equals Infimum of Subset implies Element Belongs to Subset

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X \subseteq S$, $p \in S$ such that
:$p$ is completely irreducible and $p = \inf X$
Then $p \in X$

Proof:
{{AimForCont}}
:$p \notin X$
By Completely Irreducible Element iff Exists Element that Strictly Succeeds First Element:
:$\exists q \in S: p \prec q \land \left({\forall s \in S: p \prec s \implies q \preceq s}\right) \land p^\succeq = \left\{ {p}\right\} \cup q^\succeq$
where $p^\succeq$ denotes the upper closure of $p$.
We will prove that
:$q$ is lower bound for $X$
Let $x \in X$.
By definitions of infimum and lower bound
:$p \preceq x$
By assumption:
:$x \ne p$
By definition of strictly precede:
:$p \prec x$
Thus by step condition:
:$q \preceq x$
{{qed|lemma}}
By definition of strictly precede:
:$p \preceq q$
We will prove that
:$\forall b \in S: b$ is lower bound for $X \implies b \preceq q$
Let $b \in S$ such that
:$b$ is lower bound for $X$.
By definition of infimum:
:$b \preceq p$
Thus by definition of transitivity:
:$b \preceq q$
{{qed|lemma}}
By definition of infimum:
:$q = \inf X = p$
Thus this contradicts $p \ne q$ by definition of strictly precede.
{{qed}}
Theorem: Preimage of Lower Section under Increasing Mapping is Lower

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be preordered sets.
Let $f: S \to T$ be an increasing mapping.
Let $X \subseteq T$ be a lower section of $T$.
Then:
:$f^{-1} \sqbrk X$ is lower
where $f^{-1} \sqbrk X$ denotes the preimage of $X$ under $f$.

Proof:
Let $x \in f^{-1} \sqbrk X$, $y \in S$ such that $y \preceq x$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \preceq
      | r = x
}}
{{eqn | ll= \leadsto
      | l = \map f y
      | o = \precsim
      | r = \map f x
      | c = {{Defof|Increasing Mapping}}
}}
{{eqn | l = x
      | o = \in
      | r = f^{-1} \sqbrk X
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | o = \in
      | r = X
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map f y
      | o = \in
      | r = X
      | c = {{Defof|Lower Section}}
}}
{{eqn | ll= \leadsto
      | l = \map f y
      | o = \in
      | r = X
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{end-eqn}}
{{qed}}
Theorem: Preimage of Upper Section under Increasing Mapping is Upper

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be preordered sets.
Let $f: S \to T$ be an increasing mapping.
Let $X \subseteq T$ be a upper subset of $T$.
Then $f^{-1} \sqbrk X$ is upper
where $f^{-1} \sqbrk X$ denotes the preimage of $X$ under $f$.

Proof:
Let $x \in f^{-1} \sqbrk X$, $y \in S$ such that
:$x \preceq y$
By definition of increasing mapping:
:$\map f x \precsim \map f y$
By definition of preimage of set:
:$\map f x \in X$
By definition of upper section:
:$\map f y \in X$
Thus by definition of preimage of subset:
:$y \in f^{-1} \sqbrk X$
{{qed}}
Theorem: Continuous implies Increasing in Scott Topological Lattices

Let $T_1 = \struct {S_1, \preceq_1, \tau_1}$ and $T_2 = \struct {S_2, \preceq_2, \tau_2}$ be up-complete topological lattices with Scott topologies.
Let $f: S_1 \to S_2$ be a continuous mapping.
Then $f$ is an increasing mapping.

Proof:
Let $x, y \in S_1$ such that
:$x \preceq_1 y$
{{AimForCont}} that
:$\map f x \npreceq_2 \map f y$
By definition of lower closure of element:
:$\map f x \notin \paren {\map f y}^\preceq$
By definition of relative complement:
:$\map f x \in \relcomp {S_2} {\paren {\map f y}^\preceq}$
By definition of reflexivity:
:$\map f y \preceq_2 \map f y$
By definition of lower closure of element:
:$\map f y \in \paren {\map f y}^{\preceq_2}$
By Closure of Singleton is Lower Closure of Element in Scott Topological Lattice:
:$\set {\map f y}^- = \paren {\map f y}^{\preceq_2}$
By definition of closure:
:$\paren {\map f y}^{\preceq_2}$ is a closed set.
By definition of closed set:
:$\relcomp {S_2} {\paren {\map f y}^{\preceq_2} }$ is a open set.
By definition of continuous:
:$f^{-1} \sqbrk {\relcomp {S_2} {\paren {\map f y}^{\preceq_2} } }$ is an open set.
By definition of Definition:Scott Topology:
:$f^{-1} \sqbrk {\relcomp {S_2} {\paren {\map f y}^{\preceq_2} } }$ is an upper section.
By definition of preimage of set:
:$x \in f^{-1} \sqbrk {\relcomp {S_2} {\paren {\map f y}^{\preceq_2} } }$
By definition of upper section:
:$y \in f^{-1} \sqbrk {\relcomp {S_2} {\paren {\map f y}^{\preceq_2} } }$
By definition of preimage of set:
:$\map f y \in \relcomp {S_2} {\paren {\map f y}^{\preceq_2} }$
Thus this contradicts $\map f y \in \paren {\map f y}^{\preceq_2}$
{{qed}}
Theorem: Directed Suprema Preserving Mapping at Element is Supremum

Let $\struct {S, \vee, \wedge, \preceq}$ and $\struct {T, \vee_2, \wedge_2, \precsim}$ be bounded below continuous lattices.
Let $f: S \to T$ be a mapping such that
:$f$ preserves directed suprema.
Let $x \in S$.
Then:
:$\map f x = \sup \set {\map f w: w \in S \land w \ll x}$

Proof:
By definition of continuous:
:$x^\ll$ is directed
and
:$\struct {S, \vee, \wedge, \preceq}$ is up-complete
and
:$\struct {S, \vee, \wedge, \preceq}$ satisfies the {{Axiom-link|Approximation}}.
By definition of mapping preserves directed suprema:
:$f$ preserves the supremum of $x^\ll$.
By definition of up-complete:
:$x^\ll$ admits a supremum.
Thus
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f {\map \sup {x^\ll} }
      | c = {{Axiom-link|Approximation}}
}}
{{eqn | r = \map \sup {f \sqbrk {x^\ll} }
      | c = {{Defof|Mapping Preserves Supremum/Subset|Mapping Preserves Supremum: Subset}}
}}
{{eqn | r = \map \sup {f \sqbrk {\set {w \in S: w \ll x} } }
      | c = {{Defof|Way Below Closure}}
}}
{{eqn | r = \sup \set {\map f w: w \in S \land w \ll x}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{end-eqn}}
{{qed}}
Theorem: Preceding implies Way Below Closure is Subset of Way Below Closure

Let $\struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
:$x \preceq y$
Then $x^\ll \subseteq y^\ll$
where $x^\ll$ denotes the way below closure of $x$.

Proof:
Let $z \in x^\ll$.
By definition of way below closure:
:$z \ll x$
By Preceding and Way Below implies Way Below and definition of reflexivity:
:$z \ll y$
Thus by definition of way below closure:
:$z \in y^\ll$
{{qed}}
Theorem: Mapping at Element is Supremum implies Mapping is Increasing

Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $\struct {T, \vee_2, \wedge_2, \precsim}$ be a complete lattice.
Let $f: S \to T$ be a mapping such that:
:$\forall x \in S: \map f x = \sup \set {\map f w: w \in S \land w \ll x}$
Then $f$ is an increasing mapping.

Proof:
Let $x, y \in S$ such that:
:$x \preceq y$
By Preceding implies Way Below Closure is Subset of Way Below Closure:
:$x^\ll \subseteq y^\ll$
By definitions of image of set and way below closure:
:$f \sqbrk {x^\ll} = \set {\map f w: w \in S \land w \ll x}$
and
:$f \sqbrk {y^\ll} = \set {\map f w: w \in S \land w \ll y}$
where $f \sqbrk {x^\ll}$ denotes the image of $x^\ll$ under $f$.
By Image of Subset under Mapping is Subset of Image:
:$f \sqbrk {x^\ll} \subseteq f \sqbrk {y^\ll}$
Thus
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map \sup {f \sqbrk {x^\ll} }
      | c = {{hypothesis}}
}}
{{eqn | o = \precsim
      | r = \map \sup {f \sqbrk {y^\ll} }
      | c = Supremum of Subset
}}
{{eqn | r = \map f y
      | c = {{hypothesis}}
}}
{{end-eqn}}
{{qed}}
Theorem: Semiperfect Number is not Deficient

Let $n \in \Z_{>0}$ be a semiperfect number.
Then $n$ is not deficient.

Proof:
Let $n$ be semiperfect.
Then by definition, the sum of the aliquot parts of $n$ is not less than $n$.
The result follows by definition of deficient.
{{qed}}
Category:Semiperfect Numbers
Category:Deficient Numbers
hc85iiuau9aa2yjhlxau95ge4lnn53b
Theorem: Perfect Number is Primitive Semiperfect

Let $n \in \Z_{>0}$ be a perfect number.
Then $n$ is also a primitive semiperfect number.

Proof:
Let $n$ be perfect.
From Divisor of Perfect Number is Deficient, all divisors of $n$ are deficient.
But from Semiperfect Number is not Deficient, it follows that the divisors of $n$ cannot be semiperfect.
Hence the result, by definition of primitive semiperfect number.
{{qed}}
Category:Perfect Numbers
Category:Primitive Semiperfect Numbers
m2rwpvgnzeynsz9mte4tobkvu5pwm2i
Theorem: Mapping at Element is Supremum implies Way Below iff There Exists Element that Way Below and Way Below

Let $\left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Let $\left({T, \vee_2, \wedge_2, \precsim}\right)$ be a continuous complete lattice.
Let $f: S \to T$ be a mapping such that
:$\forall x \in S: f\left({x}\right) = \sup \left\{ {f\left({w}\right): w \in S \land w \ll x}\right\}$
Let $x \in S, y \in T$.
Then
:$y \ll f\left({x}\right) \iff \exists w \in S: w \ll x \land y \ll f\left({w}\right)$

Proof:
By Mapping at Element is Supremum implies Mapping is Increasing:
:$f$ is an increasing mapping.
Theorem: Subset and Image Admit Suprema and Mapping is Increasing implies Supremum of Image Precedes Mapping at Supremum

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a increasing mapping.
Let $D \subseteq S$ such that
:$D$ admits a supremum in $S$ and $f \sqbrk D$ admits a supremum in $T$.
Then:
:$\map \sup {f \sqbrk D} \precsim \map f {\sup D}$

Proof:
By definition of supremum:
:$\sup D$ is upper bound for $D$.
By Increasing Mapping Preserves Upper Bounds:
:$\map f {\sup D}$ is upper bound for $f \sqbrk D$.
Thus by definition of supremum:
:$\map \sup {f \sqbrk D} \precsim \map f {\sup D}$
{{qed}}
Theorem: Characteristic Subgroup of Normal Subgroup is Normal

Let $G$ be a group.
Let $N\leq G$ be normal.
Let $H\leq N$ be characteristic.
Then $H$ is normal in $G$.

Proof:
Let $g \in G$.
Because $N$ is normal, conjugation by $g$ is an automorphism of $N$.
Because $H$ is characteristic in $N$, $g H g^{-1} = H$.
Thus $H$ is normal in $G$.
{{qed}}
Theorem: Center is Characteristic Subgroup

Let $G$ be a group.
Then its center $\map Z G$ is characteristic in $G$.

Proof:
By Identity Mapping is Group Automorphism, there exists at least one automorphism of $G$.
Let $\phi$ be an automorphism of $G$.
Let $x \in \map Z G, y \in G$.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi x y
      | r = \map \phi x \map \phi {\map {\phi^{-1} } y}
      | c = automorphisms are bijections
}}
{{eqn | r = \map \phi {x \map {\phi^{-1} } y}
      | c = {{Defof|Group Homomorphism}}
}}
{{eqn | r = \map \phi {\map {\phi^{-1} } y x}
      | c = {{Defof|Center of Group}}
}}
{{eqn | r = \map \phi {\map {\phi^{-1} } y} \map \phi x
      | c = {{Defof|Group Homomorphism}}
}}
{{eqn | r = y \map \phi x
}}
{{end-eqn}}
Hence $\map \phi x \in \map Z G$.
So we have $\phi \sqbrk {\map Z G} \subseteq \map Z G$.
Since $\phi^{-1}$ is also an automorphism:
:$\phi^{-1} \sqbrk {\map Z G} \subseteq \map Z G$
Since $\phi$ is a bijection:
:$\map Z G = \phi \sqbrk {\phi^{-1} \sqbrk {\map Z G}} \subseteq \phi \sqbrk {\map Z G}$
Therefore we conclude that $\phi \sqbrk {\map Z G} = \map Z G$.
Hence $\map Z G$ is characteristic in $G$.
{{qed}}
Category:Characteristic Subgroups
Category:Centers of Groups
6ozriw39x5rleco2kb60gwi2ohqnl6g
Theorem: Semidirect Product of Groups is Group

Let $H$ and $N$ be groups.
Let $\Aut N$ denote the automorphism group of $N$.
Let $\phi : H\to \Aut N$ be a group homomorphism, that is, let $H$ act on $N$.
Let $N \rtimes_\phi H$ be the (outer)semidirect product of $N$ and $H$ with respect to $\phi$, that is:
:$N \rtimes_\phi H = (N \times H, \circ)$ where
:$(n_1, h_1) \circ (n_2, h_2) = (n_1\cdot \phi(h_1)(n_2), h_1\cdot h_2)$
Then $N\rtimes_\phi H$ is a group.

Proof:
=== Associativity ===
Let $(n_1,h_1),(n_2,h_2),(n_3,h_3)\in N\times H$. Then
{{begin-eqn}}
{{eqn | l = ((n_1, h_1) \circ (n_2, h_2)) \circ (n_3, h_3)
      | r = ((n_1\cdot \phi_{h_1}(n_2), h_1\cdot h_2)) \circ (n_3,h_3)
}}
{{eqn | l = 
      | r = (n_1\cdot \phi_{h_1}(n_2) \cdot \phi_{h_1h_2}(n_3), h_1\cdot h_2\cdot h_3)
}}
{{eqn | l = 
      | r = (n_1\cdot \phi_{h_1}(n_2) \cdot \phi_{h_1}(\phi_{h_2}(n_3)), h_1\cdot h_2\cdot h_3)
      | c = {{Defof|Group Action}}
}}
{{eqn | l = 
      | r = (n_1\cdot \phi_{h_1}(n_2\phi_{h_2}(n_3)), h_1\cdot h_2\cdot h_3)
      | c = $H$ acts by automorphisms
}}
{{eqn | l = 
      | r = (n_1, h_1) \circ ((n_2, h_2) \circ (n_3, h_3))
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Inverse of Element in Semidirect Product

Let $N$ and $H$ be groups.
Let $H$ act by automorphisms on $N$ via $\phi$.
Let $N \rtimes_\phi H$ be the corresponding (outer) semidirect product.
Let $\tuple {n, h} \in N \rtimes_\phi H$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {n, h}^{-1}
      | r = \tuple {\map {\phi_{h^{-1} } } {n^{-1} }, h^{-1} }
      | c = 
}}
{{eqn | r = \tuple {\paren {\map {\phi_{h^{-1} } } n}^{-1}, h^{-1} }
      | c = 
}}
{{eqn | r = \tuple {\map { {\phi_h}^{-1} } {n^{-1} }, h^{-1} }
      | c = 
}}
{{eqn | r = \tuple {\paren {\map { {\phi_h}^{-1} } n}^{-1}, h^{-1} }
      | c = 
}}
{{end-eqn}}

Proof:
Follows from Semidirect Product of Groups is Group.
The alternatives follow from the fact that $H$ acts by automorphisms.
{{qed}}
{{finish|Expand the proof by demonstrating how it works.}}
Category:Group Theory
Category:Semidirect Products
o8rs9bgvrqwle1hig2ok7q7zmyknuue
Theorem: Semidirect Product with Trivial Action is Direct Product

Let $H$ and $N$ be groups.
Let $\Aut N$ denote the automorphism group of $N$.
Let $\phi: H \to \Aut N$ be defined as:
:$\forall h \in H: \map \phi h = I_N$ for all $h \in H$
where $I_N$ denotes the identity mapping on $N$.
Let $N \rtimes_\phi H$ be the corresponding semidirect product.
Then $N \rtimes_\phi H$ is the direct product of $N$ and $H$.

Proof:
Pick arbitrary $\tuple {n_1, h_1}, \tuple {n_2, h_2} \in N \rtimes_\phi H$.
{{begin-eqn}}
{{eqn | l = \tuple {n_1, h_1} \tuple {n_2, h_2}
      | r = \tuple {n_1 \cdot \map \phi {h_1} \paren {n_2}, h_1 h_2}
      | c = {{Defof|Outer Semidirect Product}}
}}
{{eqn | r = \tuple {n_1 \cdot \map {I_N} {n_2}, h_1 h_2}
      | c = Definition of $\phi$
}}
{{eqn | r = \tuple {n_1 n_2, h_1 h_2}
      | c = 
}}
{{end-eqn}}
which meets the definition of direct product.
{{qed}}
Category:Semidirect Products
o06ysbwlzbnfl9h30wo0y0ed5nwkxi7
Theorem: Semidirect Product is Abelian iff Components are Abelian and Action is Trivial

Let $N$ and $H$ be groups.
Let $H$ act by automorphisms on $N$ via $\phi$.
Let $N \rtimes_\phi H$ be the corresponding (outer) semidirect product.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$N \rtimes_\phi H$ is abelian}}
{{item|(2):|$N$ and $H$ are abelian and $H$ acts trivially}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Let $n \in N$, $h \in H$.
From $\tuple {n, e} \tuple {e, h} = \tuple {e,h} \tuple {n, e}$ we have $n \map {\phi_e} e = e \map {\phi_h} n$.
Thus $H$ acts trivially.
By Semidirect Product with Trivial Action is Direct Product, $N \rtimes_\phi H = N \times H$.
By External Direct Product of Abelian Groups is Abelian Group, $N$ and $H$ are abelian.
{{qed|lemma}}
Theorem: Integers whose Squares end in 444

The sequence of positive integers whose square ends in $444$ begins:
:$38, 462, 538, 962, 1038, 1462, 1538, 1962, 2038, 2462, 2538, 2962, 3038, 3462, \ldots$
{{OEIS|A039685}}

Proof:
{{begin-eqn}}
{{eqn | l = 38^2
      | r = 1444
}}
{{eqn | l = 462^2
      | r = 213 \, 444
}}
{{eqn | l = 538^2
      | r = 289 \, 444
}}
{{eqn | l = 962^2
      | r = 925 \, 444
}}
{{eqn | l = 1038^2
      | r = 1 \, 077 \, 444
}}
{{eqn | l = 1462^2
      | r = 2 \, 137 \, 444
}}
{{eqn | l = 1538^2
      | r = 2 \, 365 \, 444
}}
{{eqn | l = 1962^2
      | r = 3 \, 849 \, 444
}}
{{eqn | l = 2038^2
      | r = 4 \, 153 \, 444
}}
{{eqn | l = 2462^2
      | r = 6 \, 061 \, 444
}}
{{eqn | l = 2538^2
      | r = 6 \, 441 \, 444
}}
{{eqn | l = 2962^2
      | r = 8 \, 773 \, 444
}}
{{eqn | l = 3038^2
      | r = 9 \, 229 \, 444
}}
{{eqn | l = 3462^2
      | r = 11 \, 985 \, 444
}}
{{end-eqn}}
All such $n$ are of the form $500 m + 38$ or $500 m - 38$:
{{begin-eqn}}
{{eqn | l = \paren {500 m + 38}^2
      | r = 250 \, 000 m^2 + 38 \, 000 m + 1444
      | c = 
}}
{{eqn | r = \paren {250 m^2 + 38 m + 1} + 444
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \paren {500 m - 38}^2
      | r = 250 \, 000 m^2 - 38 \, 000 m + 1444
      | c = 
}}
{{eqn | r = \paren {250 m^2 - 38 m + 1} + 444
      | c = 
}}
{{end-eqn}}
and it is seen that all such numbers end in $444$.
Now we show that all such numbers are so expressed.
In Squares Ending in Repeated Digits, we have shown the only numbers with squares ending in $44$ ends in:
:$12, 38, 62, 88$
hence any number with square ending in $444$ must also end in those numbers.
Suppose $\sqbrk {axy}^2 \equiv 444 \pmod {1000}$, where $a < 10$ and $\sqbrk {xy}$ is in the above list.
For $\sqbrk {xy} = 12$:
{{begin-eqn}}
{{eqn | l = 444
      | r = \paren {100 a + 12}^2
      | rr = \pmod {200}
}}
{{eqn | r = 10000 a^2 + 2400 a + 144
      | rr = \pmod {200}
}}
{{eqn | r = 144
      | rr = \pmod {200}
}}
{{end-eqn}}
This is a contradiction.
Similarly for $\sqbrk {xy} = 88$:
{{begin-eqn}}
{{eqn | l = 444
      | r = \paren {100 a + 88}^2
      | rr = \pmod {200}
}}
{{eqn | r = 10000 a^2 + 17600 a + 7744
      | rr = \pmod {200}
}}
{{eqn | r = 144
      | rr = \pmod {200}
}}
{{end-eqn}}
Again, a contradiction.
For $\sqbrk {xy} = 38$:
{{begin-eqn}}
{{eqn | l = 444
      | r = \paren {100 a + 38}^2
      | rr = \pmod {1000}
}}
{{eqn | r = 10000 a^2 + 7600 a + 1444
      | rr = \pmod {1000}
}}
{{eqn | r = 600 a + 444
      | rr = \pmod {1000}
}}
{{end-eqn}}
The solutions to $600 a \equiv 0 \pmod {1000}$ are $a = 0$ or $5$.
Hence:
:$\paren {500 n + 38}^2 \equiv 444 \pmod {1000}$
Similarly, for $\sqbrk {xy} = 62$:
{{begin-eqn}}
{{eqn | l = 444
      | r = \paren {100 a + 62}^2
      | rr = \pmod {1000}
}}
{{eqn | r = 10000 a^2 + 12400 a + 3844
      | rr = \pmod {1000}
}}
{{eqn | r = 400 a + 844
      | rr = \pmod {1000}
}}
{{end-eqn}}
The solutions to $400 a + 400 \equiv 0 \pmod {1000}$ are $a = 4$ or $9$.
Hence:
:$\paren {500 n + 462}^2 \equiv \paren {500 n - 38}^2 \equiv 444 \pmod {1000}$
{{qed}}
Theorem: Subset and Image Admit Infima and Mapping is Increasing implies Infimum of Image Succeeds Mapping at Infimum

Let $\struct {S, \preceq}$ and $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a increasing mapping.
Let $D \subseteq S$ such that
:$D$ admits a infimum in $S$ and $f \sqbrk D$ admits a infimum in $T$.
Then $\map f {\inf D} \precsim \map \inf {f \sqbrk D}$

Proof:
By definition of infimum:
:$\inf D$ is lower bound for $D$.
By Increasing Mapping Preserves Lower Bounds:
:$\map f {\inf D}$ is a lower bound for $f \sqbrk D$.
Thus by definition of infimum:
:$\map f {\inf D} \precsim \map \inf {f \sqbrk D}$
{{qed}}
Theorem: Equivalence of Definitions of Finite Galois Extension

Let $L / K$ be a finite field extension.
{{TFAE|def = Finite Galois Extension}}

Proof:
=== 1 implies 2 ===
Note that by Finite Field Extension has Finite Galois Group, $G = \Aut {L / K}$ is finite.
Let $\alpha \in L$.
Then its orbit under $G$ is finite.
By:
:Minimal Polynomial of Element with Finite Orbit under Group of Automorphisms over Fixed Field in terms of Orbit
its minimal polynomial over $K$ splits completely in $L$.
Thus $L / K$ is normal.
By:
:Finite Orbit under Group of Automorphisms of Field implies Separable over Fixed Field
$L / K$ is separable.
{{qed|lemma}}
Theorem: Finite Field Extension has Finite Galois Group

Let $E / F$ be a finite field extension.
Then its Galois group is finite.

Proof:
Because $E / F$ is finite, it is finitely generated.
Let $\alpha_1, \ldots, \alpha_n \in E$ with $E = \map F {\alpha_1, \ldots, \alpha_n}$.
By Finite Field Extension is Algebraic, $\alpha_1, \ldots, \alpha_n$ are algebraic over $F$.
Let $f_1, \ldots, f_n$ be their minimal polynomials.
Let $f = f_1\dots f_n$.
By Galois Group Acts Faithfully on Generating Set, $\Gal {E / F}$ acts faithfully on the roots of $f$.
Thus $\Gal {E / F}$ is finite.
{{qed}}
Category:Field Extensions
Category:Galois Groups of Field Extensions
aykhxcoyl0j78qxh90e1ce7g987y2i9