(************** 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[ 35564, 1084]*) (*NotebookOutlinePosition[ 38687, 1183]*) (* CellTagsIndexPosition[ 38152, 1162]*) (*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["(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[{ 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]}], "]"}]}]}], ")"}]}]], "Conclusion", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[",", "ProofText", TaggingRules:>{}] }], "Conclusion", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}, CellTags->"Lemma (coprime)"], Cell[CellGroupData[{ Cell["under the assumptions:", "ProofText", CellBracketOptions->{"Color"->RGBColor[0.643137, 0.756863, 1]}, TaggingRules:>{}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Proposition (even numbers): characteristic)", ButtonFunction:> FocusWindows[ $TmaReturnedObject, "Proposition (even numbers): characteristic"], 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[{ RowBox[{"2", "*", StyleBox["b", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "=", StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], ")"}], "\[Implies]", RowBox[{"is\[Dash]even", "[", StyleBox["a", 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->"Proposition (even numbers): characteristic"], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Proposition (even numbers): even square)", ButtonFunction:> FocusWindows[ $TmaReturnedObject, "Proposition (even numbers): even square"], 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], " "}]], RowBox[{"(", RowBox[{ RowBox[{"is\[Dash]even", "[", SuperscriptBox[ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"], "]"}], "\[Implies]", RowBox[{"is\[Dash]even", "[", StyleBox["a", 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->"Proposition (even numbers): even square"], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Proposition (common factor))", ButtonFunction:> FocusWindows[ $TmaReturnedObject, "Proposition (common factor)"], 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[{"\[Not]", RowBox[{"coprime", "[", RowBox[{ RowBox[{"2", "*", StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], ",", RowBox[{"2", "*", 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->"Proposition (common factor)"], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{}], Cell[TextData[ButtonBox["(Definition (even))", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "Definition (even)"], 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], " "}]], RowBox[{"(", RowBox[{ RowBox[{"is\[Dash]even", "[", StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], InterpretationBox[\(\(:\)\(\[NegativeThickSpace]\ \[NegativeThinSpace]\)\(\[DoubleLeftRightArrow]\)\), IffByDef, SyntaxForm->":="], " ", RowBox[{ UnderscriptBox["\[Exists]", RowBox[{ StyleBox["m", FontWeight->"Plain", FontSlant->"Italic", Background->None], " "}]], RowBox[{"(", RowBox[{ StyleBox["a", FontWeight->"Plain", FontSlant->"Italic", Background->None], "=", RowBox[{"2", "*", StyleBox["m", 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 (even)"] }, Open ]], Cell["We assume", "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[{ 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.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"], Cell["and show", "ProofText", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{2, 1}], Cell[TextData[ButtonBox["(2)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "2"], ButtonEvaluator->Automatic, Active->True, ButtonStyle->None]], "Label", TaggingRules:>{2, 1}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{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]}], "]"}]}]], "Conclusion", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1}], Cell[".", "ProofText", TaggingRules:>{2, 1}] }], "Conclusion", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1}, CellTags->"2"], Cell[TextData[{ "We prove ", StyleBox["(", "Label"], ButtonBox["2", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "2"]&), 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[ 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}], 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["1", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "1"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", by ", StyleBox["(", "Label"], ButtonBox["Proposition (even numbers): characteristic", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Proposition (even numbers): characteristic"]&), 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["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{"is\[Dash]even", "[", SuperscriptBox[ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"], "]"}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1}], "," }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[TextData[{ "which, by ", StyleBox["(", "Label"], ButtonBox["Proposition (even numbers): even square", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Proposition (even numbers): even square"]&), 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["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{"is\[Dash]even", "[", StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.705882, 0.054902, 0.611765]}, TaggingRules:>{2, 1, 2, 1, 2, 1}], "," }], "ProofText", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1}], Cell[TextData[{ "which, by ", StyleBox["(", "Label"], ButtonBox["Definition (even)", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Definition (even)"]&), 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["m", FontWeight->"Plain", FontSlant->"Italic", Background->None], " "}]], RowBox[{"(", RowBox[{ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "=", RowBox[{"2", "*", StyleBox["m", 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[{ StyleBox[\(a\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "=", RowBox[{"2", "*", StyleBox[\(m\_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[{ "Formula ", StyleBox["(", "Label"], ButtonBox["3", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "3"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", by ", StyleBox["(", "Label"], ButtonBox["5", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "5"]&), 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}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{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}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{"coprime", "[", RowBox[{ RowBox[{"2", "*", StyleBox[\(m\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]}], ",", StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}]], "Assumption", CellBracketOptions->{"Color"->RGBColor[0.305882, 0.815686, 0]}, TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[".", "ProofText", TaggingRules:>{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}, CellTags->"6"], Cell[TextData[{ "Formula ", StyleBox["(", "Label"], ButtonBox["1", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "1"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", by ", StyleBox["(", "Label"], ButtonBox["5", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "5"]&), 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}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{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}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{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[ RowBox[{"(", RowBox[{"2", "*", StyleBox[\(m\_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}], Cell[".", "ProofText", TaggingRules:>{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}, CellTags->"7"], Cell[CellGroupData[{ Cell["\<\ Using available computation 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}], 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}], Cell[TextData[{ Cell["", "Indent", TaggingRules:>{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}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{ RowBox[{"2", "*", SuperscriptBox[ StyleBox[\(m\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"]}], "=", SuperscriptBox[ StyleBox[\(b\_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}], 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->"8"] }, Open ]], Cell[TextData[{ "Formula ", StyleBox["(", "Label"], ButtonBox["8", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "8"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", by ", StyleBox["(", "Label"], ButtonBox["Proposition (even numbers): characteristic", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Proposition (even numbers): characteristic"]&), 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, 2, 1}], Cell[TextData[{ Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{"is\[Dash]even", "[", SuperscriptBox[ StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "2"], "]"}]], "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}], "," }], "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[{ "which, by ", StyleBox["(", "Label"], ButtonBox["Proposition (even numbers): even square", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Proposition (even numbers): even square"]&), 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, 2, 1}], Cell[TextData[{ Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{"is\[Dash]even", "[", 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}], "," }], "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[{ "which, by ", StyleBox["(", "Label"], ButtonBox["Definition (even)", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Definition (even)"]&), 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, 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["(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}, LineBreakWithin->False], Cell["", "Blank", TaggingRules:>{2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1}], Cell[BoxData[ RowBox[{ UnderscriptBox["\[Exists]", RowBox[{ StyleBox["m", FontWeight->"Plain", FontSlant->"Italic", Background->None], " "}]], RowBox[{"(", RowBox[{ StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "=", RowBox[{"2", "*", StyleBox["m", FontWeight->"Plain", FontSlant->"Italic", Background->None]}]}], ")"}]}]], "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->"9"], Cell[TextData[{ "By ", StyleBox["(", "Label"], ButtonBox["9", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "9"]&), 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, 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["(10)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "10"], 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[{ StyleBox[\(b\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None], "=", RowBox[{"2", "*", StyleBox[\(m\_1\), 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->"10"], Cell[TextData[{ "Formula ", StyleBox["(", "Label"], ButtonBox["6", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "6"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], ", by ", StyleBox["(", "Label"], ButtonBox["10", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "10"]&), 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, 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, 2, 1}], Cell[TextData[ButtonBox["(15)", ButtonFunction:>FocusWindows[ $TmaReturnedObject, "15"], 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, 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, 2, 1}], Cell[BoxData[ RowBox[{"coprime", "[", RowBox[{ RowBox[{"2", "*", StyleBox[\(m\_0\), FontWeight->"Plain", FontSlant->"Italic", Background->None]}], ",", RowBox[{"2", "*", StyleBox[\(m\_1\), FontWeight->"Plain", FontSlant->"Italic", Background->None]}]}], "]"}]], "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, 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, 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, 2, 1, 2, 1}, CellTags->"15"], Cell[TextData[{ "Now, ", StyleBox["(", "Label"], ButtonBox["15", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "15"]&), ButtonEvaluator->Automatic, ButtonStyle->"Hyperlink"], StyleBox[")", "Label"], " and ", StyleBox["(", "Label"], ButtonBox["Proposition (common factor)", ButtonFunction:>( Theorema`Provers`Common`BasicProofCells`Private`ExtractTaggedCell[ "Proposition (common factor)"]&), 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, 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->{{200, Automatic}, {Automatic, 180}}, PrintingPageRange->{Automatic, Automatic}, PrintingOptions->{"PaperSize"->{597.562, 842.375}, "PaperOrientation"->"Portrait", "PostScriptOutputFile":>FrontEnd`FileName[{$RootDirectory, "home", \ "wwindste", "Publications", "Papers", "Sqrt2"}, "coprime.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->{ "Lemma (coprime)"->{ Cell[1892, 57, 1979, 57, 38, "Conclusion", CellTags->"Lemma (coprime)"]}, "Proposition (even numbers): characteristic"->{ Cell[4028, 122, 1751, 51, 62, "Assumption", CellTags->"Proposition (even numbers): characteristic"]}, "Proposition (even numbers): even square"->{ Cell[5782, 175, 1444, 42, 55, "Assumption", CellTags->"Proposition (even numbers): even square"]}, "Proposition (common factor)"->{ Cell[7229, 219, 1561, 46, 38, "Assumption", CellTags->"Proposition (common factor)"]}, "Definition (even)"->{ Cell[8793, 267, 1988, 58, 37, "Assumption", CellTags->"Definition (even)"]}, "1"->{ Cell[10926, 332, 1032, 32, 32, "Assumption", CellTags->"1"]}, "2"->{ Cell[12090, 370, 1020, 31, 32, "Conclusion", CellTags->"2"]}, "3"->{ Cell[13668, 422, 1009, 30, 32, "Assumption", CellTags->"3"]}, "4"->{ Cell[17768, 553, 1287, 38, 37, "Assumption", CellTags->"4"]}, "5"->{ Cell[19506, 608, 1062, 30, 32, "Assumption", CellTags->"5"]}, "6"->{ Cell[21244, 664, 1142, 31, 32, "Assumption", CellTags->"6"]}, "7"->{ Cell[23068, 721, 1278, 34, 32, "Assumption", CellTags->"7"]}, "8"->{ Cell[25036, 781, 1234, 32, 32, "Assumption", CellTags->"8"]}, "9"->{ Cell[29282, 903, 1467, 38, 37, "Assumption", CellTags->"9"]}, "10"->{ Cell[31230, 958, 1245, 30, 32, "Assumption", CellTags->"10"]}, "15"->{ Cell[33183, 1014, 1399, 37, 32, "Assumption", CellTags->"15"]} } *) (*CellTagsIndex CellTagsIndex->{ {"Lemma (coprime)", 36585, 1110}, {"Proposition (even numbers): characteristic", 36719, 1113}, {"Proposition (even numbers): even square", 36878, 1116}, {"Proposition (common factor)", 37022, 1119}, {"Definition (even)", 37144, 1122}, {"1", 37240, 1125}, {"2", 37321, 1128}, {"3", 37402, 1131}, {"4", 37483, 1134}, {"5", 37564, 1137}, {"6", 37645, 1140}, {"7", 37726, 1143}, {"8", 37807, 1146}, {"9", 37888, 1149}, {"10", 37970, 1152}, {"15", 38053, 1155} } *) (*NotebookFileOutline Notebook[{ Cell[CellGroupData[{ Cell[1776, 53, 113, 2, 32, "ProofText"], Cell[1892, 57, 1979, 57, 38, "Conclusion", CellTags->"Lemma (coprime)"], Cell[CellGroupData[{ Cell[3896, 118, 129, 2, 32, "ProofText"], Cell[4028, 122, 1751, 51, 62, "Assumption", CellTags->"Proposition (even numbers): characteristic"], Cell[5782, 175, 1444, 42, 55, "Assumption", CellTags->"Proposition (even numbers): even square"], Cell[7229, 219, 1561, 46, 38, "Assumption", CellTags->"Proposition (common factor)"], Cell[8793, 267, 1988, 58, 37, "Assumption", CellTags->"Definition (even)"] }, Open ]], Cell[10796, 328, 127, 2, 32, "ProofText"], Cell[10926, 332, 1032, 32, 32, "Assumption", CellTags->"1"], Cell[11961, 366, 126, 2, 32, "ProofText"], Cell[12090, 370, 1020, 31, 32, "Conclusion", CellTags->"2"], Cell[13113, 403, 415, 13, 32, "ProofText"], Cell[13531, 418, 134, 2, 32, "ProofText"], Cell[13668, 422, 1009, 30, 32, "Assumption", CellTags->"3"], Cell[14680, 454, 358, 10, 32, "ProofText"], Cell[15041, 466, 740, 22, 32, "ProofText"], Cell[15784, 490, 544, 15, 32, "ProofText"], Cell[16331, 507, 483, 13, 32, "ProofText"], Cell[16817, 522, 506, 14, 32, "ProofText"], Cell[17326, 538, 439, 13, 32, "ProofText"], Cell[17768, 553, 1287, 38, 37, "Assumption", CellTags->"4"], Cell[19058, 593, 445, 13, 32, "ProofText"], Cell[19506, 608, 1062, 30, 32, "Assumption", CellTags->"5"], Cell[20571, 640, 670, 22, 32, "ProofText"], Cell[21244, 664, 1142, 31, 32, "Assumption", CellTags->"6"], Cell[22389, 697, 676, 22, 32, "ProofText"], Cell[23068, 721, 1278, 34, 32, "Assumption", CellTags->"7"], Cell[CellGroupData[{ Cell[24371, 759, 226, 5, 32, "ProofText"], Cell[24600, 766, 433, 13, 32, "ProofText"], Cell[25036, 781, 1234, 32, 32, "Assumption", CellTags->"8"] }, Open ]], Cell[26285, 816, 770, 22, 32, "ProofText"], Cell[27058, 840, 634, 15, 32, "ProofText"], Cell[27695, 857, 513, 13, 32, "ProofText"], Cell[28211, 872, 596, 14, 32, "ProofText"], Cell[28810, 888, 469, 13, 32, "ProofText"], Cell[29282, 903, 1467, 38, 37, "Assumption", CellTags->"9"], Cell[30752, 943, 475, 13, 32, "ProofText"], Cell[31230, 958, 1245, 30, 32, "Assumption", CellTags->"10"], Cell[32478, 990, 702, 22, 32, "ProofText"], Cell[33183, 1014, 1399, 37, 32, "Assumption", CellTags->"15"], Cell[34585, 1053, 778, 23, 32, "ProofText"], Cell[35366, 1078, 182, 3, 25, "ProofText"] }, Open ]] } ] *) (******************************************************************* End of Mathematica Notebook file. *******************************************************************)