MHB Proving Properties of Multiplication for Natural Numbers

[evinda]

Hello! (Wave)

For each pair of natural numbers $m \in \omega, n \in \omega$ we define the multiplication between $m,n$ (as a function $\cdot: \omega \times \omega \to \omega $) like that:

$$m \cdot 0=0$$
$$m \cdot n'=m \cdot n+m$$

I want to show that for each $m \in \omega, n \in \omega, k \in \omega$ the following properties are satisfied:

• $m \cdot n=n \cdot m$
• $(m \cdot n) \cdot k=m \cdot (n \cdot k)$
• $(m+n) \cdot k=m\cdot k+n \cdot k$
• $1 \cdot n=n$
• If $k \neq 0$ and $n \cdot k=m \cdot k$ then $n=m$.

In order to prove the first sentence we have to show that $0 \cdot m=0$, $n' \cdot m=m \cdot n'$ and that $m \cdot n=n \cdot m$, right?In order to prove that $0 \cdot m=0$ I tried the following:

For $m=0: 0 \cdot 0=0 \checkmark$

We suppose a $m$ such that $0 \cdot m=0$.

We want to show that $0 \cdot m'=0$.

$0 \cdot m'=0 \cdot m+0 \overset{\text{induction hypothesis}}{=}0$.

Therefore, $0 \cdot m=0$, for any $m \in \omega$.Then we want to show that $n' \cdot m=m \cdot n'$.

For $m=0$: $n' \cdot 0 \overset{\text{definition}}{=}0 \overset{\text{previous sentence}}{=}0 \cdot n' \checkmark$We suppose a $m$ such that $n' \cdot m=m \cdot n'$ for all $n \in \omega$.We want to show that $n' \cdot m'=m' \cdot n'$.

$n' \cdot m'=n' \cdot m+n'=m \cdot n'+n'$How could we continue? (Thinking)

 

[Evgeny.Makarov]

In order to prove the first sentence we have to show that $0 \cdot m=0$, $n' \cdot m=m \cdot n'$ and that $m \cdot n=n \cdot m$, right?

I would prove $0 \cdot m=0$ and
\[
n'm=nm+m\qquad(*)
\]
by induction on $m$. The equality (*) is used in the inductive step of proving $mn=nm$ by induction on $n$. Indeed,
\[
mn'\overset{\text{def}}{=}mn+m\overset{\text{IH}}{=}nm+m\overset{(*)}{=}n'm.
\]

 

[evinda]

Is it right like that?

We will show that $0 \cdot m=0$.
For $m=0: 0 \cdot 0 \overset{\text{definition}}{=}0$
We suppose a $m$ such that $0 \cdot m=0$.
We will show that $0 \cdot m'=0$.
$0 \cdot m'=0 \cdot m+0 \overset{\text{ind. hypothesis}}{=}0+0=0$
$$$$

We will prove that $m \cdot n=n \cdot m$.

For $m=0: 0 \cdot n=0=n \cdot 0 \checkmark$

We suppose a $m$ such that $\forall n \in \omega: m \cdot n=n \cdot m$.

We will show $m' \cdot n=n \cdot m', \forall n \in \omega$
.
For $n=0: m' \cdot 0 \overset{\text{definition}}{=} 0 \overset{\text{above proposition}}{=} 0 \cdot m'$

Let $n$ such that $m' \cdot n=n \cdot m'$.

We will show that $m' \cdot n'=n' \cdot m'$.

$$m' \cdot n'=m' \cdot n+m' \overset{\text{ind. hypothesis}}{=}n \cdot m'+m'=n \cdot m+n+m' \overset{\star \star }{=} n \cdot m+n'+m \\ =(n \cdot m+m)+n'=n' \cdot m+n'=n' \cdot m'$$$$\star \star: $$

We will show that $n+m'=n'+m$.

For $m=0$: $n+m'=n+0'=(n+0)'=n'=n'+0=n'+m$

Let $m$ such that $n+m'=n'+m$.

We will show that $n+m''=n'+m'$.

$n+m''=(n+m')' \overset{\text{ind. hypothesis}}{=} (n'+m)' \overset{\text{definition}}{=} n'+m'$

 

[Evgeny.Makarov]

We will show that $m' \cdot n'=n' \cdot m'$.

$$m' \cdot n'=m' \cdot n+m' \overset{\text{ind. hypothesis}}{=}n \cdot m'+m'=n \cdot m+n+m' \overset{\star \star }{=} n \cdot m+n'+m \\ =(n \cdot m+m)+n'=n' \cdot m+n'=n' \cdot m'$$

Note that $nm+m=n'm$ (second last equality) is not an instance of definition. You could justify it as follows.
\begin{align}
nm+m&=mn+m&&\text{external induction hypothesis (on }m)\\
&=mn'&&\text{definition}\\
&=n'm&&\text{external induction hypothesis}.
\end{align}

We will show that $n+m'=n'+m$.

You used other properties of addition, including commutativity and associativity. It is not clear why you are proving this particular fact and not others.

 

[evinda]

Note that $nm+m=n'm$ (second last equality) is not an instance of definition. You could justify it as follows.
\begin{align}
nm+m&=mn+m&&\text{external induction hypothesis (on }m)\\
&=mn'&&\text{definition}\\
&=n'm&&\text{external induction hypothesis}.
\end{align}

I see... (Nod)

You used other properties of addition, including commutativity and associativity. It is not clear why you are proving this particular fact and not others.

I didn't prove the other properties because they are given at the proposition of my other thread about addition. (Blush) I tried to show like that that $(m \cdot n) \cdot k=m \cdot (n \cdot k)$:
For $k=0: (m \cdot n) \cdot 0 \overset{definition}{=}0=m \cdot (n \cdot 0)=m \cdot 0=0$

Let $k$ such that $(m \cdot n) \cdot k=m \cdot (n \cdot k)$.We will show that $(m \cdot n) \cdot k'=m \cdot (n \cdot k')$.

$(m \cdot n) \cdot k' \overset{definition}{=} (m \cdot n)k +(m \cdot n) \overset{ind. hypothesis}{=} m \cdot (n \cdot k)+(m \cdot n) \overset{\star}{=} m \cdot (n \cdot k+n)\\=m \cdot (n \cdot k')$$$\star:$$

We will show that $m \cdot (n \cdot k)+(m \cdot n)=m \cdot (n \cdot k+n)$For $m=0: 0 \cdot (n \cdot k)+(0 \cdot n)=0= 0 \cdot (n \cdot k+n) \checkmark$Let $m$ such that $m \cdot (n \cdot k)+(m \cdot n)=m \cdot (n \cdot k+n), \forall n,k \in \omega$

We will show that $m' \cdot (n \cdot k)+(m' \cdot n)=m' \cdot (n \cdot k+n)$$m' \cdot (n \cdot k)+(m' \cdot n)=m \cdot (n \cdot k)+(n \cdot k)+m \cdot n+n=m \cdot (n \cdot k)+m \cdot n+(n \cdot k)+n \overset{ind. hypothesis}{=} m \cdot (n \cdot k+n)+(n \cdot k)+n=m' \cdot (n \cdot k+n)$

Am I right? (Smile)