TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Euler's product formula $\varphi(n)=n\prod_{p\mid n}(1-1/p)=\prod_{p^k\parallel n}(p^k-p^{k-1})$ for $n\ge1$ , stated through a finite injective list of its prime divisors

Statement

Let $n\ge1$ , and let $p_0,\ldots,p_{r-1}$ be an injective finite list consisting exactly of the prime divisors of $n$ . Put $k_i:=v_{p_i}(n)$ , so $k_i\ge1$ . Then

$\varphi(n)=\prod_{i<r}\bigl(p_i^{k_i}-p_i^{k_i-1}\bigr).$

After carrying the natural numbers into $\mathbb Q$ , the same identity is

$\varphi(n)=n\prod_{i<r}\left(1-\frac1{p_i}\right).$

At $n=1$ the list is empty, both products are empty products equal to $1$ , and $\varphi(1)=1$ . These finite-list formulas are the precise meanings of the two products displayed in the title.

Facts & Assumptions

Given: A positive integer $n$ and an injective finite list $p_0,\ldots,p_{r-1}$ consisting exactly of its prime divisors; $k_i:=v_{p_i}(n)$ .

[L1]

A class modulo $n$ is a unit exactly when its representative is coprime to $n$ , and $\varphi(n)$ counts the unit classes (For $n\ge1$ , $[a]_n$ is a unit if and only if $\gcd(a,n)=1$ , The unit group $(\mathbb{Z}/n)^\times$ and Euler's totient $\varphi(n)=\lvert(\mathbb{Z}/n)^\times\rvert$ for $n\ge1$ ).

[L2]

The standard representatives form a set $X$ of cardinality $n$ (For $n\ge 1$ , every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$ , so $\lvert\mathbb{Z}/n\rvert=n$ ; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$ , The cardinality $\lvert A\rvert$ of a finite set).

[L3]

Inclusion-exclusion gives the cardinality of the complement of a finite union as the alternating sum of the cardinalities of all intersections, with the empty intersection equal to the ambient finite set (A finite family $(A_i)_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_J$ for $J \subseteq I$ , and the convention $A_\varnothing = X$ , Inclusion and exclusion: $\iota\lvert\bigcup_{i \in I} A_i\rvert = \sum_{\varnothing \ne J \subseteq I}(-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert$ , together with the complementary form counting the elements in none of the $A_i$ ).

[L4]

The canonical prime factorisation is $n=\prod_{i<r}p_i^{k_i}$ , and $p_i\mid n$ implies $k_i\ge1$ (For $n \ge 1$ and any injective list $p : r \to \mathbb{Z}$ of primes containing every prime divisor of $n$ , one has $n = \prod_{i<r} p_i^{\,v_{p_i}(n)}$ ; the exponents are determined by $n$ , and $v_q(n) = 0$ for every prime $q$ outside the list, The $p$ -adic valuation $v_p(a)$ of a nonzero integer: the greatest $k \in \mathbb{N}$ with $p^{k} \mid a$ , For a prime $p$ and a nonzero integer $a$ : $p^{v_p(a)} \mid a$ and $p^{v_p(a)+1} \nmid a$ ; $p^{k} \mid a$ holds exactly for $k \le v_p(a)$ ; $v_p(a) \ge 1$ exactly when $p \mid a$ ; $v_p(1) = v_p(-1) = 0$ ; and $v_p(p) = 1$ ).

[L5]

A product of pairwise-coprime positive integers divides every common multiple of its factors (For a finite pairwise-coprime list of positive integers, the product divides every common multiple, and each initial product is coprime to every remaining modulus).

[L6]

Natural finite products have empty value $1$ and obey the successor recursion (Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$ ); the integers embed injectively in the field $\mathbb Q$ , which in turn embeds injectively as an ordered subfield of $\mathbb R$ (The integers embed in the rationals, The rationals form a field, The rationals embed densely in the reals).

[L7]

Induction is valid on natural numbers (The principle of mathematical induction).

[L8]

Distinct primes are coprime: a prime not dividing another prime is coprime to it (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ , For a prime $p$ and any integer $a$ , $\gcd(p,a)$ is $p$ when $p \mid a$ and $1$ otherwise; so $p \nmid a$ makes $p$ and $a$ coprime).

[L9]

Every integer greater than $1$ has a prime divisor (Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime).

[L10]

Multiplication by a nonzero integer is cancellative (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct

1.1

For $i<r$ , let $A_i:=\{a\in X:p_i\mid a\}$ . Since the $p_i$ are distinct primes, they are pairwise coprime by [L8]. For $J\subseteq\{0,\ldots,r-1\}$ put $q_J:=\prod_{j\in J}p_j$ , with $q_\varnothing=1$ . By [L5], the intersection $A_J$ consists exactly of the standard representatives divisible by $q_J$ .

L2L5L8

1.2

A representative $a\in X$ lies outside every $A_i$ exactly when no prime divisor of $n$ divides $a$ . This is equivalent to $\gcd(a,n)=1$ : a common divisor greater than $1$ would have a prime divisor by [L9], and every such prime would occur in the list. Therefore $X\setminus\bigcup_iA_i$ is precisely the set of unit representatives and has cardinality $\varphi(n)$ .

L1L4L9

1.3

By [L4], $n=\prod_{i<r}p_i^{k_i}$ . In $\mathbb Q$ , finite distributivity and $k_i\ge1$ give $p_i^{k_i}(1-1/p_i)=p_i^{k_i}-p_i^{k_i-1}$ for each $i$ , hence $n\prod_{i<r}(1-1/p_i)=\prod_{i<r}(p_i^{k_i}-p_i^{k_i-1})$ .

L4L6

2.1

The integer $q_J$ divides $n$ by [L4]. Multiplication by $q_J$ bijects the integers $t$ with $0\le t<n/q_J$ onto $A_J$ : its values lie between $0$ and $n-1$ , every member of $A_J$ has the required quotient, and [L10] gives injectivity. Hence $|A_J|=n/q_J$ .

step 1.1L2L4L10

3.1

Inclusion-exclusion applied to steps 1.1, 2.1 and 1.2 gives this equality after embedding its integer and rational terms in $\mathbb R$ . Both sides come from $\mathbb Q$ , and the ordered-field embedding $\mathbb Q\to\mathbb R$ is injective by [L6], so already in $\mathbb Q$ one has $\varphi(n)=\sum_{J\subseteq\{0,\ldots,r-1\}}(-1)^{|J|}n/q_J$ .

step 1.1step 2.1step 1.2L3L6

4.1

Finite distributivity gives $\prod_{i<r}(1-1/p_i)=\sum_J(-1)^{|J|}/q_J$ : the empty case reads $1=1$ , and adjoining $p_r$ replaces every old term $1/q_J$ by the pair $1/q_J$ and $-1/(q_Jp_r)$ , indexed respectively by subsets not containing and containing $r$ . Multiplying this identity by $n$ and using step 3.1 yields $\varphi(n)=n\prod_{i<r}(1-1/p_i)$ .

step 3.1L6L7

5.1

Combining steps 4.1 and 1.3 proves both formulas. When $n=1$ , there are no prime divisors, so the list is empty; the products equal $1$ by [L6], and $\varphi(1)=1$ by [L1].

step 4.1step 1.3L1L6∎

Remarks

The same prime-power product also follows by repeatedly applying Euler's totient is multiplicative: $\gcd(m,n)=1$ implies $\varphi(mn)=\varphi(m)\varphi(n)$ for positive $m,n$ to the canonical factorisation and using For a prime $p$ and $k\ge1$ , $\varphi(p^k)=p^k-p^{k-1}$ . The proof above instead exposes the inclusion-exclusion count behind the factor $1-1/p_i$ .

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 164 results over 35 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Mathematics LibreTexts, Euler's phi Function (standard reference, not scraped)
K. Conrad, The Chinese Remainder Theorem (standard reference, not scraped)
Carnegie Mellon, number-theory lecture notes (standard reference, not scraped)

Euler's product formula φ(n)=n∏p∣n(1−1/p)=∏pk∥n(pk−pk−1)\varphi(n)=n\prod_{p\mid n}(1-1/p)=\prod_{p^k\parallel n}(p^k-p^{k-1})φ(n)=n∏p∣n​(1−1/p)=∏pk∥n​(pk−pk−1) for n≥1n\ge1n≥1, stated through a finite injective list of its prime divisors