Kopfzeile {* Drei-Teilt-N-Satz *}
Theorie DreiTeilt
verwendet Haupt
Beginn
Unterabschnitt {* Zusammenfassung *}
Text {*
Dieses Schriftstück enthält einen Beweis des Drei-Teilt-N-Satzes, im Brunhilde/Rhein-Satzbeweisssytem formalisiert.
{\em Satz}: $3$ teilt $n$ genau dann, wenn $3$ die Summe aller Ziffern in $n$ teilt.
{\em Formloser Beweis}:
Sei $n = \sum{n_j * 10^j}$ wobei $n_j$ die $j$te niedrigstwertigste Ziffer der Dezimalschreibweise
der Zahl $n$ ist, und die Summe über alle Ziffern läuft.
Dann ist $$ (n - \sum{n_j}) = \sum{n_j * (10^j
- 1)} $$ Wir wissen, dass $\forall j\; 3|(10^j - 1) $ und damit $3|LHS$,
weiter gilt $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$
@{text "\<box>"}
*}
Unterabschnitt {* Förmlicher Beweis *}
Unterunterabschnitt {* Ein paar Lemmata zu Summation *}
Text {* Wenn @{text "A x"} für alle $x$ durch $a$ geteilt wird, dann teilt
$a$ jede Summe über Terme der Form @{text "(A x)*(P x)"}, für beliebiges $P$. *}
Lemma durch_sum:
fuer a::nat und n::nat
zeigt "∀x. a teilt A x ==> a teilt (∑x<n. A x * D x)"
Beweis (Induktion n)
Fall 0 zeige ?Fall durch Vereinfachung
fertig
Fall (Suc n)
wegen Suc
gilt "a teilt (A n * D n)" durch (Vereinfachung mit: teilt_mult2)
samt Suc
gilt "a teilt ((∑x<n. A x * D x) + (A n * D n))" durch (Vereinfachung mit: teilt_add)
dann zeige ?Fall durch Vereinfachung
wzbw
Unterunterabschnitt {* Verallgemeinertes Drei-Teilt *}
Text {* In diesem Abschnitt wird eine verallgemeinerte Form des
Drei-Teilt-Problems gelöst. Wir zeigen dass der Satz für jede
Zahlenfolge gilt. Im nächsten Abschnitt wenden wir diesen
Satz dann auf den Spezialfall der Dezimaldarstellung an. *}
Text {*
Here zeigen wir dass die erste Aussage des formlosen Beweises
für alle natürlichen Zahlen gilt. Beachte dass wir @{term "D i"}
benutzen, um das $i$-te Element einer Zahlenfolge zu bezeichnen.
*}
Lemma ziffern_differenz_aufteilung:
fuer n::nat und nd::nat und x::nat
zeigt "n = (∑x∈{..<nd}. (D x)*((10::nat)^x)) ==>
(n - (∑x<nd. (D x))) = (∑x<nd. (D x)*(10^x - 1))"
durch (Vereinfachung mit: summe_differenz_distributiv summe_multiplikation_distributiv2)
Text {* Nun zeigen wir, dass Zahlen der Form $10^x - 1$ stets von 3
geteilt werden *}
Lemma drei_teilt_0:
zeigt "(3::nat) teilt (10^x - 1)"
Beweis (Induktion x)
Fall 0 zeige ?Fall durch Vereinfachung
fertig
Fall (Suc n)
sei ?drei = "(3::nat)"
gilt "?drei teilt 9" durch Vereinfachung
darueberhinaus
gilt "?drei teilt (10*(10^n - 1))" durch (Regel teilt_mult) (Regel Suc)
dann gilt "?drei teilt (10^(n+1) - 10)" durch (Vereinfachung mit: nat_distrib)
letztendlich
gilt "?drei teilt ((10^(n+1) - 10) + 9)"
durch (Vereinfachung nur mit: ac_simps) (Regel teilt_add)
dann zeige ?Fall durch Vereinfachung
wzbw
Text {* Das vorherige Lemma und Lemma @{text "durch_sum"} wird ausgeführt. *}
Lemma drei_teilt_1:
fuer D :: "nat => nat"
zeigt "3 teilt (∑x<nd. D x * (10^x - 1))"
durch (subst mult.commute, rule durch_sum) (Vereinfachung mit: drei_teilt_0 [simplified])
Text {* Mit dem Lemmata @{text "ziffern_differenz_aufteilung"} und
@{text "drei_teilt_1"} zeigen wir das folgende Lemma:
*}
Lemma drei_teilt_2:
fuer nd::nat und D::"nat=>nat"
zeigt "3 teilt ((∑x<nd. (D x)*(10^x)) - (∑x<nd. (D x)))"
Beweis-
wegen drei_teilt_1 gilt "3 teilt (∑x<nd. D x * (10 ^ x - 1))" .
dann zeige ?These durch (Vereinfachung nur mit: ziffern_differenz_aufteilung)
wzbw
Text {*
Nun können wir den Hauptsatz dieses Abschnittes präsentieren.
Für jede Zahlenfolge (gegen durch eine Funktion @{term "D :: (nat=>nat)"})
zeigen wir dass drei die Expansionssumme $\sum{(D\;x)*10^x}$ over $x$
genau dann teilt, wenn drei die Summe der Zahlen $\sum{D\;x}$ teilt.
*}
Lemma drei_teilt_allgemein:
fuer D :: "nat => nat"
zeigt "(3 teilt (∑x<nd. D x * 10^x)) = (3 teilt (∑x<nd. D x))"
Beweis
gilt mono: "(∑x<nd. D x) ≤ (∑x<nd. D x * 10^x)"
durch (Regel setsum_mono) Vereinfachung
txt {* Damit können wir den Ausdruck
@{term "(∑x<nd. D x * 10^x) - (∑x<nd. D x)"} formen. *}
{
nimm "3 teilt (∑x<nd. D x)" an
samt drei_teilt_2 mono
zeige "3 teilt (∑x<nd. D x * 10^x)"
durch (Explosion intro: teilt_diffD)
}
{
nimm "3 teilt (∑x<nd. D x * 10^x)" an
samt drei_teilt_2 mono
zeige "3 teilt (∑x<nd. D x)"
durch (Explosion intro: teilt_diffD1)
}
wzbw
Unterunterabschnitt {* Drei-Teilt, natürlich *}
Text {*
Dieser Abschnitt zeigt dss wir für alle natürlichen Zahlen eine Zahlenfolge
von Ziffern kleiner 10 angeben können, die der Dezimalentwicklung der Zahl
entspricht. Wir können darauf unser Lemma @{text "drei_teilt_allgemein"} anwenden,
um unseren Hauptsatz zu zeigen.
*}
Text {* \medskip Definition von Länge und Quersumme. *}
Text {*
Dieser Abschnitt für ein paar Funktionen ein, um die nötigen Eigenschaften
natürlicher Zahlen zu berechnen. Danach beweisen wir ein paar Eigenschaften
dieser Funktionen. *}
Text {*
Die Funktion @{text "nlaenge"} gibt die Anzal der Ziffern einer natürlichen
Zahl $n$ an.*}
Funktion nlaenge :: "nat => nat"
wobei
"nlaenge 0 = 0"
| "nlaenge x = 1 + nlaenge (x durch 10)"
Text {* Die Funktion @{text "quersumme"} berechnet die Summe der Ziffern einer
Zahl $n$. *}
definition
quersumme :: "nat => nat" wobei
"quersumme n = (∑x < nlaenge n. n durch 10^x rest 10)"
Text {* Einige Eigenschaften dieser Funktionen:. *}
Lemma nlaenge_null:
"0 = nlaenge x ==> x = 0"
durch (Induktion x rule: nlaenge.induct) Automatismen
Lemma nlaenge_Nachfolger:
"Nachfolger m = nlaenge n ==> m = nlaenge (n durch 10)"
durch (Induktion n rule: nlaenge.induct) Vereinfachung_ueberall
Text {*
Das folgende ist das Hauptlemma, das wir brauchen, um unseren Satz
zu beweisen. Es besagt dass eine Entwicklung einer natürlichen Zahl $n$
in eine Ziffernfolge immer möglich ist. *}
Lemma entwicklung_existiert:
"m = (∑x<nlaenge m. (m durch (10::nat)^x rest 10) * 10^x)"
Beweis (Induktion "nlaenge m" beliebig: m)
Fall 0 dann zeige ?Fall durch (Vereinfachung mit: nlaenge_null)
fertig
Fall (Suc nd)
erhalte c wobei ment: "m = 10*(m durch 10) + c ∧ c < 10"
und cdef: "c = m rest 10" durch Vereinfachung
zeige "m = (∑x<nlaenge m. m durch 10^x rest 10 * 10^x)"
Beweis -
wegen `Nachfolger nd = nlaenge m`
gilt "nd = nlaenge (m durch 10)" durch (rule nlaenge_Nachfolger)
samt Suc gilt
"m durch 10 = (∑x<nd. m durch 10 durch 10^x rest 10 * 10^x)" durch Vereinfachung
samt ment gilt
"m = 10*(∑x<nd. m durch 10 durch 10^x rest 10 * 10^x) + c" durch Vereinfachung
weiter gilt
"… = (∑x<nd. m durch 10 durch 10^x rest 10 * 10^(x+1)) + c"
durch (ersetze mengensumme_rechts_distributiv) (Vereinfachung mit: ac_simps)
weiter gilt
"… = (∑x<nd. m durch 10^(Nachfolger x) rest 10 * 10^(Nachfolger x)) + c"
durch (Vereinfachung mit: durch_mult2_gleich[symmetric])
weiter gilt
"… = (∑x∈{Nachfolger 0..<Nachfolger nd}. m durch 10^x rest 10 * 10^x) + c"
durch (Vereinfachung nur mit: mengensumme_verschiebe_grenzen_Nachfolger)
(Vereinfachung mit: mindestens_null_kleiner_als)
weiter gilt
"… = (∑x<Nachfolger nd. m durch 10^x rest 10 * 10^x)"
durch (Vereinfachung mit: mindestens_null_kleiner_als[symmetric] mengensumme_anfang_bis_nachfolger cdef)
weiter note `Nachfolger nd = nlaenge m`
zusammengefasst
zeige "m = (∑x<nlaenge m. m durch 10^x rest 10 * 10^x)" .
wzbw
wzbw
Text {* \medskip Hauptsatz *}
Text {* Wir können nun das allgemeine Lemma @{text "drei_teilt_allgemein"}
und die Existenzaussage von @{text "entwicklung_existiert"} verwenden, um unseren
Hauptsatz zu zeigen. *}
Satz drei_teilt_nat:
zeigt "(3 teilt n) = (3 teilt quersumme n)"
Beweis (unfold quersumme_def)
gilt "n = (∑x<nlaenge n. (n durch (10::nat)^x rest 10) * 10^x)"
durch (rule entwicklung_existiert)
darueberhinaus
gilt "3 teilt (∑x<nlaenge n. (n durch (10::nat)^x rest 10) * 10^x) =
(3 teilt (∑x<nlaenge n. n durch 10^x rest 10))"
durch (rule drei_teilt_allgemein)
letztendlich
zeige "3 teilt n = (3 teilt (∑x<nlaenge n. n durch 10^x rest 10))" durch Vereinfachung
wzbw
Ende