## 11.9 multzero: A small formal proof

 Page 386 of 800 Search internet

The multzero page states and proves a simple lemma. The page uses the definition of Peano arithmetic, a lemma, and a lot of proof tactics from the Peano page. A numbered version of the multzero.lgs source text is included below. Also see the original, unnumbered lgs file, the main pdf, and the document root.

     1	"";;014E20344F3D486370710A10269E83D974EB8E9787EFB994A0BBD8BB0806
2	""P multzero
3	""R check
4	""R Peano
5	""R base
6
7	""D 0
8	3.2l
9
10	""B
11	page ( ""N , ""C )
12	title "Multiplication by zero"
13	bib "
14	@Book         {Mendelson87,
15	  author    = {E. Mendelson},
16	  title     = {Introduction to Mathematical Logic},
17	  publisher = {Wadsworth and Brooks},
18	  year      = {1987},
19	  edition   = {3.}}
20	"
21	main text "
22	\title{Multiplication by zero}
23	\author{A. U. Thor}
24	\maketitle
25	\tableofcontents
26	"[ make macro expanded version ragged right ]"
27	"[ prepare proof indentation ]"
28	\section{Theorem}
29	We now state Lemma 3.2l of \cite{Mendelson87}:
30	"[ PA lemma 3.2l : all x : 0 * x = 0 end lemma ]"
31	\section{Proof}
32	"[ PA proof of 3.2l :
33	line L01 : S7 >> 0 * 0 = 0 ;
34	line L02 : Block >> Begin ;
35	line L03 : Hypothesis >> 0 * x = 0 ;
36	line L04 : S8 >> 0 * x suc = 0 * x + 0 ;
37	line L05 : S5 >> 0 * x + 0 = 0 * x ;
38	line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ;
39	line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ;
40	line L08 : Block >> End ;
41	line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ;
42	line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed ]"
43	\bibliography{./page}
44	"
45	appendix "
46	\title{Multiplication by zero - appendix}
47	\author{A. U. Thor}
48	\maketitle
49	\tableofcontents
50	\section{\TeX\ definitions}
51	\begin{statements}
52	\item "[[ tex show define 3.2l as "
53	\mathbf{3.2l}" end define ]]"
54	\end{statements}
55	"
56	end page
57



 Page 386 of 800 Search logiweb.eu