nyuuzyou/wikis huggingface dataset:
Broken Chord Theorem/Proof 4

== Theorem ==
== Proof ==
Find $E$ on $BC$ such that $BD = BE$.
 
Thus we have five equal angles:
:$\angle MBE$
:$\angle MEB$
:$\angle AFM$
:$\angle MFC$
:$\angle CEF$
By Triangle with Two Equal Angles is Isosceles:
:$\triangle CEF$ is isosceles
By definition of isosceles:
:$CE = CF$
Since $\angle AFM = \angle CEF$:
:$\angle AFC + \angle ECF =$ two right angles.
Category:Broken Chord Theorem
Broken Chord Theorem/Proof 5

== Theorem ==
== Proof ==
Given $MD \perp BC$
Draw $MN \parallel BC$ to meet the circle at $N$.
Draw $NE \parallel MD$.
By Quadrilateral is Parallelogram iff Both Pairs of Opposite Sides are Equal or Parallel:
:$MNED$ is a parallelogram
By Parallelogram with One Right Angle is Rectangle:
:$MNED$ is a rectangle.
By Parallelism implies Equal Corresponding Angles:
:$\angle MDB = \angle NEC$
and both are right angles.
The result follows.
Category:Broken Chord Theorem
Brouncker's Formula

== Theorem ==
:$\dfrac 4 \pi = 1 + \cfrac {1^2} {2 + \cfrac {3^2} {2 + \cfrac {5^2} {2 + \cfrac {7^2} {2 + \cfrac {9^2} {2 + \cdots} } } } }$
== Proof ==
From Continued Fraction for Real Arctangent Function, we have:
:$\arctan x = \cfrac x {1 + \cfrac {x^2} {3 - x^2 + \cfrac {\paren {3 x}^2} {5 - 3 x^2 + \cfrac {\paren {5 x}^2} {7 - 5 x^2 + \cfrac {\paren {7 x}^2} {\ddots } } } } }$
From Arctangent of One, we have:
:$\map \arctan 1 = \dfrac \pi 4$
Therefore:
Taking the reciprocal of both sides, we obtain:
:$\dfrac 4 \pi = 1 + \cfrac {1^2} {2 + \cfrac {3^2} {2 + \cfrac {5^2} {2 + \cfrac {7^2} {2 + \cfrac {9^2} {2 + \cdots} } } } }$
== Also presented as ==
== Sources ==
* : Chapter $\text {A}.21$: Euler ()
* : Chapter $\text {B}.12$: Wallis's Product: Footnote $1$
* 
* 
Category:Brouncker's Formula
Category:Formulas for Pi
Brouncker's Formula/Also presented as

== Brouncker's Formula: Also presented as ==
Brouncker's Formula can also be presented as:
:$\dfrac \pi 4 = \dfrac 1 {1 + \cfrac {1^2} {2 + \cfrac {3^2} {2 + \cfrac {5^2} {2 + \cfrac {7^2} {2 + \cfrac {9^2} {2 + \cdots} } } } } }$
== Sources ==
* : Chapter $\text {A}.21$: Euler ()
Category:Brouncker's Formula
Brouwer's Fixed Point Theorem

== Theorem ==
=== One-Dimensional Version ===
=== Smooth Mapping ===
=== General Case ===
== Also known as ==
== Also see ==
* Definition:Fixed Point Theorem
== Historical Note ==
== Sources ==
* 
* 
Category:Brouwer's Fixed Point Theorem
Category:Fixed Point Theorems
Category:Continuous Real Functions
Category:Algebraic Topology
Category:Topology
Brouwer's Fixed Point Theorem/General Case

== Theorem ==
A continuous mapping $f$ of the closed unit ball ${B^n}^- \subset \R^n$ into itself has a fixed point:
:$\forall f \in \map {C^0} { {B^n}^- \to {B^n}^-} : \exists x \in {B^n}^- : \map f x = x$
== Proof ==
== Sources ==
* 
* 
* 
Category:Brouwer's Fixed Point Theorem
Brouwer's Fixed Point Theorem/One-Dimensional Version

== Theorem ==
Let $f: \closedint a b \to \closedint a b$ be a real function which is continuous on the closed interval $\closedint a b$.
Then:
:$\exists \xi \in \closedint a b: \map f \xi = \xi$
That is, a continuous real function from a closed real interval to itself fixes some point of that interval.
== Proof by Intermediate Value Theorem ==
== Proof using Connectedness ==
Category:Brouwer's Fixed Point Theorem
Brouwer's Fixed Point Theorem/One-Dimensional Version/Proof Using Connectedness

== Theorem ==
== Proof ==
By Subset of Real Numbers is Interval iff Connected, $\closedint a b$ is connected.
 there is no fixed point.
Then $\map f a > a$ and $\map f b < b$.
Let:
:$U = \set {x \in \closedint a b: \map f x > x}$
:$V = \set {x \in \closedint a b: \map f x < x}$
Then $U$ and $V$ are open in $\closedint a b$.
Because $a \in U$ and $b\in V$, $U$ and $V$ are non-empty.
By assumption:
:$U \cup V = \closedint a b$
Thus $\closedint a b$ is not connected, which is a contradiction.
Thus, by Proof by Contradiction, there exists at least one fixed point.
Category:Brouwer's Fixed Point Theorem
Brouwer's Fixed Point Theorem/One-Dimensional Version/Proof by Intermediate Value Theorem

== Theorem ==
== Proof==
As the codomain of $f$ is $\closedint a b$, it follows that the image of $f$ is a subset of $\closedint a b$.
Thus:
:$\map f a \ge a$
and
:$\map f b \le b$
Let us define the real function $g: \closedint a b \to \R$ by:
:$\map g x = \map f x - x$
Then by the Combined Sum Rule for Continuous Real Functions, $\map g x$ is continuous on $\closedint a b$.
But:
:$\map g a \ge 0$ and $\map g b \le 0$
By the Intermediate Value Theorem:
:$\exists \xi \in \openint a b: \map g \xi = 0$
Thus:
:$\map f \xi = \xi$
== Sources ==
* : $\S 9.16$
Category:Brouwer's Fixed Point Theorem
Brouwer's Fixed Point Theorem/Smooth Mapping

== Theorem ==
A smooth mapping $f$ of the closed unit ball $B^n \subset \R^n$ into itself has a fixed point:
:$\forall f \in \map {C^\infty} {B^n \to B^n}: \exists x \in B^n: \map f x = x$
== Proof ==
Suppose there exists such a mapping $f$ of the unit ball to itself without fixed points.
Since $\map f x \ne x$, the two points $x$ and $\map f x$ are distinct and there is a unique ray from $x$ to $\map f x$ on which they both lie.
Call this line $L$ and let $\map h x = \partial B^n \cap L$.
If $x \in \partial B^n$, then $\map h x = x$ and $h$ restricts to the identity on $\partial B^n$.
Since $x$ is in the line segment between $\map f x$ and $\map h x$, one may write the vector $\map h x - \map f x$ as a multiple $t$ times the vector $x - \map f x$, where $t \ge 1$.
Hence:
:$\map h x = t x + \paren {1 - t} \map f x$
Since $f$ is smooth, the smoothness of $t$ with respect to $x$ implies the smoothness of $h$.
Taking the dot product of both sides of this formula and noting that $\size {\map h x} = 1$:
:$t^2 \size {x - \map f x}^2 + 2 t \map f x \cdot \paren {x - \map f x} + \size {\map f x}^2 - 1 = 0$
Applying the Quadratic Formula gives:
:$t = \dfrac {\map f x \cdot \paren {\map f x - x} } {\size {x - \map f x}^2}$
an expression for $t$ in smooth terms of $x$.
Hence $h$ is a smooth retract of a compact manifold onto its boundary, which contradicts the Retraction Theorem.
Category:Brouwer's Fixed Point Theorem
Brouwerian Lattice iff Meet-Continuous and Distributive

== Theorem ==
Let $\mathscr S = \left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Then
:$\mathscr S$ is a Brouwerian lattice
:$\mathscr S$ is meet-continuous and distributive.
== Proof ==
=== Sufficient Condition ===
Let $\mathscr S$ be a Brouwerian lattice.
By Relative Pseudocomplement and Shift Mapping form Galois Connection in Brouwerian Lattice:
:for every $x \in S$, a mapping $f: S \to S$ if $\forall y \in S: f\left({y}\right) = x \wedge y$, then $f$ is lower adjoint of Galois connection
By Shift Mapping is Lower Adjoint iff Meet is Distributive with Supremum:
:$\forall x \in S, X \subseteq S: x \wedge \sup X = \sup \left\{ {x \wedge y: y \in X}\right\}$
Thus by definition of complete lattice:
:$\mathscr S$ is up-complete.
Thus
:for every an element $x \in S$ and a directed subset $D$ of $S$: $x \wedge \sup D = \sup \left\{ {x \wedge d: d \in D}\right\}$
Thus by definition
:$\mathscr S$ is meet-continuous.
Thus by Brouwerian Lattice is Distributive:
:$\mathscr S$ is distributive.
=== Necessary Condition ===
Assume that:
:$\mathscr S$ is meet-continuous and distributive.
Let $x \in S$.
Define a mapping $f: S \to S$:
:$\forall y \in S: f\left({y}\right) = x \wedge y$
By Meet-Continuous and Distributive implies Shift Mapping Preserves Finite Suprema:
:$f$ preserves finite suprema.
By Meet-Continuous implies Shift Mapping Preserves Directed Suprema:
:$f$ preserves directed suprema.
By Mapping Preserves Finite and Directed Suprema:
:$f$ preserves all suprema.
By All Suprema Preserving Mapping is Lower Adjoint of Galois Connection:
:$f$ is lower adjoint of Galois connection.
Thus by Brouwerian Lattice iff Shift Mapping is Lower Adjoint:
:$\mathscr S$ is Brouwerian lattice.
== Sources ==
* 
* 
Category:Brouwerian Lattices
Category:Meet-Continuous Lattices
Category:Distributive Lattices
Category:Complete Lattices
Brouwerian Lattice iff Shift Mapping is Lower Adjoint

== Theorem ==
Let $\struct {S, \preceq}$ be a lattice.
Then $\struct {S, \preceq}$ is a Brouwerian lattice :
:$\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is a lower adjoint
== Proof ==
:$\struct {S, \preceq}$ is a Brouwerian lattice
:
:$\forall x, y \in S: x$ has relative pseudocomplement with respect to $y$ by definition of Brouwerian lattice
:
:$\forall x, y \in S: \max \set {s \in S: x \wedge s \preceq y}$ exists by definition of relative pseudocomplement
:
:$\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is a lower adjoint by Shift Mapping is Lower Adjoint iff Appropriate Maxima Exist
== Sources ==
* 
* 
Category:Galois Connections
Category:Brouwerian Lattices
Brouwerian Lattice is Distributive

== Theorem ==
Let $\struct {S, \preceq}$ be a Brouwerian lattice.
Then $\struct {S, \preceq}$ is a distributive lattice
== Proof ==
Let $x, y, z \in S$.
By Brouwerian Lattice iff Shift Mapping is Lower Adjoint:
:$\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is a lower adjoint
Define a mapping $f: S \to S$:
:$\forall s \in S: \map f s = x \wedge s$
Then:
:$f$ is a lower adjoint
By Lower Adjoint Preserves All Suprema:
:$f$ preserves all suprema
By definition of preserves all suprema:
:$f$ preserves the supremum of $\set {y, z}$
By definition of lattice:
:$\set {y, z}$ admits a supremum
By preserves the supremum of set:
:$\map \sup {\map {f^\to} {\set {y, z} } } = \map f {\sup \set {y, z} }$
Thus
Thus by definition:
:$\struct {S, \preceq}$ is a distributive lattice
== Sources ==
* 
* 
Category:Distributive Lattices
Category:Brouwerian Lattices
Brouwerian Lattice is Upper Bounded

== Theorem ==
Let $\struct {S, \vee, \wedge, \preceq}$ be a Brouwerian lattice.
Then $S$ is upper bounded.
== Proof ==
By assumption:
:$S \ne \O$
By definition of non-empty set:
:$\exists s: s \in S$
By definition of Brouwerian lattice:
:$s$ has relative pseudocomplement with respect to $s$
By definition of relative pseudocomplement:
:$\max \set {x \in S: s \wedge x \preceq s}$ exists and equals $s \to s$
Let $x \in S$.
By Meet Precedes Operands:
:$s \wedge x \preceq s$
Then:
:$x \in \set {x \in S: s \wedge x \preceq s}$
Thus by definition of maximum:
:$x \preceq s \to s$
Thus by definition:
:$s \to s$ is an upper bound for $S$
Thus by definition:
:$S$ is upper bounded.
== Sources ==
* 
* 
Category:Bounded Lattices
Category:Brouwerian Lattices
Brun's Theorem

== Theorem ==
The sum of the reciprocals of all the twin primes converges.
== Proof ==
== Also see ==
* Definition:Brun's Constant
== Historical Note ==
== Sources ==
* : $1 \cdotp 90195 \ldots$
* : $1 \cdotp 90216 \, 054 \ldots$
Category:Twin Primes
Brun's Theorem/Historical Note

== Historical Note on Brun's Theorem ==
While Brun's Theorem proves that the sum of the reciprocals of all the twin primes converges, it has not yet been established what it actually converges to.
The number, whatever it is, is referred to as Brun's constant. Its best estimate is updated as and when the occasion demands.
As pointed out by in his of $1986$:
:Its value is exceedingly hard to calculate.
== Sources ==
* : $1 \cdotp 90195 \ldots$
* : $1 \cdotp 90216 \, 054 \ldots$
Category:Historical Notes
Buffon's Needle

== Theorem ==
Let a horizontal plane be divided into strips by a series of parallel lines a fixed distance apart, like floorboards.
Let a needle whose length equals the distance between the parallel lines be dropped onto the plane randomly from a random height.
Then the probability that the needle falls across one of the parallel lines is $\dfrac 2 \pi$.
== Proof ==
For simplicity, consider the real number plane $\R^2$ divided into strips by the lines $x = k$ for each integer $k$.
Then the needle would have length $1$, which is the distance between the lines.
Define $\theta \in \hointr {-\dfrac \pi 2} {\dfrac \pi 2}$ as the angle between the needle and the $x$-axis.
Then the horizontal component of length of the needle is $\cos \theta$ for each $\theta$.
Let:
:$E$ be the event where the needle falls across the vertical lines,
:$\Theta_\theta$ be the event where the angle between the needle and the $x$-axis is $\theta$.
Let the needle drop.
, let the end with the larger $x$-coordinate have $x$-coordinate $0 \le x_n < 1$.
Then for each $\theta$, the needle falls across the line $x = 0$ exactly when $0 \le x_n \le \cos \theta$.
Therefore the probability that this happens is:
:$\condprob E {\Theta_\theta} = \dfrac {\cos \theta} 1 = \cos \theta$
By considering $\theta$ as a continuous random variable,
== Also known as ==
== Also see ==
* Buffon-Laplace Problem
== Historical Note ==
== Sources ==
* : $3 \cdotp 14159 \, 26535 \, 89793 \, 23846 \, 26433 \, 83279 \, 50288 \, 41972 \ldots$
* : $3 \cdotp 14159 \, 26535 \, 89793 \, 23846 \, 26433 \, 83279 \, 50288 \, 41971 \ldots$
* 
* 
* 
Category:Buffon's Needle
Category:Trigonometry
Category:Pi
Buffon's Needle/Historical Note

== Historical Note on Buffon's Needle ==
 published this problem in his Histoire Naturelle in $1777$.
 extended the problem to a general rectangular grid, thus creating what is now sometimes referred to as the Buffon-Laplace Problem.
 reports that a pupil of his once performed a practical experiment using Buffon's Needle to calculate a value for $\pi$.
After $600$ trials, a value of $3.137$ was obtained.
== Sources ==
* : $3 \cdotp 14159 \, 26535 \, 89793 \, 23846 \, 26433 \, 83279 \, 50288 \, 41972 \ldots$
* : $3 \cdotp 14159 \, 26535 \, 89793 \, 23846 \, 26433 \, 83279 \, 50288 \, 41971 \ldots$
* 
* 
Category:Historical Notes
Buffon-Laplace Problem

== Theorem ==
Let a horizontal plane be divided into rectangles by a rectangular grid of straight lines of distances $a$ and $b$ apart.
Let a needle whose length equals $l$ be dropped onto the plane randomly from a random height.
Then the probability that the needle falls across one or more lines is $\dfrac {2 l \paren {a + b} - l^2} {\pi a b}$.
== Proof ==
== Also known as ==
== Historical Note ==
== Sources ==
* 
* 
Category:Buffon's Needle
Bullseye Illusion

== Classic Problem ==
:
The circle of radius $3 a$ at the center has the same area as the outer annulus whose width is $1$.
However, it appears to be larger.
== Proof ==
From the diagram, it is seen that the circles are evenly spaced.
Let $C$ denote the circle of radius $3 a$ at the center, colored orange.
Let $A$ denote the outer annulus of width $a$ and outer radius $5 a$, colored blue.
We have that:
Hence the result.
== Sources ==
* 
* 
Category:Circles
Category:Classic Problems
Bung that fits Triangular, Square and Circular Holes

== Problem ==
What shape of bung can be used to plug three different holes:
:one square
:one triangular
:one circular?
== Solution ==
Let $r$ be the radius of the circle we want to plug.
Take a right circular cylindrical piece $B$ of the material for your bung whose base has radius $r$.
This will plug the circular hole.
Cut $B$ so that its height is $2 r$.
When you hold $B$ sideways, you see it will plug a square hole of side $2 r$.
Now draw a diameter $D$ of one of the bases of $B$.
Take two planes through $B$, both of which pass through $D$ such that they are both tangent to the other bases.
Slice away the material of $B$ on the other sides of the planes from the center of $B$.
Now $B$ has a triangular cross-section and it will plug a triangle whose sides are $\tuple {2 r, \sqrt 5 r, \sqrt 5 r}$.
:
== Historical Note ==
== Sources ==
* 
* : Henry van Etten: $116$
Category:Geometry
Category:Classic Problems
Bunyakovsky Conjecture

== Conjecture ==
Let $P$ be an irreducible polynomial of degree two or higher whose coefficients are all integers.
Then, for arguments which are all natural numbers, $P$ generates either:
:$(1):\quad$ an infinite set of numbers with greatest common divisor exceeding $1$
or:
:$(2):\quad$ infinitely many prime numbers.
== Historical Note ==
Category:Unproven Hypotheses
Burali-Forti Paradox

== Paradox ==
The ordinal of the set of all ordinals must be larger than any of the ordinals in that set.
Hence this would be an ordinal which is not contained in that set.
That is, it is an ordinal which is not contained in the set of all ordinals.
Hence the set of all ordinals is not an allowable set.
== Refutation ==
This paradox is an antinomy caused by the incorrect assumption that one can create a set of all ordinals.
This is formally expressed in Existence of Set of Ordinals leads to Contradiction.
== Also known as ==
== Also see ==
* Russell's Paradox, another paradox in naive set theory.
== Historical Note ==
== Sources ==
* 
* 
* 
Category:Burali-Forti Paradox
Category:Ordinals
Category:Naive Set Theory
Category:Antinomies
Category:Logical Paradoxes
Buridan's Ass

== Paradox ==
Choice cannot be determined by reasoned preference alone.
=== Traditional ===
=== Modern Setting ===
== Resolution ==
This is a falsidical paradox.
The reasoning has two weak points:
:$(1): \quad$ It is practically and realisatically impossible to design a system in which such perfect equality can exist.
:$(2): \quad$ Even if it is possible to create a system whereby it is not possible to make such an example of perfect equality, there are other ways of making choices.
:::The traditional technique for making such an arbitrary decision is just to toss a coin.
== Also see ==
* Definition:Unstable Equilibrium
== Historical Note ==
== Sources ==
* 
Category:Buridan's Ass
Category:Falsidical Paradoxes
Burnout Height of Upward Rocket under Constant Gravity

== Theorem ==
Let $R$ be a rocket whose structural mass is $m_1$.
Let $R$ contain fuel of initial mass $m_2$.
Let $R$ be fired straight up from the surface of a planet whose gravitational field exerts an Acceleration Due to Gravity of $g$, assumed constant.
Let $R$ burn fuel at a constant rate $a$, with a constant exhaust velocity $b$ relative to $R$.
Let all forces on $R$ except that due to the gravitational field be neglected.
Then the burnout height of $R$ is given by:
:$h_b = -\dfrac {g m_2^2} {2 a^2} + \dfrac {b m_2} a + \dfrac {b m_1} a \ln \dfrac {m_1} {m_1 + m_2}$
== Proof ==
The total mass of the rocket at time $t$ is given by
:$m = m_1 + m_2 - at$
The time $t_b$ at which the rocket runs out of fuel is given by:
:$t_b = \dfrac {m_2} a$
Now we can calculate the total force on the rocket to be:
:$F = b a - mg$
where:
:$b a$ is the rocket's thrust as calculated from Newton's Second Law of Motion
:$-mg$ is the force of gravity on the rocket
We can now calculate the acceleration of the rocket as a function of time using our calculated total force in Newton's First Law of Motion to obtain
where $\ddot h = \dfrac {\d^2 h} {\d t^2}$ is the second time derivative of the height of the rocket.
Integrating the acceleration function twice with respect to time will yield the height of the rocket as a function of time.
Performing the first integration:
The second integration:
Hence the result.
== Sources ==
* : Miscellaneous Problems for Chapter $2$: Problem $29$
Category:Rocket Science
Burnout Velocity of Upward Rocket under Constant Gravity

== Theorem ==
Let $R$ be a rocket whose structural mass is $m_1$.
Let $R$ contain fuel of initial mass $m_2$.
Let $R$ be fired straight up from the surface of a planet whose gravitational field exerts an Acceleration Due to Gravity of $g$, assumed constant.
Let $R$ burn fuel at a constant rate $a$, producing a constant exhaust velocity $b$ relative to $R$.
Let all forces on $R$ except that due to the gravitational field be neglected.
Then the burnout velocity of $R$ is given by:
:$v_b = b \ln \left({1 + \dfrac {m_1} {m_2} }\right) - \dfrac {g m_2} a$
== Proof ==
== Sources ==
* : Miscellaneous Problems for Chapter $2$: Problem $29$
Category:Rocket Science
Burnside's Lemma

== Theorem ==
Let $G$ be a finite group acting on a set $X$.
Let $X / G$ be the set of orbits under this action.
For $x \in X$, let $\Stab x$ be the stabilizer of $x$ by $G$.
For $g \in G$, let $X^g$ denotes the set of all elements in $X$ which is fixed by $g$, that is:
:$X^g := \set {x \in X: g x = x}$
Then:
:$\ds \size {X / G} = \frac 1 {\order G} \sum_{g \mathop \in G} \size {X^g}$
In words, the number of orbits equals the average number of fixed elements.
== Proof ==
== Also known as ==
This theorem is also known as Burnside's Counting Theorem.
Category:Group Actions
Bézout's Identity

== Theorem ==
Let $a, b \in \Z$ such that $a$ and $b$ are not both zero.
Let $\gcd \set {a, b}$ be the greatest common divisor of $a$ and $b$.
Then:
:$\exists x, y \in \Z: a x + b y = \gcd \set {a, b}$
That is, $\gcd \set {a, b}$ is an integer combination (or linear combination) of $a$ and $b$.
Furthermore, $\gcd \set {a, b}$ is the smallest positive integer combination of $a$ and $b$.
=== Bézout's Identity on Euclidean Domain ===
=== Bézout's Identity on Principal Ideal Domain ===
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Proof 4 ==
== Proof 5 ==
== Proof 6 ==
== Also known as ==
== Also see ==
* Integer Combination of Coprime Integers
== Applications ==
Bézout's Identity is primarily used when finding solutions to linear Diophantine equations, but is also used to find solutions via Euclidean Division Algorithm.
This result can also be applied to the Extended Euclidean Division Algorithm.
== Historical Note ==
== Sources ==
* 
Category:Number Theory
Category:Greatest Common Divisor
Category:Bézout's Identity
Bézout's Identity/Euclidean Domain

== Theorem ==
Let $\struct {D, +, \times}$ be a Euclidean domain whose zero is $0$ and whose unity is $1$.
Let $\nu: D \setminus \set 0 \to \N$ be the Euclidean valuation on $D$.
Let $a, b \in D$ such that $a$ and $b$ are not both equal to $0$.
Let $\gcd \set {a, b}$ be the greatest common divisor of $a$ and $b$.
Then:
:$\exists x, y \in D: a \times x + b \times y = \gcd \set {a, b}$
such that $\gcd \set {a, b}$ is the element of $D$ such that:
:$\forall c = a \times x + b \times y \in D: \map \nu {\gcd \set {a, b} } \le \map \nu c$
== Proof ==
We are given that $a, b \in D$ such that $a$ and $b$ are not both equal to $0$.
, suppose specifically that $b \ne 0$.
Let $S \subseteq D$ be the set defined as:
:$S = \set {x \in D_{\ne 0}: x = m \times a + n \times b: m, n \in D}$
where $D_{\ne 0}$ denotes $D \setminus 0$.
Setting $m = 0$ and $n = 1$, for example, it is noted that $b \in S$.
Therefore $S \ne \O$.
By definition, $\nu$ has the properties:
:$(1): \quad \forall a, b \in D, b \ne 0: \exists q, r \in D$ such that $\map \nu r < \map \nu b$, or $r = 0$, such that:
::::$a = q \times b + r$
:$(2): \quad \forall a, b \in D, b \ne 0$:
::::$\map \nu a \le \map \nu {a \times b}$
Let $\nu \sqbrk S$ denote the image of $S$ under $\nu$.
We have that:
:$\nu \sqbrk S \subseteq \N$
Hence by the Well-Ordering Principle $\nu \sqbrk S$ has a smallest element.
Let $d \in S$ be such that $\map \nu d$ is that smallest element of $\nu \sqbrk S$.
By definition of $S$, we have that:
:$d = u \times a + v \times b$
for some $u, v \in D$.
Let $x \in S$.
By $(2)$ above:
:$x = q \times d + r$
such that either:
:$\map \nu r < \map \nu d$
or:
:$r = 0$
 $r \ne 0$.
Then:
which contradicts the choice of $d$ as the element of $S$ such that $\map \nu d$ is the smallest element of $\nu \sqbrk S$.
Therefore:
:$\forall x \in S: x = q \times d$
for some $q \in D$.
That is:
:$\forall x \in S: d \divides x$
where $\divides$ denotes divisibility.
In particular:
:$d \divides a = 1 \times a + 0 \times b$
:$d \divides b = 0 \times a + 1 \times b$
Thus:
:$d \divides a \land d \divides b \implies \map \nu 1 \le \map \nu d \le \map \nu {\gcd \set {a, b} }$
However, note that as $\gcd \set {a, b}$ also divides $a$ and $b$ (by definition), we have:
Since $d$ is the element of $S$ such that $\map \nu d$ is the smallest element of $\nu \sqbrk S$:
:$\gcd \set {a, b} = d = u \times a + v \times b$
== Also known as ==
== Historical Note ==
Category:Euclidean Domains
Category:Greatest Common Divisor
Category:Bézout's Identity