Metamath Proof Explorer

Theorem phibndlem

Description: Lemma for phibnd . (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion phibndlem ⊢ N ∈ ℤ ≥ 2 → x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N − 1

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
2 fzm1 ⊢ N ∈ ℤ ≥ 1 → x ∈ 1 … N ↔ x ∈ 1 … N − 1 ∨ x = N
3 nnuz ⊢ ℕ = ℤ ≥ 1
4 2 3 eleq2s ⊢ N ∈ ℕ → x ∈ 1 … N ↔ x ∈ 1 … N − 1 ∨ x = N
5 4 biimpa ⊢ N ∈ ℕ ∧ x ∈ 1 … N → x ∈ 1 … N − 1 ∨ x = N
6 5 ord ⊢ N ∈ ℕ ∧ x ∈ 1 … N → ¬ x ∈ 1 … N − 1 → x = N
7 1 6 sylan ⊢ N ∈ ℤ ≥ 2 ∧ x ∈ 1 … N → ¬ x ∈ 1 … N − 1 → x = N
8 eluzelz ⊢ N ∈ ℤ ≥ 2 → N ∈ ℤ
9 gcdid ⊢ N ∈ ℤ → N gcd N = N
10 8 9 syl ⊢ N ∈ ℤ ≥ 2 → N gcd N = N
11 nnre ⊢ N ∈ ℕ → N ∈ ℝ
12 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
13 12 nn0ge0d ⊢ N ∈ ℕ → 0 ≤ N
14 11 13 absidd ⊢ N ∈ ℕ → N = N
15 1 14 syl ⊢ N ∈ ℤ ≥ 2 → N = N
16 10 15 eqtrd ⊢ N ∈ ℤ ≥ 2 → N gcd N = N
17 1re ⊢ 1 ∈ ℝ
18 eluz2gt1 ⊢ N ∈ ℤ ≥ 2 → 1 < N
19 ltne ⊢ 1 ∈ ℝ ∧ 1 < N → N ≠ 1
20 17 18 19 sylancr ⊢ N ∈ ℤ ≥ 2 → N ≠ 1
21 16 20 eqnetrd ⊢ N ∈ ℤ ≥ 2 → N gcd N ≠ 1
22 oveq1 ⊢ x = N → x gcd N = N gcd N
23 22 neeq1d ⊢ x = N → x gcd N ≠ 1 ↔ N gcd N ≠ 1
24 21 23 syl5ibrcom ⊢ N ∈ ℤ ≥ 2 → x = N → x gcd N ≠ 1
25 24 adantr ⊢ N ∈ ℤ ≥ 2 ∧ x ∈ 1 … N → x = N → x gcd N ≠ 1
26 7 25 syld ⊢ N ∈ ℤ ≥ 2 ∧ x ∈ 1 … N → ¬ x ∈ 1 … N − 1 → x gcd N ≠ 1
27 26 necon4bd ⊢ N ∈ ℤ ≥ 2 ∧ x ∈ 1 … N → x gcd N = 1 → x ∈ 1 … N − 1
28 27 ralrimiva ⊢ N ∈ ℤ ≥ 2 → ∀ x ∈ 1 … N x gcd N = 1 → x ∈ 1 … N − 1
29 rabss ⊢ x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N − 1 ↔ ∀ x ∈ 1 … N x gcd N = 1 → x ∈ 1 … N − 1
30 28 29 sylibr ⊢ N ∈ ℤ ≥ 2 → x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N − 1