This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem phibndlem

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

Ref Expression
Assertion phibndlem ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ... ( 𝑁 − 1 ) ) )

Proof

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