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 ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) )

Proof

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