eulerthlem1

	Ref	Expression
Hypotheses	eulerth.1	$⊢ φ \to (N \in ℕ \land A \in ℤ \land A \gcd N = 1)$
	eulerth.2	$⊢ S = \{y \in (0 ..^N) \| y \gcd N = 1\}$
	eulerth.3	$⊢ T = (1 \dots ϕ (N))$
	eulerth.4	$⊢ φ \to F : T \underset{1-1 onto}{⟶} S$
	eulerth.5	$⊢ G = (x \in T ⟼ A F (x) \mod N)$
Assertion	eulerthlem1	$⊢ φ \to G : T ⟶ S$

Proof

Step	Hyp	Ref	Expression
1		eulerth.1	$⊢ φ \to (N \in ℕ \land A \in ℤ \land A \gcd N = 1)$
2		eulerth.2	$⊢ S = \{y \in (0 ..^N) \| y \gcd N = 1\}$
3		eulerth.3	$⊢ T = (1 \dots ϕ (N))$
4		eulerth.4	$⊢ φ \to F : T \underset{1-1 onto}{⟶} S$
5		eulerth.5	$⊢ G = (x \in T ⟼ A F (x) \mod N)$
6	1	simp2d	$⊢ φ \to A \in ℤ$
7	6	adantr	$⊢ (φ \land x \in T) \to A \in ℤ$
8		f1of	$⊢ F : T \underset{1-1 onto}{⟶} S \to F : T ⟶ S$
9	4 8	syl	$⊢ φ \to F : T ⟶ S$
10	9	ffvelrnda	$⊢ (φ \land x \in T) \to F (x) \in S$
11		oveq1	$⊢ y = F (x) \to y \gcd N = F (x) \gcd N$
12	11	eqeq1d	$⊢ y = F (x) \to (y \gcd N = 1 \leftrightarrow F (x) \gcd N = 1)$
13	12 2	elrab2	$⊢ F (x) \in S \leftrightarrow (F (x) \in (0 ..^N) \land F (x) \gcd N = 1)$
14	10 13	sylib	$⊢ (φ \land x \in T) \to (F (x) \in (0 ..^N) \land F (x) \gcd N = 1)$
15	14	simpld	$⊢ (φ \land x \in T) \to F (x) \in (0 ..^N)$
16		elfzoelz	$⊢ F (x) \in (0 ..^N) \to F (x) \in ℤ$
17	15 16	syl	$⊢ (φ \land x \in T) \to F (x) \in ℤ$
18	7 17	zmulcld	$⊢ (φ \land x \in T) \to A F (x) \in ℤ$
19	1	simp1d	$⊢ φ \to N \in ℕ$
20	19	adantr	$⊢ (φ \land x \in T) \to N \in ℕ$
21		zmodfzo	$⊢ (A F (x) \in ℤ \land N \in ℕ) \to A F (x) \mod N \in (0 ..^N)$
22	18 20 21	syl2anc	$⊢ (φ \land x \in T) \to A F (x) \mod N \in (0 ..^N)$
23		modgcd	$⊢ (A F (x) \in ℤ \land N \in ℕ) \to (A F (x) \mod N) \gcd N = A F (x) \gcd N$
24	18 20 23	syl2anc	$⊢ (φ \land x \in T) \to (A F (x) \mod N) \gcd N = A F (x) \gcd N$
25	19	nnzd	$⊢ φ \to N \in ℤ$
26	25	adantr	$⊢ (φ \land x \in T) \to N \in ℤ$
27	18 26	gcdcomd	$⊢ (φ \land x \in T) \to A F (x) \gcd N = N \gcd A F (x)$
28	25 6	gcdcomd	$⊢ φ \to N \gcd A = A \gcd N$
29	1	simp3d	$⊢ φ \to A \gcd N = 1$
30	28 29	eqtrd	$⊢ φ \to N \gcd A = 1$
31	30	adantr	$⊢ (φ \land x \in T) \to N \gcd A = 1$
32	26 17	gcdcomd	$⊢ (φ \land x \in T) \to N \gcd F (x) = F (x) \gcd N$
33	14	simprd	$⊢ (φ \land x \in T) \to F (x) \gcd N = 1$
34	32 33	eqtrd	$⊢ (φ \land x \in T) \to N \gcd F (x) = 1$
35		rpmul	$⊢ (N \in ℤ \land A \in ℤ \land F (x) \in ℤ) \to ((N \gcd A = 1 \land N \gcd F (x) = 1) \to N \gcd A F (x) = 1)$
36	26 7 17 35	syl3anc	$⊢ (φ \land x \in T) \to ((N \gcd A = 1 \land N \gcd F (x) = 1) \to N \gcd A F (x) = 1)$
37	31 34 36	mp2and	$⊢ (φ \land x \in T) \to N \gcd A F (x) = 1$
38	24 27 37	3eqtrd	$⊢ (φ \land x \in T) \to (A F (x) \mod N) \gcd N = 1$
39		oveq1	$⊢ y = A F (x) \mod N \to y \gcd N = (A F (x) \mod N) \gcd N$
40	39	eqeq1d	$⊢ y = A F (x) \mod N \to (y \gcd N = 1 \leftrightarrow (A F (x) \mod N) \gcd N = 1)$
41	40 2	elrab2	$⊢ A F (x) \mod N \in S \leftrightarrow (A F (x) \mod N \in (0 ..^N) \land (A F (x) \mod N) \gcd N = 1)$
42	22 38 41	sylanbrc	$⊢ (φ \land x \in T) \to A F (x) \mod N \in S$
43	42 5	fmptd	$⊢ φ \to G : T ⟶ S$

Metamath Proof Explorer

Theorem eulerthlem1

Proof