[proofplan] We prove the two implications separately. If $n$ is prime, then its only positive divisors are $1$ and $n$, while every prime $p \le \sqrt n$ is strictly smaller than $n$, so such a $p$ cannot divide $n$. Conversely, we prove the contrapositive: if $n$ is not prime, choose the least divisor $a > 1$ of $n$; minimality forces $a$ to be prime, and comparing the complementary factor shows $a \le \sqrt n$. [/proofplan] [step:Exclude small prime divisors when $n$ is prime] Assume that $n$ is prime. Let $p \in \mathbb{N}$ be a [prime number](/page/Prime%20Number) with $p \le \sqrt n$. Since $n \ge 2$, we have $n < n^2$. Because both $n$ and $\sqrt n$ are non-negative [real numbers](/page/Real%20Numbers), taking square roots gives $\sqrt n < n$. Hence $p < n$. If $p \mid n$, then $p$ is a positive divisor of the prime number $n$. Therefore $p \in \{1,n\}$. Since $p$ is prime, $p \ge 2$, so $p \ne 1$; since $p < n$, we also have $p \ne n$. This contradiction shows that no prime $p \le \sqrt n$ divides $n$. [/step] [step:Choose the least non-trivial divisor when $n$ is not prime] We prove the reverse implication by contrapositive. Assume that $n$ is not prime. Since $n \ge 2$, the definition of primality gives a divisor $d \in \mathbb{N}$ of $n$ such that $1 < d < n$. Define the set of non-trivial positive divisors of $n$ by \begin{align*} D := \{d \in \mathbb{N} : d \mid n \text{ and } d > 1\}. \end{align*} The set $D$ is non-empty because it contains the divisor just chosen. By the [well-ordering principle](/theorems/721) for $\mathbb{N}$, let $a \in D$ be the least element of $D$. Thus $a \mid n$ and $a > 1$. Since $a \mid n$, there exists $b \in \mathbb{N}$ such that \begin{align*} n = ab. \end{align*} Because $a < n$, the equality $n = ab$ gives $b > 1$. [guided] The purpose of choosing the least divisor greater than $1$ is to manufacture a prime divisor of $n$ without citing any external factorisation theorem. Since $n$ is not prime and $n \ge 2$, there is some positive divisor of $n$ strictly between $1$ and $n$. We collect all divisors of $n$ greater than $1$ in the set \begin{align*} D := \{d \in \mathbb{N} : d \mid n \text{ and } d > 1\}. \end{align*} This set is non-empty, so the well-ordering principle for $\mathbb{N}$ supplies a least element $a \in D$. By membership in $D$, the integer $a$ satisfies $a \mid n$ and $a > 1$. The divisibility relation $a \mid n$ means exactly that there exists $b \in \mathbb{N}$ with \begin{align*} n = ab. \end{align*} Also $a < n$ because our original non-trivial divisor can be chosen below $n$, and the least such divisor cannot equal $n$. Therefore $b \ne 1$, so $b > 1$. [/guided] [/step] [step:Show the least non-trivial divisor is prime] We claim that $a$ is prime. Suppose, toward a contradiction, that $a$ is not prime. Since $a > 1$, there exist $r,s \in \mathbb{N}$ such that \begin{align*} a = rs \end{align*} with $1 < r < a$. Since $a \mid n$ and $r \mid a$, transitivity of divisibility gives $r \mid n$. Thus $r \in D$. But $1 < r < a$, contradicting the minimality of $a$ in $D$. Hence $a$ is prime. [/step] [step:Bound the least prime divisor by $\sqrt n$] We next show that $a \le \sqrt n$. If $b < a$, then $b \mid n$ because $n = ab$, and we already have $b > 1$. Thus $b \in D$, contradicting the minimality of $a$ because $b < a$. Therefore $a \le b$. Multiplying the inequality $a \le b$ by the positive integer $a$ gives \begin{align*} a^2 \le ab = n. \end{align*} Both $a$ and $\sqrt n$ are non-negative real numbers. Since $\sqrt n$ is the non-negative real number whose square is $n$, the inequality $a^2 \le n$ implies \begin{align*} a \le \sqrt n. \end{align*} [/step] [step:Conclude the contrapositive] We have shown that if $n$ is not prime, then there exists a prime number $a \in \mathbb{N}$ such that $a \mid n$ and $a \le \sqrt n$. This is exactly the negation of the condition that no prime $p \le \sqrt n$ divides $n$. Therefore, if no prime $p \le \sqrt n$ divides $n$, then $n$ must be prime. Combining this with the forward implication proves the equivalence. [/step]