Metamath Proof Explorer

Theorem phicl2

Description: Bounds and closure for the value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion phicl2 ⊢ N ∈ ℕ → ϕ ⁡ N ∈ 1 … N

Proof

Step Hyp Ref Expression
1 phival ⊢ N ∈ ℕ → ϕ ⁡ N = x ∈ 1 … N | x gcd N = 1
2 fzfi ⊢ 1 … N ∈ Fin
3 ssrab2 ⊢ x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N
4 ssfi ⊢ 1 … N ∈ Fin ∧ x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N → x ∈ 1 … N | x gcd N = 1 ∈ Fin
5 2 3 4 mp2an ⊢ x ∈ 1 … N | x gcd N = 1 ∈ Fin
6 hashcl ⊢ x ∈ 1 … N | x gcd N = 1 ∈ Fin → x ∈ 1 … N | x gcd N = 1 ∈ ℕ 0
7 5 6 ax-mp ⊢ x ∈ 1 … N | x gcd N = 1 ∈ ℕ 0
8 7 nn0zi ⊢ x ∈ 1 … N | x gcd N = 1 ∈ ℤ
9 8 a1i ⊢ N ∈ ℕ → x ∈ 1 … N | x gcd N = 1 ∈ ℤ
10 1z ⊢ 1 ∈ ℤ
11 hashsng ⊢ 1 ∈ ℤ → 1 = 1
12 10 11 ax-mp ⊢ 1 = 1
13 ovex ⊢ 1 … N ∈ V
14 13 rabex ⊢ x ∈ 1 … N | x gcd N = 1 ∈ V
15 oveq1 ⊢ x = 1 → x gcd N = 1 gcd N
16 15 eqeq1d ⊢ x = 1 → x gcd N = 1 ↔ 1 gcd N = 1
17 eluzfz1 ⊢ N ∈ ℤ ≥ 1 → 1 ∈ 1 … N
18 nnuz ⊢ ℕ = ℤ ≥ 1
19 17 18 eleq2s ⊢ N ∈ ℕ → 1 ∈ 1 … N
20 nnz ⊢ N ∈ ℕ → N ∈ ℤ
21 1gcd ⊢ N ∈ ℤ → 1 gcd N = 1
22 20 21 syl ⊢ N ∈ ℕ → 1 gcd N = 1
23 16 19 22 elrabd ⊢ N ∈ ℕ → 1 ∈ x ∈ 1 … N | x gcd N = 1
24 23 snssd ⊢ N ∈ ℕ → 1 ⊆ x ∈ 1 … N | x gcd N = 1
25 ssdomg ⊢ x ∈ 1 … N | x gcd N = 1 ∈ V → 1 ⊆ x ∈ 1 … N | x gcd N = 1 → 1 ≼ x ∈ 1 … N | x gcd N = 1
26 14 24 25 mpsyl ⊢ N ∈ ℕ → 1 ≼ x ∈ 1 … N | x gcd N = 1
27 snfi ⊢ 1 ∈ Fin
28 hashdom ⊢ 1 ∈ Fin ∧ x ∈ 1 … N | x gcd N = 1 ∈ Fin → 1 ≤ x ∈ 1 … N | x gcd N = 1 ↔ 1 ≼ x ∈ 1 … N | x gcd N = 1
29 27 5 28 mp2an ⊢ 1 ≤ x ∈ 1 … N | x gcd N = 1 ↔ 1 ≼ x ∈ 1 … N | x gcd N = 1
30 26 29 sylibr ⊢ N ∈ ℕ → 1 ≤ x ∈ 1 … N | x gcd N = 1
31 12 30 eqbrtrrid ⊢ N ∈ ℕ → 1 ≤ x ∈ 1 … N | x gcd N = 1
32 ssdomg ⊢ 1 … N ∈ V → x ∈ 1 … N | x gcd N = 1 ⊆ 1 … N → x ∈ 1 … N | x gcd N = 1 ≼ 1 … N
33 13 3 32 mp2 ⊢ x ∈ 1 … N | x gcd N = 1 ≼ 1 … N
34 hashdom ⊢ x ∈ 1 … N | x gcd N = 1 ∈ Fin ∧ 1 … N ∈ Fin → x ∈ 1 … N | x gcd N = 1 ≤ 1 … N ↔ x ∈ 1 … N | x gcd N = 1 ≼ 1 … N
35 5 2 34 mp2an ⊢ x ∈ 1 … N | x gcd N = 1 ≤ 1 … N ↔ x ∈ 1 … N | x gcd N = 1 ≼ 1 … N
36 33 35 mpbir ⊢ x ∈ 1 … N | x gcd N = 1 ≤ 1 … N
37 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
38 hashfz1 ⊢ N ∈ ℕ 0 → 1 … N = N
39 37 38 syl ⊢ N ∈ ℕ → 1 … N = N
40 36 39 breqtrid ⊢ N ∈ ℕ → x ∈ 1 … N | x gcd N = 1 ≤ N
41 elfz1 ⊢ 1 ∈ ℤ ∧ N ∈ ℤ → x ∈ 1 … N | x gcd N = 1 ∈ 1 … N ↔ x ∈ 1 … N | x gcd N = 1 ∈ ℤ ∧ 1 ≤ x ∈ 1 … N | x gcd N = 1 ∧ x ∈ 1 … N | x gcd N = 1 ≤ N
42 10 20 41 sylancr ⊢ N ∈ ℕ → x ∈ 1 … N | x gcd N = 1 ∈ 1 … N ↔ x ∈ 1 … N | x gcd N = 1 ∈ ℤ ∧ 1 ≤ x ∈ 1 … N | x gcd N = 1 ∧ x ∈ 1 … N | x gcd N = 1 ≤ N
43 9 31 40 42 mpbir3and ⊢ N ∈ ℕ → x ∈ 1 … N | x gcd N = 1 ∈ 1 … N
44 1 43 eqeltrd ⊢ N ∈ ℕ → ϕ ⁡ N ∈ 1 … N