(************** Content-type: application/mathematica ************** CreatedBy='Mathematica 5.0' Mathematica-Compatible Notebook This notebook can be used with any Mathematica-compatible application, such as Mathematica, MathReader or Publicon. The data for the notebook starts with the line containing stars above. To get the notebook into a Mathematica-compatible application, do one of the following: * Save the data starting with the line of stars above into a file with a name ending in .nb, then open the file inside the application; * Copy the data starting with the line of stars above to the clipboard, then use the Paste menu command inside the application. Data for notebooks contains only printable 7-bit ASCII and can be sent directly in email or through ftp in text mode. Newlines can be CR, LF or CRLF (Unix, Macintosh or MS-DOS style). NOTE: If you modify the data for this notebook not in a Mathematica- compatible application, you must delete the line below containing the word CacheID, otherwise Mathematica-compatible applications may try to use invalid cache data. For more information on notebooks and Mathematica-compatible applications, contact Wolfram Research: web: http://www.wolfram.com email: info@wolfram.com phone: +1-217-398-0700 (U.S.) Notebook reader applications are available free of charge from Wolfram Research. *******************************************************************) (*CacheID: 232*) (*NotebookFileLineBreakTest NotebookFileLineBreakTest*) (*NotebookOptionsPosition[ 29697, 886]*) (*NotebookOutlinePosition[ 32356, 973]*) (* CellTagsIndexPosition[ 31981, 956]*) (*WindowFrame->Normal*) Notebook[{ Cell[CellGroupData[{ Cell["Prove:", "ProofText", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Theorem (sqrt[2] irrational))", ButtonFunction:> FocusWindows[ $TmaReturnedObject, "Theorem (sqrt[2] irrational)"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{}], Cell[BoxData[ \(\[Not] rat[\@2]\)], "Conclusion", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[",", "ProofText", TaggingRules:>{}] }], "Conclusion", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}, CellTags->"Theorem (sqrt[2] irrational)"], Cell[CellGroupData[{ Cell["under the assumptions:", "ProofText", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Lemma (coprime))", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "Lemma (coprime)"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{}], Cell[BoxData[ RowBox[{ UnderscriptBox["\[ForAll]", RowBox[{ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]}]], RowBox[{"(", RowBox[{ RowBox[{ RowBox[{"nat", "[", StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "\[And]", RowBox[{"nat", "[", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]}], "\[Implies]", RowBox[{"(", RowBox[{ RowBox[{"(", RowBox[{ RowBox[{"2", "*", SuperscriptBox[ StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"]}], "=", SuperscriptBox[ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"]}], ")"}], "\[Implies]", RowBox[{"\[Not]", RowBox[{"coprime", "[", RowBox[{ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}]}]}], ")"}]}], ")"}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[",", "ProofText", TaggingRules:>{}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}, CellTags->"Lemma (coprime)"], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Definition (rational))", ButtonFunction:> FocusWindows[ $TmaReturnedObject, "Definition (rational)"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{}], Cell[BoxData[ RowBox[{ UnderscriptBox["\[ForAll]", RowBox[{ StyleBox["r", FontWeight->"Plain", FontSlant->"Italic", Background->None], " "}]], RowBox[{"(", RowBox[{ RowBox[{"rat", "[", StyleBox["r", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], InterpretationBox[\(\(:\)\(\[NegativeThickSpace]\ \[NegativeThinSpace]\)\(\[DoubleLeftRightArrow]\)\), IffByDef, SyntaxForm->":="], " ", RowBox[{ UnderscriptBox["\[Exists]", RowBox[{ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]}]], RowBox[{"(", RowBox[{ RowBox[{"nat", "[", StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "\[And]", RowBox[{"nat", "[", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "\[And]", RowBox[{"(", RowBox[{ StyleBox["r", FontWeight->"Plain", FontSlant->"Italic", Background->None], "=", FractionBox[ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]]}], ")"}], "\[And]", RowBox[{"coprime", "[", RowBox[{ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}]}], ")"}]}]}], ")"}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[",", "ProofText", TaggingRules:>{}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}, CellTags->"Definition (rational)"], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Definition (sqrt))", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "Definition (sqrt)"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{}], Cell[BoxData[ RowBox[{ UnderscriptBox["\[ForAll]", RowBox[{ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], " "}]], RowBox[{"(", RowBox[{ RowBox[{"(", SqrtBox[ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None]], ")"}], ":=", RowBox[{ UnderscriptBox[\(\(\[SuchThat]\)\(\[NegativeThickSpace]\)\(!\)\)\ , RowBox[{ StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], " "}]], RowBox[{"(", RowBox[{ SuperscriptBox[ StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"], "=", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], ")"}]}]}], ")"}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[".", "ProofText", TaggingRules:>{}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}, CellTags->"Definition (sqrt)"] }, Open ]], Cell[CellGroupData[{ Cell["From what we already know follows:", "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1}], Cell[TextData[{ "From ", StyleBox["(", "Label"], ButtonBox["Definition (sqrt)", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Definition (sqrt)"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " we can infer by expansion of the \"such that\"\[Dash]quantifier" }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1}], Cell[TextData[ButtonBox["(1)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "1"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1}], Cell[BoxData[ RowBox[{ UnderscriptBox["\[ForAll]", RowBox[{ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None]}]], RowBox[{"(", RowBox[{ RowBox[{"(", RowBox[{ RowBox[{"(", SqrtBox[ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None]], ")"}], "=", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], ")"}], "\[DoubleLeftRightArrow]", RowBox[{"(", RowBox[{ SuperscriptBox[ StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"], "=", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], ")"}]}], ")"}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1}], Cell[".", "ProofText", TaggingRules:>{2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1}, CellTags->"1"] }, Open ]], Cell[TextData[{ "We prove ", StyleBox["(", "Label"], ButtonBox["Theorem (sqrt[2] irrational)", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Theorem (sqrt[2] irrational)"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " by contradiction." }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1}], Cell["We assume ", "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1, 2, 1}], Cell[TextData[ButtonBox["(3)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "3"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1, 2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1}], Cell[BoxData[ \(rat[\@2]\)], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1}], Cell[",", "ProofText", TaggingRules:>{2, 1, 2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1}, CellTags->"3"], Cell[TextData[{ "and show ", Cell[BoxData[ \("a contradiction"\)], "Expression", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1}, FontColor->RGBColor[1, 0, 0]], "." }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1}], Cell[TextData[{ "Formula ", StyleBox["(", "Label"], ButtonBox["3", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "3"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", by ", StyleBox["(", "Label"], ButtonBox["Definition (rational)", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Definition (rational)"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", implies:" }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[TextData[ButtonBox["(4)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "4"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1, 2, 1, 2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{ UnderscriptBox["\[Exists]", RowBox[{ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]}]], RowBox[{"(", RowBox[{ RowBox[{"coprime", "[", RowBox[{ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "\[And]", RowBox[{"nat", "[", StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "\[And]", RowBox[{"nat", "[", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "\[And]", RowBox[{"(", RowBox[{\((\@2)\), "=", FractionBox[ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]]}], ")"}]}], ")"}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[".", "ProofText", TaggingRules:>{2, 1, 2, 1, 2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1}, CellTags->"4"], Cell[TextData[{ "By ", StyleBox["(", "Label"], ButtonBox["4", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "4"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " we can take appropriate values such that:" }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[ButtonBox["(5)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "5"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{ RowBox[{"coprime", "[", RowBox[{ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "\[And]", RowBox[{"nat", "[", StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "\[And]", RowBox[{"nat", "[", StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "\[And]", RowBox[{"(", RowBox[{\((\@2)\), "=", FractionBox[ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]]}], ")"}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1}], Cell[".", "ProofText", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1}, CellTags->"5"], Cell[TextData[{ "By modus ponens, from ", StyleBox["(", "Label"], ButtonBox["5.2", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "5.2"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", ", StyleBox["(", "Label"], ButtonBox["5.3", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "5.3"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " and an appropriate instance of ", StyleBox["(", "Label"], ButtonBox["Lemma (coprime)", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Lemma (coprime)"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " follows:" }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[ButtonBox["(6)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "6"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{ RowBox[{"(", RowBox[{ RowBox[{"2", "*", SuperscriptBox[ StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"]}], "=", SuperscriptBox[ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"]}], ")"}], "\[Implies]", RowBox[{"\[Not]", RowBox[{"coprime", "[", RowBox[{ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}]}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[",", "ProofText", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, CellTags->"6"], Cell[TextData[{ "Formula ", StyleBox["(", "Label"], ButtonBox["5.4", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "5.4"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", by ", StyleBox["(", "Label"], ButtonBox["1", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "1"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", implies:" }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[ButtonBox["(7)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "7"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{ SuperscriptBox[ RowBox[{"(", FractionBox[ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]], ")"}], "2"], "=", "2"}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[".", "ProofText", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, CellTags->"7"], Cell[CellGroupData[{ Cell["\<\ Using built\[Dash]in simplification rules we can simplify the \ knowledge base:\ \>", "ProofText", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[{ "Formula ", StyleBox["(", "Label"], ButtonBox["7", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "7"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " simplifies to" }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[ButtonBox["(8)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "8"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{ RowBox[{"2", "*", SuperscriptBox[ StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"]}], "=", SuperscriptBox[ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[".", "ProofText", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, CellTags->"8"] }, Open ]], Cell[TextData[{ "From ", StyleBox["(", "Label"], ButtonBox["8", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "8"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " and ", StyleBox["(", "Label"], ButtonBox["6", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "6"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " we obtain by modus ponens" }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[TextData[ButtonBox["(9)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "9"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{"\[Not]", RowBox[{"coprime", "[", RowBox[{ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}]}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[".", "ProofText", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}] }], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}, CellTags->"9"], Cell[TextData[{ "Now, ", StyleBox["(", "Label"], ButtonBox["9", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "9"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " and ", StyleBox["(", "Label"], ButtonBox["5.1", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "5.1"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " are contradictory." }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell["\[EmptySquare]", "ProofText", CellMargins->{{Inherited, Inherited}, {Inherited, 0}}, CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TextAlignment->Right] }, Open ]] }, FrontEndVersion->"5.0 for X", ScreenRectangle->{{0, 1280}, {0, 1024}}, ScreenStyleEnvironment->"Working", CellGrouping->Manual, WindowSize->{520, 600}, WindowMargins->{{Automatic, 372}, {184, Automatic}}, PrintingPageRange->{Automatic, Automatic}, PrintingOptions->{"PrintingMargins"->{{54, 54}, {0, 72}}, "PaperSize"->{597.562, 842.375}, "PaperOrientation"->"Portrait", "PrintCellBrackets"->False, "PrintRegistrationMarks"->True, "PrintMultipleHorizontalPages"->False, "PostScriptOutputFile":>FrontEnd`FileName[{$RootDirectory, "home", \ "wwindste", "Publications", "Papers", "Sqrt2"}, "notRatSqrt2.nb.ps", \ CharacterEncoding -> "iso8859-1"], "Magnification"->1}, Magnification->1, StyleDefinitions -> "TheoremaProof.nb" ] (******************************************************************* Cached data follows. If you edit this Notebook file directly, not using Mathematica, you must remove the line containing CacheID at the top of the file. The cache data will then be recreated when you save this file from within Mathematica. *******************************************************************) (*CellTagsOutline CellTagsIndex->{ "Theorem (sqrt[2] irrational)"->{ Cell[1892, 57, 735, 22, 32, "Conclusion", CellTags->"Theorem (sqrt[2] irrational)"]}, "Lemma (coprime)"->{ Cell[2784, 87, 2561, 71, 62, "Assumption", CellTags->"Lemma (coprime)"]}, "Definition (rational)"->{ Cell[5348, 160, 3300, 89, 62, "Assumption", CellTags->"Definition (rational)"]}, "Definition (sqrt)"->{ Cell[8651, 251, 1868, 55, 39, "Assumption", CellTags->"Definition (sqrt)"]}, "1"->{ Cell[11197, 330, 1912, 56, 39, "Assumption", CellTags->"1"]}, "3"->{ Cell[13733, 408, 714, 21, 32, "Assumption", CellTags->"3"]}, "4"->{ Cell[15512, 467, 2270, 64, 38, "Assumption", CellTags->"4"]}, "5"->{ Cell[18233, 548, 1852, 52, 38, "Assumption", CellTags->"5"]}, "6"->{ Cell[21100, 635, 1705, 45, 32, "Assumption", CellTags->"6"]}, "7"->{ Cell[23497, 706, 1259, 32, 40, "Assumption", CellTags->"7"]}, "8"->{ Cell[25466, 764, 1270, 32, 32, "Assumption", CellTags->"8"]}, "9"->{ Cell[27468, 823, 1308, 31, 32, "Assumption", CellTags->"9"]} } *) (*CellTagsIndex CellTagsIndex->{ {"Theorem (sqrt[2] irrational)", 30874, 916}, {"Lemma (coprime)", 30993, 919}, {"Definition (rational)", 31106, 922}, {"Definition (sqrt)", 31222, 925}, {"1", 31318, 928}, {"3", 31399, 931}, {"4", 31479, 934}, {"5", 31560, 937}, {"6", 31641, 940}, {"7", 31722, 943}, {"8", 31803, 946}, {"9", 31884, 949} } *) (*NotebookFileOutline Notebook[{ Cell[CellGroupData[{ Cell[1776, 53, 113, 2, 32, "ProofText"], Cell[1892, 57, 735, 22, 32, "Conclusion", CellTags->"Theorem (sqrt[2] irrational)"], Cell[CellGroupData[{ Cell[2652, 83, 129, 2, 32, "ProofText"], Cell[2784, 87, 2561, 71, 62, "Assumption", CellTags->"Lemma (coprime)"], Cell[5348, 160, 3300, 89, 62, "Assumption", CellTags->"Definition (rational)"], Cell[8651, 251, 1868, 55, 39, "Assumption", CellTags->"Definition (sqrt)"] }, Open ]], Cell[CellGroupData[{ Cell[10556, 311, 152, 2, 32, "ProofText"], Cell[10711, 315, 483, 13, 32, "ProofText"], Cell[11197, 330, 1912, 56, 39, "Assumption", CellTags->"1"] }, Open ]], Cell[13124, 389, 469, 13, 32, "ProofText"], Cell[13596, 404, 134, 2, 32, "ProofText"], Cell[13733, 408, 714, 21, 32, "Assumption", CellTags->"3"], Cell[14450, 431, 358, 10, 32, "ProofText"], Cell[14811, 443, 698, 22, 32, "ProofText"], Cell[15512, 467, 2270, 64, 38, "Assumption", CellTags->"4"], Cell[17785, 533, 445, 13, 32, "ProofText"], Cell[18233, 548, 1852, 52, 38, "Assumption", CellTags->"5"], Cell[20088, 602, 1009, 31, 50, "ProofText"], Cell[21100, 635, 1705, 45, 32, "Assumption", CellTags->"6"], Cell[22808, 682, 686, 22, 32, "ProofText"], Cell[23497, 706, 1259, 32, 40, "Assumption", CellTags->"7"], Cell[CellGroupData[{ Cell[24781, 742, 240, 5, 32, "ProofText"], Cell[25024, 749, 439, 13, 32, "ProofText"], Cell[25466, 764, 1270, 32, 32, "Assumption", CellTags->"8"] }, Open ]], Cell[26751, 799, 714, 22, 32, "ProofText"], Cell[27468, 823, 1308, 31, 32, "Assumption", CellTags->"9"], Cell[28779, 856, 717, 22, 32, "ProofText"], Cell[29499, 880, 182, 3, 25, "ProofText"] }, Open ]] } ] *) (******************************************************************* End of Mathematica Notebook file. *******************************************************************)