\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{../lib/tex/naproche}

\title{Square roots of primes are irrational}
\author{}
\date{}

\begin{document}

  \maketitle

  \section*{(Strictly) positive rational numbers}

  \begin{forthel}
    [synonym number/-s]
    [synonym divide/-s]

    \begin{signature}
      A positive rational number is an object.
    \end{signature}

    Let $q, s, r$ stand for positive rational numbers.

    \begin{signature}
      $r \cdot q$ is a positive rational number.
    \end{signature}

    \begin{axiom}
      $r \cdot q = q \cdot r$.
    \end{axiom}

    \begin{axiom}
      $r \cdot (q \cdot s) = (r \cdot q) \cdot s$.
    \end{axiom}

    \begin{definition}
      $q$ is left cancellative iff
      for all $r, s$ if $q\cdot s = q\cdot r$ then $s = r$.
    \end{definition}

    \begin{axiom}
      Every positive rational number is left cancellative.
    \end{axiom}
  \end{forthel}

  \section*{Natural numbers}

  \begin{forthel}
    \begin{signature}
      A natural number is a positive rational number.
    \end{signature}

    Let $m, n, k$ denote natural numbers.

    \begin{signature}
        $1$ is a natural number.
    \end{signature}

    \begin{axiom}
      $n \cdot m$ is a natural number.
    \end{axiom}

    \begin{definition}
      $n \mid m$ iff there exists $k$ such that $k \cdot n = m$.
    \end{definition}

    Let $n$ divides $m$ stand for $n \mid m$.
    Let a divisor of $m$ stand for a natural number that divides $m$.
  \end{forthel}

  \section*{Prime numbers}

  \begin{forthel}
    \begin{definition}
      Let $p$ be a natural number.
      $p$ is prime iff $p\neq 1$ and for all $m, n$
      if $p\mid n\cdot m$ then $p \mid n$ or $p \mid m$.
    \end{definition}

    Let a prime number stand for a prime natural number.

    Let $p$ denote a prime number.

    \begin{definition}
      $n$ and $m$ are coprime iff $n$ and $m$ have no common prime divisor.
    \end{definition}

    \begin{axiom}
      There exist coprime $m,n$ such that $m \cdot q = n$.
    \end{axiom}

    Let $q^{2}$ stand for $q \cdot q$.

    \begin{proposition}
      $q^{2} = p$ for no positive rational number $q$.
    \end{proposition}
    \begin{proof}[by contradiction]
      Assume the contrary.
      Take a positive rational number $q$ such that $p = q^{2}$.
      Take coprime $m,n$ such that $m \cdot q = n$.
      Then $p \cdot m^{2} = n^{2}$.
      Therefore $p$ divides $n$.
      Take a natural number $k$ such that $n = k \cdot p$.
      Then $p \cdot m^{2} = p \cdot (k \cdot n)$.
      Therefore $m \cdot m$ is equal to $p \cdot k^{2}$.
      Hence $p$ divides $m$.
      Contradiction.
    \end{proof}
  \end{forthel}

\end{document}
