Biconditional proof of odd factors and product

Question

EDIT 1: Thanks @coffeemath for pointing out my mistake of defining both m and n in terms of k. They now each have their own respective constants for the Even and Odd forms.

EDIT 2: Fixed a typo

---

I'm trying to get my first proof down using quantifiers and math (or actual numbers) involved.

I have just a few questions:

• Is the claim section a correct representation of what's asking to be proved? (i.e. notation, binding order, etc)
• Is the structure of this proof clear?
• Is the proof itself sound?

Any other feedback is appreciated, but I'm really just aiming for the correct fundamentals before moving to anything advanced or applying optimizations.

Thanks,

Prove

Let m,n denote any two natural numbers. Prove that mn is odd iff m and n are odd.

Claim

$(\forall m\in\mathbb{N})(\forall n\in\mathbb{N})[(Odd(m) \wedge Odd(n)) \iff Odd(mn)]$

Definitions

Even: A natural number with the form $2k$

Odd: A natural number with the form $2k + 1$

Proof

$\Rightarrow$ $(Odd(m) \wedge Odd(n)) \iff Odd(mn)$

1. Assume both $m$ and $n$ are odd.
2. We can write $mn$ as $(2a+1)(2b+1)$
3. $(2a+1)(2b+1) = 4ab + 2a + 2b + 1$
4. $4ab + 2a + 2b + 1 = 2(2ab + a + b) + 1$
5. Note that $2(2ab + a + b) + 1$ has the Odd form.
6. $\therefore (Odd(m) \wedge Odd(n)) \implies Odd(mn)$

$\Leftarrow$ $Odd(mn) \implies (Odd(m) \wedge Odd(n))$

1. We will prove the contrapositive: $(Even(m) \lor Even(n)) \implies Even(mn)$
2. WLOG: Assume $m$ is even.
3. We can write $mn$ as $(2a)(n)$
4. $(2a)(n) = 2(an)$
5. Note that $2(an)$ has the Even form.
6. $\therefore (Even(m) \lor Even(n)) \implies Even(mn)$