\documentclass[10pt,twoside]{article}
\usepackage{amssymb}
\usepackage{epsf}
\input epsf
\newcount{\quesco}
\def\eqj#1#2#3{\hbox to 12.5cm{
\noindent\hbox to 3cm{\hfill $#1$}$\,\,=\,\,$\hbox to 6.9cm{$#2$\hfill}\hfill\fbox{\hbox to 1.7cm{\hfill\phantom{A}#3\phantom{A}\hfill}}}}
\def\eqpend{\hbox to 12cm{\hfill\pend\hbox to 1.3cm{\hfill}}}
\def\eqjn#1#2#3{\hbox to 12cm{
\noindent\hbox to 2cm{\hfill $#1$}$\,\,\phantom{=}\,\,$\hbox to 7.5cm{$#2$\hfill}\hfill\fbox{\hbox to 1.3cm{\hfill\phantom{A}#3\phantom{A}\hfill}}}}
\def\imply{\longrightarrow}
\def\bimply{\longleftrightarrow}
\def\lto{\longrightarrow}
\def\quesno{\the\quesco\global\advance\quesco by 1}
\def\wmo{{\large{\bf\em WMO}}}
\def\nin{\noindent}
\def\mnin{\medbreak\noindent}
\def\bnin{\bigbreak\noindent}
\newcounter{boxcount}
\setcounter{boxcount}{0}
\quesco=1
\newcommand{\boxon}[1]{\refstepcounter{boxcount}
\medbreak
\begin{center}
{\bf BOX NO. \theboxcount$\,$:\ \ #1.}
\end{center}
\medbreak}
\newcommand{\boxonnop}[1]{\refstepcounter{boxcount}
\medbreak
\begin{center}
{\bf BOX NO. \theboxcount$\,$:\ \ #1}
\end{center}
\medbreak}
\newcommand{\Ft}[1]{\footnote{\mynine\baselineskip 8pt #1}}
\def\vup{\vspace{-1mm}}
\def\imply{\longrightarrow}
\def\zz{\mathbb{Z}}
\def\kk{\mathbb{K}}
\def\qq{\mathbb{Q}}
\def\cc{\mathbb{C}}
\def\rr{\mathbb{R}}
\def\nn{\mathbb{N}} 
\def\itobf{\subsubsection}
\def\unde#1{\underbar{#1}}
\def\tto{\mbox{$\kern4pt\rightarrow\kern-14.3pt\mapsto\kern5pt$}}
\def\vepsi{V^{\beps,\eps,\delta}}
\def\vepsim{V^{\beps(m),\eps(m),\delta(m)}}
\def\kepsi{K^{\beps,\eps}}
\def\pepsi{P^{\beps,\eps}}
\def\phixeps{\Phi_x^{\beps}}
\newcommand{\bprn}{\begin{proof}}
\newcommand{\eprn}{\end{proof}}
\newenvironment{proof}{\noindent {\em Proof}.\ }{\medskip}
\def\So{{\rm So}}
\def\Ta{{\rm Ta}}
\def\Gr{{\rm Gr}}
\def\Do{{\rm Dom}}
\def\Im{{\rm Im}}
\def\acabx{AC([a,b],X)}
\def\cabx{C^0([a,b],X)}
\def\acomabx{AC_{\Omega}([a,b],X)}
\def\comabx{C_{\Omega}^0([a,b],X)}
\newcommand{\myput}{\input}
\newcommand{\authorsar}{\cite{antocell,bressancolombo,cellina,cellinaornelas,colomboetal,fry,ornelas}}
\newcommand{\dato}{\vskip 3cm
{\bf THIS IS A DRAFT.\\
\vskip 0.2cm
DO NOT QUOTE WITHOUT PERMISSION.\\
\vskip 0.2cm
Date of this draft: \today.}}
\renewcommand{\theequation}{\arabic{section}.\arabic{subsection}.\arabic{equation}}
\newcommand{\idx}{\index}
\renewcommand{\contentsname}{\hfil {%\small
{\bf Contents}}}
%\topmargin -1.5cm
\newcommand{\hjsdraft}{\hfill{\rm Math 300 -- 01 -- Fall 2002}}
\newcommand{\mpdraft}{{\rm Instructor's Notes, No. 1, 
September 5, 2002} \hfill }
\begin{document}
\markboth{\hjsdraft}{\mpdraft}\parskip 0pt
\def\lefquo{``} %``for home use
\newcommand{\tgt}{{T}^{2,\ge}}
\newcommand{\bi}{\begin{itemize}}
\newcommand{\comment}[1]{}
\newcommand{\ei}{\end{itemize}}
\def\beps{\bar\varepsilon}
\def\co{{\rm co}}
\def\cco{\overline{{\rm co}}}
\def\belo{\,\epsilon\,}
\def\lowsub#1{\lower 2pt\hbox{${_{#1}}$}}
\def\adj{{\rm Adj\,}}
\def\traj{{\rm Traj\,}}
\def\ctraj{{\rm CTraj\,}}
\def\arc{{\rm Arc\,}}
\def\carc{{\rm CArc\,}}
\def\bloi{{\cal BL}(\Omega,I)}
\def\blon{{\cal BL}(\rr^n,\rr)}
\def\bor{{\rm Bor}}
\def\leb{{\rm Leb}}
\def\blons{{\cal BL}(\rr^n,\rr;S)}
\def\mbloiy{{\cal M}_e(\bloi,Y)}
\def\blxr{{\cal BL}(X,\rr)}
\def\bbxr{{\cal B}(X\times\rr)}
\def\mblxr{{\cal M}(\blxr,Y)}
\def\cvf{TVVF}
\def\cvfadomi{TVVF_{AD}(\Om,I)}
\def\ndc{{\bf W}}
\def\togr{{\buildrel \rm igr \over \to}}
\newcommand{\halmos}{\rule{1ex}{1.4ex}}
\newcommand{\edo}{\end{document}}
%\newcommand{\indexentry}[2]{\smalltype #1,$\,$#2}
%\newcommand{\indexentry}[2]{#1,$\,$#2}
\newcommand{\eprnoen}{\hspace*{\fill}$\halmos$\medskip}
\newtheorem{ittheorem}{Theorem}
\newtheorem{itdef}{Definition} 
\newtheorem{itlem}{Lemma} 
\newtheorem{itprop}{Proposition}
\newtheorem{itcor}{Corollary}
\newtheorem{itrem}{Remark}
\newcounter{itfac}
\newcounter{itexam}
\newtheorem{myfact}[itfac]{Fact}
\newtheorem{myexample}[itexam]{Example}
\newtheorem{mytheorem}[ittheorem]{Theorem}
\newtheorem{mydefinition}[itdef]{Definition}
\newtheorem{mylemma}[itlem]{Lemma}
\newtheorem{myproposition}[itprop]{Proposition}
\newtheorem{mycorollary}[itcor]{Corollary}
\newtheorem{myremark}[itrem]{Remark}
\newcommand{\subssection}[1]{\subsection{#1}
   \setcounter{equation}{0}}
\newenvironment{theorem}{\begin{mytheorem}$\!\!\!{\bf .}$}{\end{mytheorem}}
\newenvironment{definition}{\begin{mydefinition}$\!\!\!{\bf .}$\rm}{\end{mydefinition}} %no-italics
\newenvironment{lemma}{\begin{mylemma}$\!\!\!{\bf .}$}{\end{mylemma}}
\newenvironment{corollary}{\begin{mycorollary}$\!\!\!{\bf .}$}{\end{mycorollary}}
\newenvironment{proposition}{\begin{myproposition}$\!\!\!{\bf .}$}{\end{myproposition}}
\newenvironment{remark}{\begin{myremark}$\!\!\!{\bf .}$\rm}{\end{myremark}} %no-italics
\newenvironment{fact}{\begin{myfact}$\!\!\!{\bf .}$}{\end{myfact}}
\newenvironment{example}{\begin{myexample}$\!\!\!{\bf .}$\rm}{\end{myexample}} %no-italics
\def\proofend{\hfill$\diamondsuit\,$}
\def\pend{$\quad${\bf THE END}}
\newcommand{\beq}{\begin{equation}}
\newcommand{\eeq}{\end{equation}}
\newcommand{\beqn}{\begin{eqnarray}}
\newcommand{\eeqn}{\end{eqnarray}}
\newcommand{\beqno}{\begin{eqnarray*}}
\newcommand{\eeqno}{\end{eqnarray*}}
\newcommand{\bequot}{\begin{quotation}}
\newcommand{\equot}{\end{quotation}}
\newcommand{\rf}[1]{[\ref{#1}]} %bibliographical references
\newcommand{\text}[1]{\hbox{\rm \ #1\ \/}}
\newcommand{\beql}[1]{\begin{equation}\label{#1}}
\newcommand{\bt}{\begin{theorem}}
\newcommand{\bl}{\begin{lemma}}
\newcommand{\br}{\begin{remark}}
\newcommand{\bc}{\begin{corollary}}
\newcommand{\bp}{\begin{proposition}}
\newcommand{\bd}{\begin{definition}}
\newcommand{\bfact}{\begin{fact}}
\newcommand{\bex}{\begin{example}}
\newcommand{\ber}[1]{\begin{exercise}\label{#1}}
\newcommand{\bem}[1]{\begin{example}\label{#1}}  %Yes, 2 different ones...
\newcommand{\ec}{\end{corollary}}
\newcommand{\el}{\end{lemma}}
\newcommand{\er}{\end{remark}}
\newcommand{\et}{\end{theorem}}
\newcommand{\ed}{\end{definition}}
\newcommand{\ednoen}{\end{definition}}
\newcommand{\eprop}{\end{proposition}}
\newcommand{\epr}{\end{proof}}
\newcommand{\bpr}{\begin{proof}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  These are just for statements, no "qed" box is put in.
%%  (Also for when I have to finish something after a displayed equation
%%        or itemized.)
\newcommand{\ecs}{\end{corollary}}
\newcommand{\eers}{\end{exercise}}
\newcommand{\eexs}{\end{example}}
\newcommand{\eems}{\end{example}}
\newcommand{\els}{\end{lemma}}
\newcommand{\eles}{\end{lemmaex}}
\newcommand{\ers}{\end{remark}}
\newcommand{\ets}{\end{theorem}}
\newcommand{\eds}{\end{definition}}
\newcommand{\eps}{\end{proposition}}
\newcommand{\efact}{\end{fact}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\mybox}{\hfill \mbox{$\Box$}} %put at right margin (white square)
\newcommand{\qed}{\mybox} %put qed at right margin


\def\bptl{\pmb{\partial}}
\def\bptld{\pmb{\partial}^{{\cal D}}}
\def\nball{\bmath^n}  
\def\idnpball{{\rm id}_{\partial\bmath_n}}
\def\idrn{{\rm id}_{\rr^n}}
\def\id{{\rm id}}
\def\nno{\nn\cup\{0\}}
\def\dom{{\rm Dom}}
\def\msr{{\rm meas}}
\def\mitem{\medbreak\item}
\def\uitem{\vspace{-3mm}\item}
\def\oitem{\vspace{-1.2mm}\item}
\def\bigparo{\parindent=23pt}
\def\miitem{\medbreak\itemitem}
\def\medno{\medbreak\noindent}
\def\smalltype{\baselineskip=8pt}
\def\normaltype{\baselineskip=11pt}
\def\dekkertype{\baselineskip=0.54true cm}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%% Set up for Black Board Bold (\Bbb) font
% N.B. \Bbb works only in math mode
%\def\aabx{{\cal A}([a,b],X)}
\def\convav#1{{\onarr{{\rm av}#1}}}
\def\convtr{{\onarr{{\rm T}}}}
\def\Om{\Omega}
\def\mtraj{{\rm MTraj\,}}
\def\indi{\raise 1.5pt\hbox{$\chi$}}
\def\lowsub#1{\lower 2pt\hbox{${_{#1}}$}}
\def\pfo#1{{\cal P}_{#1}^{\rightarrow}}
\def\pba#1{{\cal P}_{#1}^{\leftarrow}}  
\def\aabx{{\cal A}(a,b,X)}
\def\icone{IC\kern0.1pt$^1$}
\def\iconeit{IC\kern0.5pt$^1$}
\def\mdno{\medbreak\noindent}
\def\inn{\int_{0}^{\tau}}
\def\bel{\beta}
\def\al{\alpha}
\def\eps{\varepsilon}
\def\bes{\bar\varepsilon}
\def\bdel{\bar\delta}\def\ffi{\varphi}
\def\al{\alpha}
%\font\twelvemsy=msym10 scaled\magstep1
%\font\tenmsy=msym10
%\font\sevenmsy=msym7
%\font\tinyfont=cmr6 
%\newfam\msyfam
%\textfont\msyfam=\twelvemsy
%\scriptfont\msyfam=\tenmsy
%\scriptscriptfont\msyfam=\sevenmsy
%\def\Bbb{\fam\msyfam}
%\def\nn{\Bbb{N}}
\def\nninf{\bar{\Bbb{N}}}
%\def\pmb#1{\setbox0=\hbox{$#1$}%
%  \kern-.025em\copy0\kern-\wd0
%  \kern.05em\copy0\kern-\wd0
%  \kern-.025em\raise.0433em\box0 }
\def\pmb#1{\setbox0=\hbox{$#1$}%
  \kern-.025em\copy0\kern-\wd0
  \kern.05em\copy0\kern-\wd0
  \kern-.025em\raise.0144em\box0 
  \kern-.025em\raise.0288em\box0 
  \kern-.025em\raise.0433em\box0 }
\def\pmbsus{\pmb}
\def\equaldef{\,{\buildrel \rm def \over =}\,}
\def\steero{$\sim$\kern -0.1cm$\sim$\kern -0.1cm$\sim$\kern-0.2cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern-0.28cm$>$\kern0.1cm}
\def\PPhi{\pmb{\Phi}}
\def\steer#1#2{$#1$\steero$#2$}
\def\steert#1#2#3{\hbox{$#1$\hbox{\lower0.4ex\hbox{\steero}}\kern-0.59cm\raise0.53ex\hbox{$#2$}}\kern0.35cm$#3$}
%BLACKBOARD BOLD
\def\vbar{\mathchoice{\vrule height6.3ptdepth-.5ptwidth.8pt\kern-.8pt}
   {\vrule height6.3ptdepth-.5ptwidth.8pt\kern-.8pt}
   {\vrule height4.1ptdepth-.35ptwidth.6pt\kern-.6pt}
   {\vrule height3.1ptdepth-.25ptwidth.5pt\kern-.5pt}}
\def\fudge{\mathchoice{}{}{\mkern.5mu}{\mkern.8mu}}
\def\bbc#1#2{{\rm \mkern#2mu\vbar\mkern-#2mu#1}}
\def\bbb#1{{\rm I\mkern-3.5mu #1}}
\def\bba#1#2{{\rm #1\mkern-#2mu\fudge #1}}
\def\bb#1{{\count4=`#1 \advance\count4by-64 \ifcase\count4\or\bba A{11.5}\or
   \bbb B\or\bbc C{5}\or\bbb D\or\bbb E\or\bbb F \or\bbc G{5}\or\bbb H\or
   \bbb I\or\bbc J{3}\or\bbb K\or\bbb L \or\bbb M\or\bbb N\or\bbc O{5} \or
   \bbb P\or\bbc Q{5}\or\bbb R\or\bbc S{4.2}\or\bba T{10.5}\or\bbc U{5}\or
   \bba V{12}\or\bba W{16.5}\or\bba X{11}\or\bba Y{11.7}\or\bba Z{7.5}\fi}}
\def\eps{\varepsilon}
\def\pmath{{\rm I}\kern-.2em{\rm P}}
\def\emath{{\rm I}\kern-.2em{\rm E}}
\def\bmath{{\rm I}\kern-.2em{\rm B}}
\def\rarr{\rightarrow}
\font\mymagfivebf=cmbx10 scaled\magstep 5
\font\mymagfiverm=cmr10 scaled\magstep 5
\font\mymagfourbf=cmbx10 scaled\magstep 4
\font\mymagfourrm=cmr10 scaled\magstep 4
\font\mymagthreebf=cmbx10 scaled\magstep 3
\font\mymagthreerm=cmr10 scaled\magstep 3
\font\mymagtwobf=cmbx10 scaled\magstep 2
\font\mymagtworm=cmr10 scaled\magstep 2
\font\mymagonebf=cmbx10 scaled\magstep 1
\font\mymagonerm=cmr10 scaled\magstep 1
\font\mymagzerobf=cmbx10 scaled\magstep 0
\font\mymagzerorm=cmr10 scaled\magstep 0
\font\mymagfivesl=cmsl10 scaled\magstep 5
\font\mymagfiveit=cmti10 scaled\magstep 5
\font\mymagfoursl=cmsl10 scaled\magstep 4
\font\mymagfourit=cmti10 scaled\magstep 4
\font\mymagthreesl=cmsl10 scaled\magstep 3
\font\mymagthreeit=cmti10 scaled\magstep 3
\font\mymagtwosl=cmsl10 scaled\magstep 2
\font\mymagtwoit=cmti10 scaled\magstep 2
\font\mymagonesl=cmsl10 scaled\magstep 1
\font\mymagoneit=cmti10 scaled\magstep 1
\font\mymagzerosl=cmsl10 scaled\magstep 0
\font\mymagzeroit=cmti10 scaled\magstep 0
\font\mynine=cmr9
\font\myninebf=cmbx9
\font\mysmall=cmr7
\font\mysmallit=cmti7
\font\myverysmall=cmr5
\def\figcap#1#2{\medbreak
\centerline{ Figure {#1}:\ #2}
\vbox to 0.3true in{\vfill}}
\def\mybigbreak{\vskip 0.3true in}
\def\mynotsobigbreak{\vskip 0.2true in}
%THE FOLLOWING MACROS WERE USED FOR THE 1987 CDC PAPER
\def\lip{{\rm Lip}}
\def\lipomy{{\rm Lip}(\Omega,Y)}
\def\rarr{\rightarrow}
\def\rint{\enspace\rightarrow\!\!\!\!\!\!\int}
\def\lint{\enspace\leftarrow\!\!\!\!\!\int}
\def\pvarieta{{\cal  P}({\bf P},\eta)}
\def\pvdata{{\bf P}=(m,{\bf t},{\bf r},{\bf E})}
\def\sre{S_{\rho}(\eta)}
\def\vari{E=\{\eta_{\varepsilon}:\varepsilon\in C\}}
\def\varii{E_{i}=\{\eta_{i,\varepsilon_{i}}:\varepsilon_{i}\in C_{i}\}}
\def\tou{trajectory of uniqueness}
\def\uzsig{{\cal U}_{0}(\Sigma)}
\def\uosig{{\cal U}_{1}(\Sigma)}
\def\uksig{{\cal U}_{k}(\Sigma)}
\def\sigisz{$\Sigma$ is a $C^{0}$ system}
\def\sigiso{$\Sigma$ is a $C^{1}$ system}
\def\sigisk{$\Sigma$ is a $C^{k}$ system}
\def\czad{$C^{0}$-admissible}
\def\coad{$C^{1}$-admissible}
\def\ckad{$C^{k}$-admissible}
\def\mysys{\Sigma=(M,U,f)}
\def\vk{(V,\kappa)}
\def\vkk{(V,\kappa,K)}
\def\chm{{\cal CH}(M)}
\def\km{{\cal K}(M)}
\def\kz{{\cal K}_{0}}
%\def\kk{\kappa(K)}
\def\kv{\kappa(V)}
\def\rr{{\rm I}\kern-.2em{\rm R}}
\def\rrinf{\overline{\rr}}
\def\nn{{\rm I}\kern-.2em{\rm N}}
\def\nninf{\overline{\nn}}
\def\rrsmall{{\mysmall I}\kern-.2em{\mysmall R}}
\def\R{{\rm I}\kern-.2em{\rm R}}
\def\emath{{\rm I}\kern-.2em{\rm E}}
\def\pmath{{\rm I}\kern-.2em{\rm P}}
\def\lmath{{\rm I}\kern-.2em{\rm L}}
\def\ro{{\rr}}
\def\rn{{\rr}^{n}}
\def\rnn{{\rr}^{n\times n}}
\def\rnlow{{\rr}_{n}}
\def\vkinchm{(V,\kappa)\in {\cal CH}(M)}
\def\vkkinkm{(V,\kappa,K)\in {\cal K}(M)}
\def\vvkkinkm{{\cal V}=(V,\kappa,K)\in {\cal K}(M)}
\def\vvkkinkz{{\cal V}=(V,\kappa,K)\in {\cal K}_{0}}
\def\vinkm{{\cal V}\in {\cal K}(M)}
\def\vinkz{{\cal V}\in {\cal K}_{0}}
\def\xinkv{x\in\kappa(V)}
\def\xinkk{x\in\kappa(K)}
\def\fk{f^{\kappa}}
\def\fke{f_{\eta}^{\kappa}}
\def\fkeo{f_{\eta_{1}}^{\kappa}}
\def\fket{f_{\eta_{2}}^{\kappa}}
\def\fkei{f_{\eta_{i}}^{\kappa}}
\def\szve{\sigma_{{\cal V},\eta}^{0}}
\def\sove{\sigma_{{\cal V},\eta}^{1}}
\def\skve{\sigma_{{\cal V},\eta}^{k}}
\def\rzveoet{\rho_{{\cal V},\eta_{1},\eta_{2}}^{0}}
\def\roveoet{\rho_{{\cal V},\eta_{1},\eta_{2}}^{1}}
\def\rtildeoveoet{\tilde \rho_{{\cal V},\eta_{1},\eta_{2}}^{1}}
\def\rkveoet{\rho_{{\cal V},\eta_{1},\eta_{2}}^{k}}
\def\delzveoet{\delta_{\cal V}^{0}(\eta_{1},\eta_{2})}
\def\deloveoet{\delta_{\cal V}^{1}(\eta_{1},\eta_{2})}
\def\delkveoet{\delta_{\cal V}^{k}(\eta_{1},\eta_{2})}
\def\delkvee{\delta_{\cal V}^{k}(\eta,\eta)}
\def\delkv{\delta_{\cal V}^{k}}
\def\delkvj{\delta_{{\cal V}_{j}}^{k}}
\def\dome{{\rm Dom}(\eta)}
\def\domei{{\rm Dom}(\eta_{i})}
\def\domej{{\rm Dom}(\eta_{j})}
\def\domeo{{\rm Dom}(\eta_{1})}
\def\domet{{\rm Dom}(\eta_{2})}
\def\arrint{\rightarrow\kern -7.5pt\int}
\def\expint#1#2#3{e^{\arrint_{#1}^{#2}#3}}
\def\compo{\hbox{$\,${\myverysmall o}$\,$}}
\def\plplus{(+\kern-0.02in\compo\kern -0.02in\oplus)}
\def\Om{\Omega}
\def\om{\omega}
\def\restr{\lceil}
\def\ffi{\varphi}
\def\ep{\varepsilon}
\def\dki{{\partial\,\,\,\over\partial\kappa^i}}
\def\dkia{\partial_i^\kappa}
\def\dkonea{\partial_1^\kappa}
\def\dkna{\partial_n^\kappa}
\def\pdto{\,\rightarrow\kern -12pt ^{pd}\,}
\def\tvto{\,\rightarrow\kern -12pt ^{tv}\,}
\def\opdto{\,\longrightarrow\kern -18pt ^{opd}\,}
\def\pdtvto{\,\hbox to 1.1true cm{\rightarrowfill}\kern -20pt ^{pdtv}\,\,\,}
\def\tpdtvto{\,\hbox to 1.1true cm{\rightarrowfill}\kern -23pt ^{tpdtv}\,\,\,}
\def\adjo#1{{\rm Adj}(#1)}
\def\adjonul#1{{\rm Adj}^{\nu,L}(#1)}
\def\cch{\overline{co}}


%\voffset=-0.28true in
%\hsize=16true cm
%\vsize=9.45true in
%\parindent 0.25true in
\raggedbottom
%\def\onarr#1{\,\hbox to 0.4in{\rightarrowfill}\kern-0.25 in
%\raise 5pt\hbox{$#1$}\kern 0.2 in}
\def\onarr#1{\,\hbox to 0.37in{\rightarrowfill}\kern-0.37in
\raise 7pt\hbox to 0.37in{\hfill$#1$\hfill}\kern 0.04 in}
\def\nextarr#1{\,\,\,\,\,\,|\kern-3.8pt\lower 9.3pt
\hbox{$\downarrow$}\lower 3pt\hbox{$#1$}\,\,}
\def\pmbeta{{\pmb{\eta}\kern 0.02in}}
\def\pmbetas{{\pmbsus{\eta}\kern 0.02in}}

\setcounter{page}{1}
%\pagestyle{empty}

\begin{center}
{\mymagtwobf THE BASIC AXIOMS AND SOME SIMPLE\\
THEOREMS OF INTEGER ARITHMETIC}
\end{center}
\bigbreak

\baselineskip=11pt

\begin{center}
{\mymagonebf 1.\ THE BASIC VOCABULARY}
\end{center}
\medbreak


\def\plin#1#2#3{\noindent\hbox to 0.4cm{\hfill#1.$\,$}
#2\ \ \hrulefill\ \hbox to 0.9cm{\hfill\ Page}\hbox to 0.6cm{\hfill #3}}

\begin{itemize}
\item[I.] The {\bf logical connectives:}
\begin{itemize}
\item[1.] The {\bf propositional connectives:}
\begin{itemize}
\item[a.] the {\em negation symbol} (``$\neg\ldots$'', read as
``not  $\ldots$'', or ``it is not the case that $\ldots$''),
\item[b.] the {\em conjunction symbol} (``$\ldots\wedge\ldots$'', read as
``$\ldots\,$and$\,\ldots$''),
\item[c.] the {\em disjunction symbol} (``$\ldots\vee\ldots$'', read as
``$\ldots\,$or$\,\ldots$''),
\item[d.] the {\em implication symbol} (``$\ldots\imply\ldots$'', read as
``$\ldots\,$implies$\,\ldots$'', or ``if,$\ldots\,$then$\,\ldots$''), 
\item[e.] the {\em biconditional symbol} (``$\ldots\bimply\ldots$'', read as
``$\ldots\,$if and only if$\,\ldots$''),
\end{itemize}
\item[2.] The {\bf quantifiers:}
\begin{itemize}
\item[a.] the {\em existential quantifier} (``$\exists \ldots$'', read as
``there exists $\ldots$ such that'');
\item[b.] the {\em universal quantifier} (``$\forall\ldots$'', read as
``for all $\ldots$'');
\end{itemize}
\item[3.] The {\bf right and left parentheses and the comma.}
\end{itemize}
\item[II.] The {\bf letter variables:} $a$, $b$, $\ldots$, 
$i$, $j$, $k$, $\ldots$, $m$, $n$, $p$, $q$, $\ldots$,
$x$, $y$, $z$, $\ldots$.  (In principle, any symbol
can be used as a variable, provided you declare it as such.  
This includes Greek letters such as $\alpha$, $\beta$, etc., 
Hebrew or Arabic letters, weird symbols such as $\diamondsuit$
or $\clubsuit$, 
\item[II.] {\bf The arithmetical symbols:}
\begin{itemize}
\item[a.] the {\em constants} ``$0$'' (``zero'') and
``$1$'' (``one''), 
\item[b.] the {\em symbols for the arithmetical operations}: ``$+$'' 
(``plus'') and ``$.$'' (``times'', sometimes written ``$\times$''), 
\item[c.] the {\em minus} (or {\em negative}) {\em symbol}: ``$-$'' 
(read ``minus'', or ``negative''),
\item[d.] the {\em predicates:} ``$=$'' (``is equal to'', or ``equals'') ,
``$<$'' (``is less than'', or ``is smaller than''),
``$>$'' (``is larger than''), 
``$\le$'' (``is less than or equal to'', or ``is not greater than''),
``$\ge$'' (``is greater than or equal to'', or ``is not smaller than'').
\end{itemize}
\end{itemize}
If you want, you can also include the predicates ``$\in\nn$'' 
(``belongs to $\nn$'', or ``is a natural number'', or ``is a nonnegative
integer'') and 
``$\in\nn$'' 
(``belongs to $\zz$'', or ``is an integer''). This, however, 
is not necessary, strictly speaking, because 
\begin{itemize}
\item[A.] If it is clear that we are just talking about the integers, 
then {\em everything is an integer}, so there is not need to say 
``$x$ is an integer'' every time we bring in an object $x$, because
$x$ couldn't possibly be anything other than an integer. So if this is the
case then ``$\in\zz$'' is not needed.
\item[B.] The predicate ``$\in\nn$'' is unnecessary, because instead
of saying ``$x\in\nn$'' you could just say 
``$x\ge 0$'', or ``$0\le x$.'' 
\end{itemize}
On the other hand, 
\begin{itemize}
\item[C.] If you include the predicate ``$\in\nn$'' then you do
not need to include the predicates $<$, $>$, $\le$, and $\ge$, because you
can {\em define} them in terms of the other symbols together with
``$\in\nn$''.  (This is what Problem 4 of page 5 of the book is about.) 
\item[D.] If you want to talk about integers and also things that are not
integers (e.g., sets, lists, integers modulo $n$), then you need the
predicate ``$\in\zz$ to specify when the things you are talking about are
supposed to be integers.
\end{itemize}

\medbreak\noindent Here are four versions of the basic vocabulary.
Version I is used if the universe of discourse is $\zz$, i.e., if we
are talking about integers only. Version II can be substituted for
Version I. Version III is used if the universe of discourse contains
$\zz$ and other things as well, i.e., if we are talking about integers
and also other things.  Version IV can be substituted for Version III.

\begin{center}
\fbox{\fbox{\begin{minipage}{10cm}
\begin{center}
{\mymagonebf THE BASIC VOCABULARY OF\\
INTEGER ARITHMETIC, VERSION I}
\end{center}
$$\neg\quad\wedge\quad\vee\imply\quad\bimply\quad\exists\quad\forall\quad
(\quad)\quad,$$
$$=\quad<\quad>\quad\le\quad\ge\quad 0\quad 1
\quad+\quad-\quad\cdot$$
$\qquad\qquad\qquad$ and the variables.
\end{minipage}}}
\end{center}

\begin{center}
\fbox{\fbox{\begin{minipage}{10cm}
\begin{center}
{\mymagonebf THE BASIC VOCABULARY OF \\
INTEGER ARITHMETIC, VERSION II}
\end{center}
$$\neg\quad\wedge\quad\vee\imply\quad\bimply\quad\exists\quad\forall\quad
(\quad)\quad,$$
$$=\quad\in\nn\quad 0\quad 1\quad+\quad-\quad\cdot$$
$\qquad\qquad\qquad$ and the variables.
\end{minipage}}}
\end{center}

\begin{center}
\fbox{\fbox{\begin{minipage}{10cm}
\begin{center}
{\mymagonebf THE BASIC VOCABULARY OF \\
INTEGER ARITHMETIC, VERSION III}
\end{center}
$$\neg\quad\wedge\quad\vee\imply\quad\bimply\quad\exists\quad\forall\quad
(\quad)\quad,$$
$$=\quad<\quad>\quad\le\quad\ge\quad\in\zz\quad 0\quad 1
\quad+\quad-\quad\cdot$$
$\qquad\qquad\qquad$ and the variables.
\end{minipage}}}
\end{center}

\begin{center}
\fbox{\fbox{\begin{minipage}{10cm}
\begin{center}
{\mymagonebf THE BASIC VOCABULARY OF \\
INTEGER ARITHMETIC, VERSION IV}
\end{center}
$$\neg\quad\wedge\quad\vee\imply\quad\bimply\quad\exists\quad\forall\quad
(\quad)\quad,$$
$$=\quad\in\nn\quad \in\zz\quad 0\quad 1\quad+\quad-\quad\cdot$$
$\qquad\qquad\qquad$ and the variables.
\end{minipage}}}
\end{center}

\bigbreak
\begin{center}
{\mymagonebf THE AXIOMS}
\end{center}
\bigbreak

\noindent The axioms give us some basic properties of addition,
multiplication, the ``negative of'' predicate, $0$,  $1$, 
$<$, $\le $,  $>$, and  $\ge$.

We divide these axioms into three groups: 

\begin{itemize}
\item[1.] The {\bf integral domain axioms}, i.e., the axioms 
that deal with addition,
multiplication, the ``negative of'' predicate, $0$,  and $1$.

\item[2.] The {\bf order axioms}, i.e., the axioms 
that deal with $<$, $\le $,  $>$, and  $\ge$.

\item[3.] The well-ordering principle.
\end{itemize}

\begin{center}
\fbox{\fbox{\begin{minipage}{11.4cm}
\begin{center}
{\bf THE AXIOMS OF INTEGER ARITHMETIC}
\end{center}
\bigbreak

\begin{center}
\fbox{\begin{minipage}{11.1cm}
\begin{center}
{\bf INTEGRAL DOMAIN AXIOMS}
\end{center}
\medbreak

\begin{itemize}\item[]\begin{itemize}
\item[IDA1.] $\forall x,\forall y,x+y=y+x$.

\item[IDA2.] $\forall x,\forall y,x.y=y.x$.

\item[IDA3.] $\forall x,\forall y,\forall z,(x+y)+z=x+(y+z)$.

\item[IDA4.] $\forall x,\forall y,\forall z,(x.y).z=x.(y.z)$.

\item[IDA5.] $\forall x,\forall y,\forall z,(x+y).z=x.z+y.z$.

\item[IDA6.] $\forall x,x+0=x$.

\item[IDA7.] $\forall x,x+(-x)=0$.

\item[IDA8.] $\forall x,x.1=x$.

\item[IDA9.] $\forall x,\forall y,\forall z,\Bigl((y.x=z.x\wedge\neg x=0)
\imply y=z\Bigr)$.

\item[IDA10.] $\neg 1=0$.

\end{itemize}\end{itemize}
\end{minipage}}
\medbreak
\fbox{\begin{minipage}{11.1cm}
\begin{center}
{\bf ORDER AXIOMS}
\end{center}
\medbreak

\begin{itemize}\item[]\begin{itemize}

\item[OA1.] $\forall x,\forall y,(x>y\bimply y<x)$

\item[OA2.] $\forall x,\forall y,(x\le y\bimply(x<y\vee x=y))$

\item[OA3.] $\forall x,\forall y,(x\ge y\bimply(x>y\vee x=y))$

\item[OA4.] $\forall x,\forall y,((0<x\wedge 0<y)\imply 0<x+y)$

\item[OA5.] $\forall x,\forall y,((0<x\wedge 0<y)\imply 0<x.y)$

\item[OA6.] $\forall x,\forall y,(x<y\bimply 0<y+(-x))$

\item[OA7.] $\forall x,(0\le x\vee x\le 0)$

\item[OA8.] $\neg\, 0<0$
\end{itemize}\end{itemize}
\end{minipage}}
\end{center}
\medbreak
\begin{center}
\fbox{\begin{minipage}{11.1cm}
\begin{center}
{\bf THE WELL-ORDERING PRINCIPLE}
\end{center}
\medbreak
\begin{itemize}\item[]\begin{itemize}
\item[WOP.] Let $u,v$ be variables, let $p(u)$ be a formula not
containing $v$ at all and containing no quantifiers $\exists u$, $\forall u$.
Let $p(v)$ be the formula obtained from $p(u)$ by substituting 
$v$ for $u$ throughout $p(u)$. Then
$$
\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
(\exists u,\!(0\!\le\! u\wedge p(u)))\!\imply\!
(\exists u,\!(0\!\le\! u\wedge p(u)\wedge\forall v,((0\!\le\! v\wedge p(v))
\!\imply\! u\!\le\!v)))\,.
$$
\end{itemize}\end{itemize}
\end{minipage}}
\end{center}
\vspace{-1mm}
\end{minipage}}}
\end{center}

\bigbreak\noindent{\bf THEOREM T1.} $-0=0$.

\medbreak\noindent{\bf PROOF.} 

\eqj{-0}{(-0)+0}{IDA6}

\noindent and 

\eqj{(-0)+0}{0}{IDA7}

So $-0=0$. \pend

\bigbreak\noindent{\bf DEFINITION D1.} $2=1+1$.

\bigbreak\noindent{\bf DEFINITION D2.} $3=2+1$.

\bigbreak\noindent{\bf DEFINITION D3.} $4=3+1$.

\bigbreak\noindent{\bf THEOREM T2.} $2+2=4$.

\medbreak\noindent{\bf PROOF.} 

\eqj{2+2}{2+(1+1)}{D1}

\eqj{}{(2+1)+1)}{IDA3}

\eqj{}{3+1)}{D2}

\eqj{}{4}{D3}

\eqpend

\bigbreak\noindent{\bf THEOREM T3.} $2.2=4$.

\medbreak\noindent{\bf PROOF.} 

\eqj{2.2}{2.(1+1)}{D1}

\eqj{}{2.1+2.1}{IDA5}

\eqj{}{2+2)}{IDA8}

\eqj{}{4}{T2}

\eqpend

\bigbreak\noindent{\bf THEOREM T4.} $\forall x,x.0=0$.

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. Then

\eqj{x.0}{x.0+0}{}

\eqj{}{x.0+(x.0+(-(x.0)))}{}

\eqj{}{(x.0+x.0)+(-(x.0))}{}

\eqj{}{x.(0+0)+(-(x.0))}{}

\eqj{}{x.0+(-(x.0))}{}

\eqj{}{0}{}

\eqpend

\bigbreak\noindent{\bf THEOREM T5.} $\forall x,\forall y,\forall z,
x.(y+z)=x.y+x.z$. 

\medbreak\noindent{\bf PROOF.} Let $x,y,z$ be arbitrary. Then

\eqj{x.(y+z)}{(y+z).x}{IDA2}

\eqj{}{y.x+z.x}{IDA5}

\eqj{}{x.y+x.z}{IDA2}

\eqpend

\bigbreak\noindent{\bf THEOREM T6.} $(-1).(-1)=1$.

\medbreak\noindent{\bf PROOF.}

\eqj{(-1).(-1)}{(-1).(-1)+0}{}

\eqj{}{(-1).(-1)+(1+(-1))}{}

\eqj{}{(-1).(-1)+(1+(-1).1)}{}

\eqj{}{(-1).(-1)+((-1).1+1)}{}

\eqj{}{((-1).(-1)+(-1).1)+1}{}

\eqj{}{(-1).((-1)+1)+1}{}

\eqj{}{(-1).(1+(-1))+1}{}

\eqj{}{(-1).0+1}{}

\eqj{}{0+1}{}

\eqj{}{1+0}{}

\eqj{}{1}{}

\eqpend

\bigbreak\noindent{\bf THEOREM T7.} $\forall x,(-1).x=-x$.

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. Then

\eqj{(-1).x}{(-1).x+0}{}

\eqj{}{(-1).x+(x+(-x))}{}

\eqj{}{((-1).x+x)+(-x)}{}

\eqj{}{(x.(-1)+x)+(-x)}{}

\eqj{}{(x.(-1)+x.1)+(-x)}{}

\eqj{}{x.((-1)+1)+(-x)}{}

\eqj{}{x.(1+(-1))+(-x)}{}

\eqj{}{x.0+(-x)}{}

\eqj{}{0+(-x)}{}

\eqj{}{(-x)+0}{}

\eqj{}{-x\,.}{}

\eqpend

\bigbreak\noindent{\bf THEOREM T8.} $\forall x,x.(-1)=-x$.

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. Then
$x.(-1)=(-1).x=-x$. 

\bigbreak\noindent{\bf THEOREM T9.} $\forall x,-(-x)=x$.

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. Then

\eqj{-(-x)}{(-x).(-1)}{}

\eqj{}{(x.(-1)).(-1)}{}

\eqj{}{x.((-1).(-1))}{}

\eqj{}{x.1}{}

\eqj{}{x}{}

\eqpend

\bigbreak\noindent{\bf THEOREM T10.} $\forall x,\forall y,-(x+y)=(-x)+(-y)$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. Then

\eqj{-(x+y)}{(x+y).(-1)}{}

\eqj{}{x.(-1)+y.(-1)}{}

\eqj{}{(-x)+(-y)}{}

\eqpend

\bigbreak\noindent{\bf DEFINITION D4.} $\forall x,\forall y,x-y=x+(-y)$.

\bigbreak\noindent{\bf THEOREM T11.} $\forall x,\forall y,\forall z,
(x-y=z\bimply x=y+z)$.

\medbreak\noindent{\bf PROOF.} Let $x,y,z$ be arbitrary. 
Assume $x-y=z$. Then 

\eqj{x}{x+0}{}

\eqj{}{x+(y+(-y))}{}

\eqj{}{x+((-y)+y)}{}

\eqj{}{(x+(-y))+y}{}

\eqj{}{(x-y)+y}{}

\eqj{}{z+y}{}

\eqj{}{y+z}{}

\noindent So $x-y=z\imply x=y+z$. 

Now suppose $x=y+z$. Then 

\eqj{x-y}{x+(-y)}{}

\eqj{}{(y+z)+(-y)}{}

\eqj{}{(z+y)+(-y)}{}

\eqj{}{z+(y+(-y))}{}

\eqj{}{z+0}{}

\eqj{}{z}{}
So $x=y+z\imply x-y=z$. \pend

\bigbreak\noindent{\bf THEOREM T12.} $\forall x,\forall y,-(x-y)=y-x$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. Then

\eqj{-(x-y)}{(x-y).(-1)}{}

\eqj{}{(x+(-y)).(-1)}{}

\eqj{}{x.(-1)+(-y).(-1)}{}

\eqj{}{x.(-1)+((y.(-1)).(-1))}{}

\eqj{}{(-x)+y.((-1).(-1))}{}

\eqj{}{(-x)+y.1}{}

\eqj{}{(-x)+y}{}

\eqj{}{y+(-x)}{}

\eqj{}{y-x}{}

\eqpend

\bigbreak\noindent{\bf DEFINITION D5.} $\forall x,
(x\,\,{\rm is\,\,even}\,\,\bimply\exists y,x=2.y)$. 

\bigbreak\noindent{\bf DEFINITION D6.} $\forall x,
(x\,\,{\rm is\,\,odd}\,\,\bimply\exists y,x=2.y+1)$. 

\bigbreak\noindent{\bf THEOREM T13.} $\forall x,\forall y,
((x\,\,{\rm is\,\,even}\,\,\wedge
y\,\,{\rm is\,\,even}\,\,)\imply x+y\,\,{\rm is\,\,even}\,\,)$

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Suppose $x$ and $y$ are even. Since $x$ is even, $\exists u,x=2.u$. 
Pick one such $u$ and call it $a$. Since $y$ is even, $\exists u,y=2.u$. 
Pick one such $u$ and call it $b$. Then $x=2.a$ and $y=2.b$. So
$x+y=2.(a+b)$. So $\exists u,x+y=2.u$. So $x+y$ is even.\pend

\bigbreak\noindent{\bf THEOREM T14.} $\forall x,\forall y,
((x\,\,{\rm is\,\,even}\,\,\wedge
y\,\,{\rm is\,\,odd}\,\,)\imply x+y\,\,{\rm is\,\,odd}\,\,)$

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Suppose $x$ is even and $y$ is odd. Since $x$ is even, $\exists u,x=2.u$. 
Pick one such $u$ and call it $a$. Since $y$ is odd, $\exists u,y=2.u+1$. 
Pick one such $u$ and call it $b$. Then $x=2a$ and $y=2.b+1$. So
$x+y=2.(a+b)+1$. So $\exists u,x+y=2.u+1$. So $x+y$ is odd.\pend

\bigbreak\noindent{\bf THEOREM T15.} $\forall x,\forall y,
((x\,\,{\rm is\,\,odd}\,\,\wedge
y\,\,{\rm is\,\,odd}\,\,)\imply x+y\,\,{\rm is\,\,even}\,\,)$

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Suppose $x$ and $y$ are odd. Since $x$ is odd, $\exists u,x=2.u+1$. 
Pick one such $u$ and call it $a$. Since $y$ is odd, $\exists u,y=2.u+1$. 
Pick one such $u$ and call it $b$. Then $x=2a+1$ and $y=2.b+1$. So
$x+y=(2.a+1)+(2.b+1)=2.(a+b+1)$. So $\exists u,x+y=2.u$. So $x+y$ 
is even.\pend

\bigbreak\noindent{\bf THEOREM T16.} $\forall x,\forall y,
(x\,\,{\rm is\,\,even}\imply x.y\,\,{\rm is\,\,even}\,\,)$

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary.  Suppose $x$ is
even. Then $\exists u,x=2.u$. Pick one such $u$ and call it $a$.
Then $x=2.a$.  So $x.y=(2.a).y=2.(x.y)$. So 
$\exists u,x.y=2.u$. So $x.y$ is even.\pend

\bigbreak\noindent{\bf THEOREM T17.} $\forall x,\forall y,
((x\,\,{\rm is\,\,odd}\,\,\wedge
y\,\,{\rm is\,\,odd}\,\,)\imply x.y\,\,{\rm is\,\,odd}\,\,)$

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Suppose $x$ and $y$ are odd. Since $x$ is odd, $\exists u,x=2.u+1$. 
Pick one such $u$ and call it $a$. Since $y$ is odd, $\exists u,y=2.u+1$. 
Pick one such $u$ and call it $b$. Then $x=2a+1$ and $y=2.b+1$. So
$x.y=(2.a+1).(2.b+1)=4.a.b+2.a+2.b+1=2(2.a.b+a+b)+1$. 
So $\exists u,x.y=2.u+1$. So $x.y$ is odd.\pend

\bigbreak\noindent{\bf THEOREM T18.} $\forall x,
(x\,\,{\rm is\,\,odd}\,\,\bimply x+1\,\,{\rm is\,\,even}\,\,)$

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. 
Suppose $x$ is odd. Then $\exists u,x=2.u+1$. 
Pick one such $u$ and call it $a$. Then $x+1=(2.a+1)+1=2.(a+1)$.
So $\exists u,x+1=2.u$. So $x+1$ is even.

Now suppose $x+1$ is even. Then $\exists u,x+1=2.u$. 
Pick one such $u$ and call it $a$. Then $x+1=2.a$. Therefore
$x=2.a-1=2.(a-1)+1$. So $\exists u,x=2.u+1$. So $x$ is odd.\pend

\bigbreak\noindent{\bf THEOREM T19.} $\forall x,x\le x$.

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. Then 
$x\le x\bimply(x<x\vee x=x)$ by OA2. But $x=x$, so 
``$x<x\vee x=x$'' is true, and then $x\le x$. \pend

\bigbreak\noindent{\bf THEOREM T20.} $\forall x,\forall y,
(x<y\bimply 0<y-x)$.

\medbreak\noindent{\bf PROOF.} This follows trivially from 
OA6 and D4. \pend

\bigbreak\noindent{\bf THEOREM T21.} $\forall x,\forall y,
(x\le y\bimply 0\le y-x)$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Suppose  $x\le y$. Then $x<y\vee x=y$ by OA2. If $x<y$ then
$0<y+(-x)$ by OA6, and $y+(-x)=y-x$ by D4, so 
$0<y-x$, and then $0\le y-x$ by OA2. If $x=y$ then
$y-x=x-x=x+(-x)=0$, so $\le y-x$, because $0\le 0$ by T19. 
So in both cases ($x<y$ and $x=y$) the conclusion 
$0\le y-x$ follows. Therefore $x\le y\imply 0\le y-x$.

Now suppose $0\le y-x$. Then $0<y-x\vee 0=y-x$ by OA2. 
If $0=y-x$ then 
$$y=y+0=y+(x+(-x))=y+((-x)+x)=(y+(-x))+x$$
$$=(y-x)+x=0+x=x+0=x\,,$$
so $y=x$. Then $x\le y$ by OA2. If $0<y-x$, then $0<y+(-x)$, 
so $x<y$ by OA6, and then $x\le y$ by OA2. 
So in both cases ($0<y-x$ and $0=y-x$) the conclusion 
$x\le y$ follows. Therefore $0\le y-x\imply x\le y$.

Since $x\le y\imply 0\le y-x$ and $0\le y-x\imply x\le y$,
the conclusion $x\le y\imply 0\le y-x$ follows. \pend

\bigbreak\noindent{\bf THEOREM T22.} $\forall x,\forall y,
((0\le x\wedge 0<y)\imply 0<x+y)$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Assume that $0\le x\wedge 0<y$. Then 
$0=x$ or $0<x$ by OA2. If $0=x$ then $x+y=0+y=y+0=y$, so 
the fact that $0<y$ implies that $0<x+y$. If $0<x$ then
OA5 implies $0<x+y$. \pend

\bigbreak\noindent{\bf THEOREM T23.} $\forall x,\forall y,
((0\le x\wedge 0\le y)\imply 0\le x+y)$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Assume that $0\le x\wedge 0\le y$.  If $0<x$ or $0<y$ we can 
use T22 and conclude that $0<x+y$, so $0\le x+y$. 
If $x=0$ and $y=0$ then $x+y=0+0=0$, so $0\le x+y$. \pend

\bigbreak\noindent{\bf THEOREM T24.} $\forall x,\forall y,
\forall z,\forall u,
((x\le y\wedge z<u)\imply x+z<y+u)$.

\medbreak\noindent{\bf PROOF.} Let $x,y,z,u$ be arbitrary. 
Assume that $x\le y\wedge z<u$. Then 
$0\le y-x$ by T20, and $0<u-z$ by T21. 
So $0<(y-x)+(u-z)$ by T22.   But $(y-x)+(u-z)=(y+u)-(x+z)$. 
So $0<(y+u)-(x+z)$, and then $x+z<y+u$ by T14. \pend

\bigbreak\noindent{\bf THEOREM T25.} $\forall x,\forall y,
\forall z,\forall u,
((x\le y\wedge z\le u)\imply x+z\le y+u)$.

\medbreak\noindent{\bf PROOF.} Let $x,y,z,u$ be arbitrary. 
If $x<y$ or $z<u$ then we can apply T24 and conclude
that $x+z<y+u$, so $x+z\le y+u$. 
If $x=y$ and $z=u$ then $x+z=y+u$, so $x+z\le y+u$. \pend

\bigbreak\noindent{\bf THEOREM T26.} 
$\forall x,\forall y,((0\le x\wedge 0\le y)\imply 0\le x.y)$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Assume that $0\le x\wedge 0\le y$.  If both $\neg x=0$ and 
$\neg y=0$, then OA2 implies that $0<x$ and $0<y$, so
$0<x.y$ by OA5, and then $0\le x.y$ by OA2. 
If $x=0\vee y=0$ then $x.y=0$ by T4, so 
$0\le x.y$, because $0\le 0$. \pend

\bigbreak\noindent{\bf THEOREM T27.} 
$\forall x,\forall y,\forall z,
((x\le y\wedge 0\le z)\imply x.z\le y.z)$.

\medbreak\noindent{\bf PROOF.} Let $x,y,z$ be arbitrary. 
Assume that $x\le y\wedge 0\le z$. Then 
$0\le y-x$ by T21.  So $0\le (y-x).z$ by T26. But 
$$(y-x).z=(y+(-x)).z=y.z+(-x).z=y.z+((-1).x).y$$
$$=y.z+(-1).(x.y)=y.z+(-(x.y))=y.z-x.y\,.$$
So $0\le y.z-x.z$, and then T21 tells us that 
$x.z\le y.z$. \pend

\bigbreak\noindent{\bf THEOREM T28.} 
$\forall x,\forall y,(((\neg\, x=0)\wedge\neg\, y=0)\imply(\neg\,x.y=0))$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. 
Assume that $(\neg x=0)\wedge\neg y=0$.  By 
OA7, $0\le x\vee x\le 0$. If $0\le x$, then $0<x$, because
$0<x\vee 0=x$ by OA2, and $\neg 0=x$.  If  
$x\le 0$, then $x<0$, because $x<0\vee x=0$ by OA2, and $\neg x=0$,
and this implies that $0<-x$, because 
OA6 says that $x<0\bimply 0<0+(-x)$, and $0+(-x)=-x$. 
So ``$0<x\vee 0<-x$'' is true if 
$0\le x$ and also if $x\le 0$. Since $0\le x\vee x\le 0$, 
we have established that $0<x\vee 0<-x$. Similarly,
$0<y\vee 0<-y$. 

So one of the following four possibilities hold:
\begin{itemize}
\item[(1)] $0<x\wedge 0<y$,
\item[(2)] $0<x\wedge 0<-y$,
\item[(3)] $0<-x\wedge 0<y$,
\item[(4)] $0<-x\wedge 0<-y$.
\end{itemize}
If (1) holds, then $0<x.y$ by OA5. Therefore $\neg x.y=0$, because
if $x.y=0$ it would follow that $0<0$, contradicting OA8. 

If (2) holds, then $0<x.(-y)$ by OA5. Therefore $\neg x.(-y)=0$, because
if $x.(-y)=0$ it would follow that $0<0$, contradicting OA8.  Then
$\neg x.y =0$, because if $x.y=0$ we would have
$x.(-y)=x.((-1).y)=(x.(-1)).y=((-1).x).y)=
(-1).(x.y)=-(x.y)=-0=0$, contradicting the fact that 
$\neg x.(-y)=0$.

Cases (3) and (4) are handled similarly. \pend

\bigbreak\noindent{\bf THEOREM T29.} $\forall x,\forall y,
((x\le y\wedge y\le x)\imply x=y)$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary. Suppose
$x\le y\wedge y\le x$. We prove that $x=y$ by contradiction.
Suppose $\neg x=y$. Then OA2 tells us that 
$x<y\vee x=y$. Since $\neg x=y$, we have $x<y$. Then 
OA6 and D4 imply that $0<y-x$. Similarly, $0< x-y$.
Then OA4 implies that $0<(y-x)+(x-y)$, and a simple
calculation shows that $(y-x)+(x-y)=0$. So
$0<0$, contradicting OA8. \pend

\bigbreak\noindent{\bf THEOREM T30.} $\forall x,\forall y,\forall z,
((x\le y\wedge y\le z)\imply x\le z)$.

\medbreak\noindent{\bf PROOF.} Let $x,y,z$ be arbitrary. Suppose
$x\le y\wedge y\le z$. Then $0\le y-x$ and $0\le z-y$ by T21. 
So $0\le(y-x)+(z-y)$ by T23. But 
$(y-x)+(z-y)=z-x$. So $0\le z-x$, and then T21 implies $x\le z$.\pend

\bigbreak\noindent{\bf THEOREM T31.} $0<1$.

\medbreak\noindent{\bf PROOF.} OA7 tells us that $0\le 1\vee 1\le 0$. 
We consider separately the two cases $0\le 1$ and $1\le 0$, and show
that $0<1$ in each case.

First suppose that $0\le 1$. Then $0<1\vee 0=1$ by OA2. But $\neg 0=1$
by IDA10.  So $0<1$, as desired.

Now suppose that $1\le 0$. Then $1<0\vee 1=0$ by OA2. But $\neg 1=0$
by IDA10. So $1<0$. But OA6 tells us that $1<0\bimply 0<0+(-1)$. 
So  $0<0+(-1)$, and then $0<-1$. It then follows from OA4 that
$0<(-1).(-1)$. But $(-1).(-1)=1$ by T6. So $0<1$, as desired. \pend

\bigbreak\noindent{\bf THEOREM T32.} $-1<0$.

\medbreak\noindent{\bf PROOF.} OA6 implies that 
$-1<0\bimply 0<0+(-(-1))$. But $-(-1)=1$ by T9. So 
$-1<0\bimply 0<1$. Since $0<1$ by T31, we have $-1<0$.\pend

\bigbreak\noindent{\bf THEOREM T33.} $0<2$.

\medbreak\noindent{\bf PROOF.} Since $0<1$ by T31, OA5 implies that
$0<1+1$, i.e., that $0<2$. \pend

\bigbreak\noindent{\bf THEOREM T34.} $2\neq 0$.

\medbreak\noindent{\bf PROOF.} Since $0<2$ by T33, 
OA8 implies that $2\neq 0$, because if $2=0$ then 
``$0=0$'' would be true, contradicting OA8.\pend

\bigbreak\noindent{\bf THEOREM T35.} $\forall x,(x\le 0\vee 1\le x)$.

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. Suppose
$\neg x\le 0$. We will prove that $1\le x$. 

By OA7, $x\le 0\vee 0\le x$. Since $\neg x\le 0$, we have 
$0\le x$. Therefore $0=x\vee 0<x$ by OA2. But ``$0=x$'' isn't true,
because if $0=x$ it would follow that $x\le 0$, and we are assuming that
$\neg x\le 0$.  So $0<x$.

We want to prove that $1\le x$. We do it by contradiction, Suppose
$\neg 1\le x$. By OA7, $1\le x\vee x\le 1$. Since 
$\neg 1\le x$, we have $x\le 1$. Therefore $x=1\vee x<1$ by OA2. 
But ``$x=1$'' isn't true, because if $x=1$ it would follow that 
$x\le 1$, and we are assuming that
$\neg 1\le x$.  So $x<1$.

We have shown that $0<x\wedge x<1$. Let $p(u)$ be the statement
$u<1$. Then we have shown that $0<x\wedge p(x)$ is true,
so $\exists u,(0<u\wedge p(u))$ is true. By the WOP,
there exists a smallest $y$ such that $0<y\wedge p(y)$. That is,
$$
\exists y,(0<y\wedge y<1\wedge\forall u,((0<u\wedge u<1)\imply y\le u))\,.
$$
Pick such a $y$ and call it $a$. Then
\begin{equation}\label{uuu}
0<a\wedge a<1\wedge\forall u,((0<u\wedge u<1)\imply a\le u)\,.
\end{equation}
Since $0<a$, OA5 implies that $0<a.a$. On the other hand,
$a<1$ implies that $0<1-a$ by T20. Since $0<a$, we have 
$0<a.(1-a)$ by OA5. That is, $0<a-a.a$. Therefore
T20 tells us that $a.a<a$. In particular, $a.a<1$, because $a<1$.

On the other hand, (\ref{uuu}) implies 
$$
\forall u,((0<u\wedge u<1)\imply a\le u)\,,
$$
and then we can specialize to $u=a.a$, and get
$$
(0<a.a\wedge a.a<1)\imply a\le a.a\,.
$$
Since ``$0<a.a\wedge a.a<1$'' is true, we can conclude
that $a\le a.a$. But this contradicts the fact that 
$a.a<a$. (If $a\le a.a$ and $a.a<a$, then 
$0\le a.a-a$ by T21, and $0<a-a.a$ by OA6, so 
$0<(a.a-a)+(a-a.a)$ by T18, and then $0<0$, contradicting
OA8.) 

So the assumption that $\neg 1\le x$ has led us to a contradiction.
Hence $1\le x$. \pend

\bigbreak\noindent{\bf THEOREM T36.} $\forall x,\forall y,
(x\le y\vee y+1\le x)$.

\medbreak\noindent{\bf PROOF.} Let $x,y$ be arbitrary.  Suppose
$\neg{}x\le y$. Using T35, we find that $x-y\le 0\vee 1\le x-y$.  If
$x-y\le 0$, then T25 would imply $x\le y$, contradicting the
assumption that $\neg x\le y$. So $\neg x-y\le 0$. Therefore
$1\le x-y$.  Then T25 implies $y+1\le x$. \pend

\bigbreak\noindent{\bf THEOREM T37.} $\forall x,(x\le 0\vee x=1\vee
2\le x)$.

\medbreak\noindent{\bf PROOF.} Let $x$ be arbitrary. 
Suppose $\neg x\le 0$. Then T35 implies $1\le x$, and T36 implies
$x\le 1\vee 1+1\le x$. If $x\le 1$, then T29 implies $x=1$, since
$1\le x$ and $x\le 1$. If $1+1\le x$, then $2\le x$.\pend


\bigbreak\noindent{\bf THEOREM T38.} $\forall x,
(x\,\,{\rm is\,\,even}\,\,\vee\,\,x\,\,{\rm is\,\,odd})$.

\medbreak\noindent{\bf PROOF.} Let $q(u)$ be the statement ``$0\le
u\wedge(u\,\,{\rm is\,\,even}\,\,\vee\,\,u\,\,{\rm is\,\,odd})$''.
Let $p(u)$ be the statement $\neg q(u)$. We will prove that $q(u)$
is true for all $u$ such that $0\le u$. We do this by contradiction
Suppose $\forall u,(0\le u\imply q(u))$ was not true. Then $\exists
u,(0\le u\wedge p(u))$. By the WOP, there exists a smallest $u$ such
that $p(u)$. That is,
$$
\exists u,\Bigl(0\le u\wedge p(u)\wedge\forall v,
((0\le v\wedge p(v))\imply u\le v)\Bigr)\,.
$$
Pick one such $u$ and call it $s$. Then 
$$
0\le s\wedge\neg\,\Bigl(s\,\,{\rm is\,\,even}\,\,\vee\,\,s\,\,{\rm is\,\,
odd}\Bigr)\,\,,
$$
and $s\le v$ for every $v$ such that $0\le v$ and $v$ is neither even nor
odd. 

It follows that $\neg\,s= 0$, because $0$ is even, so if $s=0$ then
``$s\,\,{\rm is\,\,even}\,\,\vee\,\,s\,\,{\rm is\,\,
odd}$''would be true. Since $0\le s$, OA2 implies that $0<s$.



\end{document}
 
