Metamath Proof Explorer

Theorem hashgcdeq

Description: Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion hashgcdeq ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = if ( 𝑁 ∥ 𝑀 , ( ϕ ‘ ( 𝑀 / 𝑁 ) ) , 0 ) )

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( ( ϕ ‘ ( 𝑀 / 𝑁 ) ) = if ( 𝑁 ∥ 𝑀 , ( ϕ ‘ ( 𝑀 / 𝑁 ) ) , 0 ) → ( ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = ( ϕ ‘ ( 𝑀 / 𝑁 ) ) ↔ ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = if ( 𝑁 ∥ 𝑀 , ( ϕ ‘ ( 𝑀 / 𝑁 ) ) , 0 ) ) )
2 eqeq2 ⊢ ( 0 = if ( 𝑁 ∥ 𝑀 , ( ϕ ‘ ( 𝑀 / 𝑁 ) ) , 0 ) → ( ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = 0 ↔ ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = if ( 𝑁 ∥ 𝑀 , ( ϕ ‘ ( 𝑀 / 𝑁 ) ) , 0 ) ) )
3 nndivdvds ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∥ 𝑀 ↔ ( 𝑀 / 𝑁 ) ∈ ℕ ) )
4 3 biimpa ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ 𝑀 ) → ( 𝑀 / 𝑁 ) ∈ ℕ )
5 dfphi2 ⊢ ( ( 𝑀 / 𝑁 ) ∈ ℕ → ( ϕ ‘ ( 𝑀 / 𝑁 ) ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ) )
6 4 5 syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ 𝑀 ) → ( ϕ ‘ ( 𝑀 / 𝑁 ) ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ) )
7 eqid ⊢ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } = { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 }
8 eqid ⊢ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } = { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 }
9 eqid ⊢ ( 𝑧 ∈ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ↦ ( 𝑧 · 𝑁 ) ) = ( 𝑧 ∈ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ↦ ( 𝑧 · 𝑁 ) )
10 7 8 9 hashgcdlem ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀 ) → ( 𝑧 ∈ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ↦ ( 𝑧 · 𝑁 ) ) : { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } –1-1-onto→ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } )
11 10 3expa ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ 𝑀 ) → ( 𝑧 ∈ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ↦ ( 𝑧 · 𝑁 ) ) : { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } –1-1-onto→ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } )
12 ovex ⊢ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∈ V
13 12 rabex ⊢ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ∈ V
14 13 f1oen ⊢ ( ( 𝑧 ∈ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ↦ ( 𝑧 · 𝑁 ) ) : { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } –1-1-onto→ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } → { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ≈ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } )
15 hasheni ⊢ ( { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ≈ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } → ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) )
16 11 14 15 3syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ 𝑀 ) → ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 } ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) )
17 6 16 eqtr2d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑁 ∥ 𝑀 ) → ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = ( ϕ ‘ ( 𝑀 / 𝑁 ) ) )
18 simprr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 gcd 𝑀 ) = 𝑁 ) ) → ( 𝑥 gcd 𝑀 ) = 𝑁 )
19 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) → 𝑥 ∈ ℤ )
20 19 ad2antrl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 gcd 𝑀 ) = 𝑁 ) ) → 𝑥 ∈ ℤ )
21 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
22 21 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 gcd 𝑀 ) = 𝑁 ) ) → 𝑀 ∈ ℤ )
23 gcddvds ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑥 gcd 𝑀 ) ∥ 𝑥 ∧ ( 𝑥 gcd 𝑀 ) ∥ 𝑀 ) )
24 20 22 23 syl2anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 gcd 𝑀 ) = 𝑁 ) ) → ( ( 𝑥 gcd 𝑀 ) ∥ 𝑥 ∧ ( 𝑥 gcd 𝑀 ) ∥ 𝑀 ) )
25 24 simprd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 gcd 𝑀 ) = 𝑁 ) ) → ( 𝑥 gcd 𝑀 ) ∥ 𝑀 )
26 18 25 eqbrtrrd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 gcd 𝑀 ) = 𝑁 ) ) → 𝑁 ∥ 𝑀 )
27 26 expr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑥 gcd 𝑀 ) = 𝑁 → 𝑁 ∥ 𝑀 ) )
28 27 con3d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) → ( ¬ 𝑁 ∥ 𝑀 → ¬ ( 𝑥 gcd 𝑀 ) = 𝑁 ) )
29 28 impancom ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ 𝑀 ) → ( 𝑥 ∈ ( 0 ..^ 𝑀 ) → ¬ ( 𝑥 gcd 𝑀 ) = 𝑁 ) )
30 29 ralrimiv ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ 𝑀 ) → ∀ 𝑥 ∈ ( 0 ..^ 𝑀 ) ¬ ( 𝑥 gcd 𝑀 ) = 𝑁 )
31 rabeq0 ⊢ ( { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } = ∅ ↔ ∀ 𝑥 ∈ ( 0 ..^ 𝑀 ) ¬ ( 𝑥 gcd 𝑀 ) = 𝑁 )
32 30 31 sylibr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ 𝑀 ) → { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } = ∅ )
33 32 fveq2d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ 𝑀 ) → ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = ( ♯ ‘ ∅ ) )
34 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
35 33 34 eqtrdi ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ¬ 𝑁 ∥ 𝑀 ) → ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = 0 )
36 1 2 17 35 ifbothda ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑥 gcd 𝑀 ) = 𝑁 } ) = if ( 𝑁 ∥ 𝑀 , ( ϕ ‘ ( 𝑀 / 𝑁 ) ) , 0 ) )