3. Irrationality of √2
-
IrrationalSqrtTwo[complete]
The real number \sqrt{2} is irrational: it is not the image of any rational
number under the canonical embedding \mathbb{Q} \hookrightarrow \mathbb{R}.
Lean code for Definition3.1●1 definition
Associated Lean declarations
-
IrrationalSqrtTwo[complete]
-
IrrationalSqrtTwo[complete]
-
defdefined in DifferentProofs/IrrationalSqrtTwo/Defs.leancomplete
def IrrationalSqrtTwo
IrrationalSqrtTwo : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.def IrrationalSqrtTwo
IrrationalSqrtTwo : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.
-
IrrationalSqrtTwoNat[complete]
The natural-number form says that the equation p^2 = 2q^2 has no solution in
natural numbers with q \neq 0.
Lean code for Definition3.2●1 definition
Associated Lean declarations
-
IrrationalSqrtTwoNat[complete]
-
IrrationalSqrtTwoNat[complete]
-
defdefined in DifferentProofs/IrrationalSqrtTwo/Defs.leancomplete
def IrrationalSqrtTwoNat
IrrationalSqrtTwoNat : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.def IrrationalSqrtTwoNat
IrrationalSqrtTwoNat : Prop: PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.
The natural-number statement Definition 3.2 implies the real statement Definition 3.1.
Lean code for Theorem3.3●1 theorem
Associated Lean declarations
-
theoremdefined in DifferentProofs/IrrationalSqrtTwo/Basic.leancomplete
theorem IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo : IrrationalSqrtTwoNat → IrrationalSqrtTwo: IrrationalSqrtTwoNatIrrationalSqrtTwoNat : Prop→ IrrationalSqrtTwoIrrationalSqrtTwo : Proptheorem IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo : IrrationalSqrtTwoNat → IrrationalSqrtTwo: IrrationalSqrtTwoNatIrrationalSqrtTwoNat : Prop→ IrrationalSqrtTwoIrrationalSqrtTwo : Prop
If \sqrt{2} were the image of a rational r, squaring gives r^2 = 2 in
\mathbb{Q}. Writing r as the quotient of its numerator and denominator
and clearing denominators yields \mathrm{num}(r)^2 = 2\,\mathrm{den}(r)^2,
so taking absolute values gives a natural-number solution of p^2 = 2q^2
with q = \mathrm{den}(r) \neq 0.
First proof is by infinite descent.
-
IrrationalSqrtTwo_Descent[complete]
\sqrt{2} is irrational.
Lean code for Theorem3.4●1 theorem
Associated Lean declarations
-
IrrationalSqrtTwo_Descent[complete]
-
IrrationalSqrtTwo_Descent[complete]
-
theoremdefined in DifferentProofs/IrrationalSqrtTwo/Descent.leancomplete
theorem IrrationalSqrtTwo_Descent
IrrationalSqrtTwo_Descent : IrrationalSqrtTwo: IrrationalSqrtTwoIrrationalSqrtTwo : Proptheorem IrrationalSqrtTwo_Descent
IrrationalSqrtTwo_Descent : IrrationalSqrtTwo: IrrationalSqrtTwoIrrationalSqrtTwo : Prop
Use Theorem 3.3 to reduce to the natural-number form.
Suppose p^2 = 2q^2 with q > 0. Then 2 \mid p^2, so 2 \mid p since
2 is prime; write p = 2r. Substituting gives q^2 = 2r^2, a new
solution whose first component q is strictly smaller than p. By strong
induction no solution with q \neq 0 exists.
Second proof is by 2-adic valuation.
-
IrrationalSqrtTwo_Valuation[complete]
\sqrt{2} is irrational.
Lean code for Theorem3.5●1 theorem
Associated Lean declarations
-
IrrationalSqrtTwo_Valuation[complete]
-
IrrationalSqrtTwo_Valuation[complete]
-
theoremdefined in DifferentProofs/IrrationalSqrtTwo/Valuation.leancomplete
theorem IrrationalSqrtTwo_Valuation
IrrationalSqrtTwo_Valuation : IrrationalSqrtTwo: IrrationalSqrtTwoIrrationalSqrtTwo : Proptheorem IrrationalSqrtTwo_Valuation
IrrationalSqrtTwo_Valuation : IrrationalSqrtTwo: IrrationalSqrtTwoIrrationalSqrtTwo : Prop
Use Theorem 3.3 to reduce to the natural-number form.
Apply the exponent of 2 in the prime factorization to both sides of
p^2 = 2q^2. The left side has even 2-adic valuation 2v_2(p), while
the right side has odd valuation 1 + 2v_2(q), a contradiction.
Third proof is by Fermat's Last Theorem for exponent 3.
-
IrrationalSqrtTwo_FermatLastTheorem[complete]
\sqrt{2} is irrational.
Lean code for Theorem3.6●1 theorem
Associated Lean declarations
-
IrrationalSqrtTwo_FermatLastTheorem[complete]
-
IrrationalSqrtTwo_FermatLastTheorem[complete]
-
theoremdefined in DifferentProofs/IrrationalSqrtTwo/FermatLastTheorem.leancomplete
theorem IrrationalSqrtTwo_FermatLastTheorem
IrrationalSqrtTwo_FermatLastTheorem : IrrationalSqrtTwo: IrrationalSqrtTwoIrrationalSqrtTwo : Proptheorem IrrationalSqrtTwo_FermatLastTheorem
IrrationalSqrtTwo_FermatLastTheorem : IrrationalSqrtTwo: IrrationalSqrtTwoIrrationalSqrtTwo : Prop
This proof establishes the irrationality of \sqrt{2} Definition 3.1
directly, without the natural-number reduction.
One has the identity (18+17\sqrt{2})^3 + (18-17\sqrt{2})^3 = 42^3, due to
Jarvis and Meekin. If \sqrt{2} were a rational r, then 18+17r,
18-17r, and 42 would be nonzero rationals (nonzero because
(\pm 18/17)^2 \neq 2) solving x^3 + y^3 = z^3, contradicting Fermat's
Last Theorem for exponent 3. See
this Math StackExchange answer.