Metamath Proof Explorer

Theorem eulerthlem1

Description: Lemma for eulerth . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses eulerth.1 ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
eulerth.2 ⊢ 𝑆 = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
eulerth.3 ⊢ 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) )
eulerth.4 ⊢ ( 𝜑 → 𝐹 : 𝑇 –1-1-onto→ 𝑆 )
eulerth.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝑇 ↦ ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) )
Assertion eulerthlem1 ( 𝜑 → 𝐺 : 𝑇 ⟶ 𝑆 )

Proof

Step Hyp Ref Expression
1 eulerth.1 ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
2 eulerth.2 ⊢ 𝑆 = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
3 eulerth.3 ⊢ 𝑇 = ( 1 ... ( ϕ ‘ 𝑁 ) )
4 eulerth.4 ⊢ ( 𝜑 → 𝐹 : 𝑇 –1-1-onto→ 𝑆 )
5 eulerth.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝑇 ↦ ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) )
6 1 simp2d ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝐴 ∈ ℤ )
8 f1of ⊢ ( 𝐹 : 𝑇 –1-1-onto→ 𝑆 → 𝐹 : 𝑇 ⟶ 𝑆 )
9 4 8 syl ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ 𝑆 )
10 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
11 oveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 gcd 𝑁 ) = ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) )
12 11 eqeq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
13 12 2 elrab2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
14 10 13 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 ) )
15 14 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
16 elfzoelz ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
18 7 17 zmulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ∈ ℤ )
19 1 simp1d ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑁 ∈ ℕ )
21 zmodfzo ⊢ ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
22 18 20 21 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
23 modgcd ⊢ ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) gcd 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) gcd 𝑁 ) )
24 18 20 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) gcd 𝑁 ) = ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) gcd 𝑁 ) )
25 19 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑁 ∈ ℤ )
27 18 26 gcdcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) gcd 𝑁 ) = ( 𝑁 gcd ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) )
28 25 6 gcdcomd ⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = ( 𝐴 gcd 𝑁 ) )
29 1 simp3d ⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = 1 )
30 28 29 eqtrd ⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = 1 )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑁 gcd 𝐴 ) = 1 )
32 26 17 gcdcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑁 gcd ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) )
33 14 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑥 ) gcd 𝑁 ) = 1 )
34 32 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑁 gcd ( 𝐹 ‘ 𝑥 ) ) = 1 )
35 rpmul ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℤ ) → ( ( ( 𝑁 gcd 𝐴 ) = 1 ∧ ( 𝑁 gcd ( 𝐹 ‘ 𝑥 ) ) = 1 ) → ( 𝑁 gcd ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) = 1 ) )
36 26 7 17 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( ( 𝑁 gcd 𝐴 ) = 1 ∧ ( 𝑁 gcd ( 𝐹 ‘ 𝑥 ) ) = 1 ) → ( 𝑁 gcd ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) = 1 ) )
37 31 34 36 mp2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑁 gcd ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) = 1 )
38 24 27 37 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) gcd 𝑁 ) = 1 )
39 oveq1 ⊢ ( 𝑦 = ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) → ( 𝑦 gcd 𝑁 ) = ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) gcd 𝑁 ) )
40 39 eqeq1d ⊢ ( 𝑦 = ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) gcd 𝑁 ) = 1 ) )
41 40 2 elrab2 ⊢ ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) ∈ 𝑆 ↔ ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) gcd 𝑁 ) = 1 ) )
42 22 38 41 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) mod 𝑁 ) ∈ 𝑆 )
43 42 5 fmptd ⊢ ( 𝜑 → 𝐺 : 𝑇 ⟶ 𝑆 )