phibndlem

		Ref	Expression
	Assertion	phibndlem	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N - 1)$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
2		fzm1	$⊢ N \in ℤ_{\geq 1} \to (x \in (1 \dots N) \leftrightarrow (x \in (1 \dots N - 1) \lor x = N))$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4	2 3	eleq2s	$⊢ N \in ℕ \to (x \in (1 \dots N) \leftrightarrow (x \in (1 \dots N - 1) \lor x = N))$
5	4	biimpa	$⊢ (N \in ℕ \land x \in (1 \dots N)) \to (x \in (1 \dots N - 1) \lor x = N)$
6	5	ord	$⊢ (N \in ℕ \land x \in (1 \dots N)) \to (\neg x \in (1 \dots N - 1) \to x = N)$
7	1 6	sylan	$⊢ (N \in ℤ_{\geq 2} \land x \in (1 \dots N)) \to (\neg x \in (1 \dots N - 1) \to x = N)$
8		eluzelz	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ$
9		gcdid	$⊢ N \in ℤ \to N \gcd N = \|N\|$
10	8 9	syl	$⊢ N \in ℤ_{\geq 2} \to N \gcd N = \|N\|$
11		nnre	$⊢ N \in ℕ \to N \in ℝ$
12		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
13	12	nn0ge0d	$⊢ N \in ℕ \to 0 \leq N$
14	11 13	absidd	$⊢ N \in ℕ \to \|N\| = N$
15	1 14	syl	$⊢ N \in ℤ_{\geq 2} \to \|N\| = N$
16	10 15	eqtrd	$⊢ N \in ℤ_{\geq 2} \to N \gcd N = N$
17		1re	$⊢ 1 \in ℝ$
18		eluz2gt1	$⊢ N \in ℤ_{\geq 2} \to 1 < N$
19		ltne	$⊢ (1 \in ℝ \land 1 < N) \to N \neq 1$
20	17 18 19	sylancr	$⊢ N \in ℤ_{\geq 2} \to N \neq 1$
21	16 20	eqnetrd	$⊢ N \in ℤ_{\geq 2} \to N \gcd N \neq 1$
22		oveq1	$⊢ x = N \to x \gcd N = N \gcd N$
23	22	neeq1d	$⊢ x = N \to (x \gcd N \neq 1 \leftrightarrow N \gcd N \neq 1)$
24	21 23	syl5ibrcom	$⊢ N \in ℤ_{\geq 2} \to (x = N \to x \gcd N \neq 1)$
25	24	adantr	$⊢ (N \in ℤ_{\geq 2} \land x \in (1 \dots N)) \to (x = N \to x \gcd N \neq 1)$
26	7 25	syld	$⊢ (N \in ℤ_{\geq 2} \land x \in (1 \dots N)) \to (\neg x \in (1 \dots N - 1) \to x \gcd N \neq 1)$
27	26	necon4bd	$⊢ (N \in ℤ_{\geq 2} \land x \in (1 \dots N)) \to (x \gcd N = 1 \to x \in (1 \dots N - 1))$
28	27	ralrimiva	$⊢ N \in ℤ_{\geq 2} \to \forall x \in (1 \dots N) (x \gcd N = 1 \to x \in (1 \dots N - 1))$
29		rabss	$⊢ \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N - 1) \leftrightarrow \forall x \in (1 \dots N) (x \gcd N = 1 \to x \in (1 \dots N - 1))$
30	28 29	sylibr	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N - 1)$

Metamath Proof Explorer

Theorem phibndlem

Proof