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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
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	⊢ ( 𝜑 → 𝐺 : 𝑇 ⟶ 𝑆 )