Metamath Proof Explorer

Theorem phibnd

Description: A slightly tighter bound on the value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Assertion	phibnd	$⊢ N \in ℤ_{\geq 2} \to ϕ (N) \leq N - 1$

Proof

Step	Hyp	Ref	Expression
1		fzfi	$⊢ (1 \dots N - 1) \in Fin$
2		phibndlem	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N - 1)$
3		ssdomg	$⊢ (1 \dots N - 1) \in Fin \to (\{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N - 1) \to \{x \in (1 \dots N) \| x \gcd N = 1\} ≼ (1 \dots N - 1))$
4	1 2 3	mpsyl	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} ≼ (1 \dots N - 1)$
5		fzfi	$⊢ (1 \dots N) \in Fin$
6		ssrab2	$⊢ \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N)$
7		ssfi	$⊢ ((1 \dots N) \in Fin \land \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N)) \to \{x \in (1 \dots N) \| x \gcd N = 1\} \in Fin$
8	5 6 7	mp2an	$⊢ \{x \in (1 \dots N) \| x \gcd N = 1\} \in Fin$
9		hashdom	$⊢ (\{x \in (1 \dots N) \| x \gcd N = 1\} \in Fin \land (1 \dots N - 1) \in Fin) \to (\|\{x \in (1 \dots N) \| x \gcd N = 1\}\| \leq \|(1 \dots N - 1)\| \leftrightarrow \{x \in (1 \dots N) \| x \gcd N = 1\} ≼ (1 \dots N - 1))$
10	8 1 9	mp2an	$⊢ \|\{x \in (1 \dots N) \| x \gcd N = 1\}\| \leq \|(1 \dots N - 1)\| \leftrightarrow \{x \in (1 \dots N) \| x \gcd N = 1\} ≼ (1 \dots N - 1)$
11	4 10	sylibr	$⊢ N \in ℤ_{\geq 2} \to \|\{x \in (1 \dots N) \| x \gcd N = 1\}\| \leq \|(1 \dots N - 1)\|$
12		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
13		phival	$⊢ N \in ℕ \to ϕ (N) = \|\{x \in (1 \dots N) \| x \gcd N = 1\}\|$
14	12 13	syl	$⊢ N \in ℤ_{\geq 2} \to ϕ (N) = \|\{x \in (1 \dots N) \| x \gcd N = 1\}\|$
15		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
16		hashfz1	$⊢ N - 1 \in ℕ_{0} \to \|(1 \dots N - 1)\| = N - 1$
17	12 15 16	3syl	$⊢ N \in ℤ_{\geq 2} \to \|(1 \dots N - 1)\| = N - 1$
18	17	eqcomd	$⊢ N \in ℤ_{\geq 2} \to N - 1 = \|(1 \dots N - 1)\|$
19	11 14 18	3brtr4d	$⊢ N \in ℤ_{\geq 2} \to ϕ (N) \leq N - 1$