Kopfzeile {* Die Quadratwurzeln von Primzahlen sind irrational. *}
Theorie Wurzel
verwendet Haupt
Beginn
Text {*
Die Quadratwurzel einer beliebigen Primzahl
(einschließlich 2) ist irrational.
*}
Satz primwurzel_irrational:
nimmt "prim (p::nat)" an
zeigt "wurzel p ∉ \<rat>"
Beweis
wegen `prim p` gilt p: "1 < p" durch (Vereinfachung mit: prim_nat_def)
nimm "wurzel p ∈ \<rat>" an
dann erhalte m n :: nat wobei
n: "n ≠ 0" und sqrt_rat: "¦wurzel p¦ = m / n"
und ggT: "ggT m n = 1" durch (Regel Rat_betrag_nat_teilt_natE)
gilt eq: "m⇧2 = p * n⇧2"
Beweis -
wegen n und sqrt_rat gilt "m = ¦wurzel p¦ * n" durch Vereinfachung
dann gilt "m⇧2 = (wurzel p)⇧2 * n⇧2"
durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat)
weiter gilt "(wurzel p)⇧2 = p" durch Vereinfachung
weiter gilt "… * n⇧2 = p * n⇧2" durch Vereinfachung
zusammengefasst zeige ?These ..
wzbw
gilt "p teilt m ∧ p teilt n"
Beweis
wegen eq gilt "p teilt m⇧2" ..
samt `prim p` zeige "p teilt m" durch (Regel prim_teilt_potenz_nat)
dann erhalte k wobei "m = p * k" ..
samt eq gilt "p * n⇧2 = p⇧2 * k⇧2" durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat ac_simps)
samt p gilt "n⇧2 = p * k⇧2" durch (Vereinfachung mit: zweierpotenz_ist_quadrat)
dann gilt "p teilt n⇧2" ..
samt `prim p` zeige "p teilt n" durch (Regel prim_teilt_potenz_nat)
wzbw
dann gilt "p teilt ggT m n" ..
samt ggT gilt "p teilt 1" durch Vereinfachung
dann gilt "p ≤ 1" durch (Vereinfachung mit: teilt_impliziert_kg)
samt p zeige Falsch durch Vereinfachung
wzbw
Korollar wurzel_2_nicht_rational: "wurzel 2 ∉ \<rat>"
verwende primwurzel_irrational[fuer 2] durch Vereinfachung
Unterabschnitt {* Veränderungen *}
Text {*
Hier ist eine weitere Version des Hauptbeweises, die vorwiegend
gerades Vorwärts-Schließen verwenden. Obwohl dies weniger einse
Von-Open-Nach-Unten-Struktur ergibt, ist es vermutlich näher den
Beweisen aus der Mathematik.
*}
Satz
nimmt "prim (p::nat)" an
zeigt "wurzel p ∉ \<rat>"
Beweis
wegen `prim p` gilt p: "1 < p" durch (Vereinfachung mit: prim_nat_def)
nimm "wurzel p ∈ \<rat>" an
dann erhalte m n :: nat wobei
n: "n ≠ 0" und sqrt_rat: "¦wurzel p¦ = m / n"
und ggT: "ggT m n = 1" durch (Regel Rat_betrag_nat_teilt_natE)
wegen n und sqrt_rat gilt "m = ¦wurzel p¦ * n" durch Vereinfachung
dann gilt "m⇧2 = (wurzel p)⇧2 * n⇧2"
durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat)
weiter gilt "(wurzel p)⇧2 = p" durch Vereinfachung
weiter gilt "… * n⇧2 = p * n⇧2" durch Vereinfachung
zusammengefasst gilt eq: "m⇧2 = p * n⇧2" ..
dann gilt "p teilt m⇧2" ..
samt `prim p` gilt teilt_m: "p teilt m" durch (Regel prim_teilt_potenz_nat)
dann erhalte k wobei "m = p * k" ..
samt eq gilt "p * n⇧2 = p⇧2 * k⇧2" durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat ac_simps)
samt p gilt "n⇧2 = p * k⇧2" durch (Vereinfachung mit: zweierpotenz_ist_quadrat)
dann gilt "p teilt n⇧2" ..
samt `prim p` gilt "p teilt n" durch (Regel prim_teilt_potenz_nat)
samt teilt_m gilt "p teilt ggT m n" durch (Regel ggT_groesster_nat)
samt ggT gilt "p teilt 1" durch Vereinfachung
dann gilt "p ≤ 1" durch (Vereinfachung mit: teilt_impliziert_kg)
samt p zeige Falsch durch Vereinfachung
wzbw
Text {* Eine alte Kastanie, die eine Konsequenz der Irrationalität von 2 ist. *}
Lemma "∃a b::real. a ∉ \<rat> ∧ b ∉ \<rat> ∧ a hoch b ∈ \<rat>" (is "EX a b. ?P a b")
Beweis cases
nimm "wurzel 2 hoch wurzel 2 ∈ \<rat>" an
dann gilt "?P (wurzel 2) (wurzel 2)"
durch (metis wurzel_2_nicht_rational)
dann zeige ?These durch Explosion
fertig
nimm 1: "wurzel 2 hoch wurzel 2 ∉ \<rat>" an
gilt "(wurzel 2 hoch wurzel 2) hoch wurzel 2 = 2"
verwende hoch_reele_potenz [fuer _ 2]
durch (Vereinfachung mit: potenz_potenz zweierpotenz_ist_quadrat [symmetric])
dann gilt "?P (wurzel 2 hoch wurzel 2) (wurzel 2)"
durch (metis 1 Rats_number_of wurzel_2_nicht_rational)
dann zeige ?These durch Explosion
wzbw
Ende