eulerthlem2

	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	eulerthlem2	$⊢ φ \to A^{ϕ (N)} \mod N = 1 \mod N$

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	simp1d	$⊢ φ \to N \in ℕ$
7	6	phicld	$⊢ φ \to ϕ (N) \in ℕ$
8	7	nnred	$⊢ φ \to ϕ (N) \in ℝ$
9	8	leidd	$⊢ φ \to ϕ (N) \leq ϕ (N)$
10	7	adantr	$⊢ (φ \land ϕ (N) \leq ϕ (N)) \to ϕ (N) \in ℕ$
11		breq1	$⊢ x = 1 \to (x \leq ϕ (N) \leftrightarrow 1 \leq ϕ (N))$
12	11	anbi2d	$⊢ x = 1 \to ((φ \land x \leq ϕ (N)) \leftrightarrow (φ \land 1 \leq ϕ (N)))$
13		oveq2	$⊢ x = 1 \to A^{x} = A^{1}$
14		fveq2	$⊢ x = 1 \to seq 1 (\times F) (x) = seq 1 (\times F) (1)$
15	13 14	oveq12d	$⊢ x = 1 \to A^{x} seq 1 (\times F) (x) = A^{1} seq 1 (\times F) (1)$
16	15	oveq1d	$⊢ x = 1 \to A^{x} seq 1 (\times F) (x) \mod N = A^{1} seq 1 (\times F) (1) \mod N$
17		fveq2	$⊢ x = 1 \to seq 1 (\times G) (x) = seq 1 (\times G) (1)$
18	17	oveq1d	$⊢ x = 1 \to seq 1 (\times G) (x) \mod N = seq 1 (\times G) (1) \mod N$
19	16 18	eqeq12d	$⊢ x = 1 \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \leftrightarrow A^{1} seq 1 (\times F) (1) \mod N = seq 1 (\times G) (1) \mod N)$
20	14	oveq2d	$⊢ x = 1 \to N \gcd seq 1 (\times F) (x) = N \gcd seq 1 (\times F) (1)$
21	20	eqeq1d	$⊢ x = 1 \to (N \gcd seq 1 (\times F) (x) = 1 \leftrightarrow N \gcd seq 1 (\times F) (1) = 1)$
22	19 21	anbi12d	$⊢ x = 1 \to ((A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1) \leftrightarrow (A^{1} seq 1 (\times F) (1) \mod N = seq 1 (\times G) (1) \mod N \land N \gcd seq 1 (\times F) (1) = 1))$
23	12 22	imbi12d	$⊢ x = 1 \to (((φ \land x \leq ϕ (N)) \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1)) \leftrightarrow ((φ \land 1 \leq ϕ (N)) \to (A^{1} seq 1 (\times F) (1) \mod N = seq 1 (\times G) (1) \mod N \land N \gcd seq 1 (\times F) (1) = 1)))$
24		breq1	$⊢ x = z \to (x \leq ϕ (N) \leftrightarrow z \leq ϕ (N))$
25	24	anbi2d	$⊢ x = z \to ((φ \land x \leq ϕ (N)) \leftrightarrow (φ \land z \leq ϕ (N)))$
26		oveq2	$⊢ x = z \to A^{x} = A^{z}$
27		fveq2	$⊢ x = z \to seq 1 (\times F) (x) = seq 1 (\times F) (z)$
28	26 27	oveq12d	$⊢ x = z \to A^{x} seq 1 (\times F) (x) = A^{z} seq 1 (\times F) (z)$
29	28	oveq1d	$⊢ x = z \to A^{x} seq 1 (\times F) (x) \mod N = A^{z} seq 1 (\times F) (z) \mod N$
30		fveq2	$⊢ x = z \to seq 1 (\times G) (x) = seq 1 (\times G) (z)$
31	30	oveq1d	$⊢ x = z \to seq 1 (\times G) (x) \mod N = seq 1 (\times G) (z) \mod N$
32	29 31	eqeq12d	$⊢ x = z \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \leftrightarrow A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N)$
33	27	oveq2d	$⊢ x = z \to N \gcd seq 1 (\times F) (x) = N \gcd seq 1 (\times F) (z)$
34	33	eqeq1d	$⊢ x = z \to (N \gcd seq 1 (\times F) (x) = 1 \leftrightarrow N \gcd seq 1 (\times F) (z) = 1)$
35	32 34	anbi12d	$⊢ x = z \to ((A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1) \leftrightarrow (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1))$
36	25 35	imbi12d	$⊢ x = z \to (((φ \land x \leq ϕ (N)) \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1)) \leftrightarrow ((φ \land z \leq ϕ (N)) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1)))$
37		breq1	$⊢ x = z + 1 \to (x \leq ϕ (N) \leftrightarrow z + 1 \leq ϕ (N))$
38	37	anbi2d	$⊢ x = z + 1 \to ((φ \land x \leq ϕ (N)) \leftrightarrow (φ \land z + 1 \leq ϕ (N)))$
39		oveq2	$⊢ x = z + 1 \to A^{x} = A^{z + 1}$
40		fveq2	$⊢ x = z + 1 \to seq 1 (\times F) (x) = seq 1 (\times F) (z + 1)$
41	39 40	oveq12d	$⊢ x = z + 1 \to A^{x} seq 1 (\times F) (x) = A^{z + 1} seq 1 (\times F) (z + 1)$
42	41	oveq1d	$⊢ x = z + 1 \to A^{x} seq 1 (\times F) (x) \mod N = A^{z + 1} seq 1 (\times F) (z + 1) \mod N$
43		fveq2	$⊢ x = z + 1 \to seq 1 (\times G) (x) = seq 1 (\times G) (z + 1)$
44	43	oveq1d	$⊢ x = z + 1 \to seq 1 (\times G) (x) \mod N = seq 1 (\times G) (z + 1) \mod N$
45	42 44	eqeq12d	$⊢ x = z + 1 \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \leftrightarrow A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N)$
46	40	oveq2d	$⊢ x = z + 1 \to N \gcd seq 1 (\times F) (x) = N \gcd seq 1 (\times F) (z + 1)$
47	46	eqeq1d	$⊢ x = z + 1 \to (N \gcd seq 1 (\times F) (x) = 1 \leftrightarrow N \gcd seq 1 (\times F) (z + 1) = 1)$
48	45 47	anbi12d	$⊢ x = z + 1 \to ((A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1) \leftrightarrow (A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N \land N \gcd seq 1 (\times F) (z + 1) = 1))$
49	38 48	imbi12d	$⊢ x = z + 1 \to (((φ \land x \leq ϕ (N)) \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1)) \leftrightarrow ((φ \land z + 1 \leq ϕ (N)) \to (A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N \land N \gcd seq 1 (\times F) (z + 1) = 1)))$
50		breq1	$⊢ x = ϕ (N) \to (x \leq ϕ (N) \leftrightarrow ϕ (N) \leq ϕ (N))$
51	50	anbi2d	$⊢ x = ϕ (N) \to ((φ \land x \leq ϕ (N)) \leftrightarrow (φ \land ϕ (N) \leq ϕ (N)))$
52		oveq2	$⊢ x = ϕ (N) \to A^{x} = A^{ϕ (N)}$
53		fveq2	$⊢ x = ϕ (N) \to seq 1 (\times F) (x) = seq 1 (\times F) (ϕ (N))$
54	52 53	oveq12d	$⊢ x = ϕ (N) \to A^{x} seq 1 (\times F) (x) = A^{ϕ (N)} seq 1 (\times F) (ϕ (N))$
55	54	oveq1d	$⊢ x = ϕ (N) \to A^{x} seq 1 (\times F) (x) \mod N = A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N$
56		fveq2	$⊢ x = ϕ (N) \to seq 1 (\times G) (x) = seq 1 (\times G) (ϕ (N))$
57	56	oveq1d	$⊢ x = ϕ (N) \to seq 1 (\times G) (x) \mod N = seq 1 (\times G) (ϕ (N)) \mod N$
58	55 57	eqeq12d	$⊢ x = ϕ (N) \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \leftrightarrow A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N)$
59	53	oveq2d	$⊢ x = ϕ (N) \to N \gcd seq 1 (\times F) (x) = N \gcd seq 1 (\times F) (ϕ (N))$
60	59	eqeq1d	$⊢ x = ϕ (N) \to (N \gcd seq 1 (\times F) (x) = 1 \leftrightarrow N \gcd seq 1 (\times F) (ϕ (N)) = 1)$
61	58 60	anbi12d	$⊢ x = ϕ (N) \to ((A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1) \leftrightarrow (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N \land N \gcd seq 1 (\times F) (ϕ (N)) = 1))$
62	51 61	imbi12d	$⊢ x = ϕ (N) \to (((φ \land x \leq ϕ (N)) \to (A^{x} seq 1 (\times F) (x) \mod N = seq 1 (\times G) (x) \mod N \land N \gcd seq 1 (\times F) (x) = 1)) \leftrightarrow ((φ \land ϕ (N) \leq ϕ (N)) \to (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N \land N \gcd seq 1 (\times F) (ϕ (N)) = 1)))$
63	1	simp2d	$⊢ φ \to A \in ℤ$
64		f1of	$⊢ F : T \underset{1-1 onto}{⟶} S \to F : T ⟶ S$
65	4 64	syl	$⊢ φ \to F : T ⟶ S$
66		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
67	7 66	eleqtrdi	$⊢ φ \to ϕ (N) \in ℤ_{\geq 1}$
68		eluzfz1	$⊢ ϕ (N) \in ℤ_{\geq 1} \to 1 \in (1 \dots ϕ (N))$
69	67 68	syl	$⊢ φ \to 1 \in (1 \dots ϕ (N))$
70	69 3	eleqtrrdi	$⊢ φ \to 1 \in T$
71	65 70	ffvelcdmd	$⊢ φ \to F (1) \in S$
72		oveq1	$⊢ y = F (1) \to y \gcd N = F (1) \gcd N$
73	72	eqeq1d	$⊢ y = F (1) \to (y \gcd N = 1 \leftrightarrow F (1) \gcd N = 1)$
74	73 2	elrab2	$⊢ F (1) \in S \leftrightarrow (F (1) \in (0 ..^N) \land F (1) \gcd N = 1)$
75	71 74	sylib	$⊢ φ \to (F (1) \in (0 ..^N) \land F (1) \gcd N = 1)$
76	75	simpld	$⊢ φ \to F (1) \in (0 ..^N)$
77		elfzoelz	$⊢ F (1) \in (0 ..^N) \to F (1) \in ℤ$
78	76 77	syl	$⊢ φ \to F (1) \in ℤ$
79	63 78	zmulcld	$⊢ φ \to A F (1) \in ℤ$
80	79	zred	$⊢ φ \to A F (1) \in ℝ$
81	6	nnrpd	$⊢ φ \to N \in ℝ^{+}$
82		modabs2	$⊢ (A F (1) \in ℝ \land N \in ℝ^{+}) \to (A F (1) \mod N) \mod N = A F (1) \mod N$
83	80 81 82	syl2anc	$⊢ φ \to (A F (1) \mod N) \mod N = A F (1) \mod N$
84		1z	$⊢ 1 \in ℤ$
85		fveq2	$⊢ x = 1 \to F (x) = F (1)$
86	85	oveq2d	$⊢ x = 1 \to A F (x) = A F (1)$
87	86	oveq1d	$⊢ x = 1 \to A F (x) \mod N = A F (1) \mod N$
88		ovex	$⊢ A F (1) \mod N \in V$
89	87 5 88	fvmpt	$⊢ 1 \in T \to G (1) = A F (1) \mod N$
90	70 89	syl	$⊢ φ \to G (1) = A F (1) \mod N$
91	84 90	seq1i	$⊢ φ \to seq 1 (\times G) (1) = A F (1) \mod N$
92	91	oveq1d	$⊢ φ \to seq 1 (\times G) (1) \mod N = (A F (1) \mod N) \mod N$
93	63	zcnd	$⊢ φ \to A \in ℂ$
94	93	exp1d	$⊢ φ \to A^{1} = A$
95		seq1	$⊢ 1 \in ℤ \to seq 1 (\times F) (1) = F (1)$
96	84 95	ax-mp	$⊢ seq 1 (\times F) (1) = F (1)$
97	96	a1i	$⊢ φ \to seq 1 (\times F) (1) = F (1)$
98	94 97	oveq12d	$⊢ φ \to A^{1} seq 1 (\times F) (1) = A F (1)$
99	98	oveq1d	$⊢ φ \to A^{1} seq 1 (\times F) (1) \mod N = A F (1) \mod N$
100	83 92 99	3eqtr4rd	$⊢ φ \to A^{1} seq 1 (\times F) (1) \mod N = seq 1 (\times G) (1) \mod N$
101	96	oveq2i	$⊢ N \gcd seq 1 (\times F) (1) = N \gcd F (1)$
102	6	nnzd	$⊢ φ \to N \in ℤ$
103	102 78	gcdcomd	$⊢ φ \to N \gcd F (1) = F (1) \gcd N$
104	75	simprd	$⊢ φ \to F (1) \gcd N = 1$
105	103 104	eqtrd	$⊢ φ \to N \gcd F (1) = 1$
106	101 105	eqtrid	$⊢ φ \to N \gcd seq 1 (\times F) (1) = 1$
107	100 106	jca	$⊢ φ \to (A^{1} seq 1 (\times F) (1) \mod N = seq 1 (\times G) (1) \mod N \land N \gcd seq 1 (\times F) (1) = 1)$
108	107	adantr	$⊢ (φ \land 1 \leq ϕ (N)) \to (A^{1} seq 1 (\times F) (1) \mod N = seq 1 (\times G) (1) \mod N \land N \gcd seq 1 (\times F) (1) = 1)$
109		nnre	$⊢ z \in ℕ \to z \in ℝ$
110	109	adantr	$⊢ (z \in ℕ \land φ) \to z \in ℝ$
111	110	lep1d	$⊢ (z \in ℕ \land φ) \to z \leq z + 1$
112		peano2re	$⊢ z \in ℝ \to z + 1 \in ℝ$
113	110 112	syl	$⊢ (z \in ℕ \land φ) \to z + 1 \in ℝ$
114	8	adantl	$⊢ (z \in ℕ \land φ) \to ϕ (N) \in ℝ$
115		letr	$⊢ (z \in ℝ \land z + 1 \in ℝ \land ϕ (N) \in ℝ) \to ((z \leq z + 1 \land z + 1 \leq ϕ (N)) \to z \leq ϕ (N))$
116	110 113 114 115	syl3anc	$⊢ (z \in ℕ \land φ) \to ((z \leq z + 1 \land z + 1 \leq ϕ (N)) \to z \leq ϕ (N))$
117	111 116	mpand	$⊢ (z \in ℕ \land φ) \to (z + 1 \leq ϕ (N) \to z \leq ϕ (N))$
118	117	imdistanda	$⊢ z \in ℕ \to ((φ \land z + 1 \leq ϕ (N)) \to (φ \land z \leq ϕ (N)))$
119	118	imim1d	$⊢ z \in ℕ \to (((φ \land z \leq ϕ (N)) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1)) \to ((φ \land z + 1 \leq ϕ (N)) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1)))$
120	63	adantr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A \in ℤ$
121		nnnn0	$⊢ z \in ℕ \to z \in ℕ_{0}$
122	121	ad2antrl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z \in ℕ_{0}$
123		zexpcl	$⊢ (A \in ℤ \land z \in ℕ_{0}) \to A^{z} \in ℤ$
124	120 122 123	syl2anc	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z} \in ℤ$
125		simprl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z \in ℕ$
126	125 66	eleqtrdi	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z \in ℤ_{\geq 1}$
127	109	ad2antrl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z \in ℝ$
128	127 112	syl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z + 1 \in ℝ$
129	8	adantr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to ϕ (N) \in ℝ$
130	127	lep1d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z \leq z + 1$
131		simprr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z + 1 \leq ϕ (N)$
132	127 128 129 130 131	letrd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z \leq ϕ (N)$
133		nnz	$⊢ z \in ℕ \to z \in ℤ$
134	133	ad2antrl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z \in ℤ$
135	7	nnzd	$⊢ φ \to ϕ (N) \in ℤ$
136	135	adantr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to ϕ (N) \in ℤ$
137		eluz	$⊢ (z \in ℤ \land ϕ (N) \in ℤ) \to (ϕ (N) \in ℤ_{\geq z} \leftrightarrow z \leq ϕ (N))$
138	134 136 137	syl2anc	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (ϕ (N) \in ℤ_{\geq z} \leftrightarrow z \leq ϕ (N))$
139	132 138	mpbird	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to ϕ (N) \in ℤ_{\geq z}$
140		fzss2	$⊢ ϕ (N) \in ℤ_{\geq z} \to (1 \dots z) \subseteq (1 \dots ϕ (N))$
141	139 140	syl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (1 \dots z) \subseteq (1 \dots ϕ (N))$
142	141 3	sseqtrrdi	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (1 \dots z) \subseteq T$
143	142	sselda	$⊢ ((φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \land x \in (1 \dots z)) \to x \in T$
144	65	ffvelcdmda	$⊢ (φ \land x \in T) \to F (x) \in S$
145		oveq1	$⊢ y = F (x) \to y \gcd N = F (x) \gcd N$
146	145	eqeq1d	$⊢ y = F (x) \to (y \gcd N = 1 \leftrightarrow F (x) \gcd N = 1)$
147	146 2	elrab2	$⊢ F (x) \in S \leftrightarrow (F (x) \in (0 ..^N) \land F (x) \gcd N = 1)$
148	144 147	sylib	$⊢ (φ \land x \in T) \to (F (x) \in (0 ..^N) \land F (x) \gcd N = 1)$
149	148	simpld	$⊢ (φ \land x \in T) \to F (x) \in (0 ..^N)$
150		elfzoelz	$⊢ F (x) \in (0 ..^N) \to F (x) \in ℤ$
151	149 150	syl	$⊢ (φ \land x \in T) \to F (x) \in ℤ$
152	151	adantlr	$⊢ ((φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \land x \in T) \to F (x) \in ℤ$
153	143 152	syldan	$⊢ ((φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \land x \in (1 \dots z)) \to F (x) \in ℤ$
154		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
155	154	adantl	$⊢ ((φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \land (x \in ℤ \land y \in ℤ)) \to x y \in ℤ$
156	126 153 155	seqcl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times F) (z) \in ℤ$
157	124 156	zmulcld	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z} seq 1 (\times F) (z) \in ℤ$
158	157	zred	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z} seq 1 (\times F) (z) \in ℝ$
159	2	ssrab3	$⊢ S \subseteq (0 ..^N)$
160	1 2 3 4 5	eulerthlem1	$⊢ φ \to G : T ⟶ S$
161	160	ffvelcdmda	$⊢ (φ \land x \in T) \to G (x) \in S$
162	159 161	sselid	$⊢ (φ \land x \in T) \to G (x) \in (0 ..^N)$
163		elfzoelz	$⊢ G (x) \in (0 ..^N) \to G (x) \in ℤ$
164	162 163	syl	$⊢ (φ \land x \in T) \to G (x) \in ℤ$
165	164	adantlr	$⊢ ((φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \land x \in T) \to G (x) \in ℤ$
166	143 165	syldan	$⊢ ((φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \land x \in (1 \dots z)) \to G (x) \in ℤ$
167	126 166 155	seqcl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z) \in ℤ$
168	167	zred	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z) \in ℝ$
169	65	adantr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to F : T ⟶ S$
170		peano2nn	$⊢ z \in ℕ \to z + 1 \in ℕ$
171	170	ad2antrl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z + 1 \in ℕ$
172	171	nnge1d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to 1 \leq z + 1$
173	171	nnzd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z + 1 \in ℤ$
174		elfz	$⊢ (z + 1 \in ℤ \land 1 \in ℤ \land ϕ (N) \in ℤ) \to (z + 1 \in (1 \dots ϕ (N)) \leftrightarrow (1 \leq z + 1 \land z + 1 \leq ϕ (N)))$
175	84 174	mp3an2	$⊢ (z + 1 \in ℤ \land ϕ (N) \in ℤ) \to (z + 1 \in (1 \dots ϕ (N)) \leftrightarrow (1 \leq z + 1 \land z + 1 \leq ϕ (N)))$
176	173 136 175	syl2anc	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (z + 1 \in (1 \dots ϕ (N)) \leftrightarrow (1 \leq z + 1 \land z + 1 \leq ϕ (N)))$
177	172 131 176	mpbir2and	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z + 1 \in (1 \dots ϕ (N))$
178	177 3	eleqtrrdi	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to z + 1 \in T$
179	169 178	ffvelcdmd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to F (z + 1) \in S$
180		oveq1	$⊢ y = F (z + 1) \to y \gcd N = F (z + 1) \gcd N$
181	180	eqeq1d	$⊢ y = F (z + 1) \to (y \gcd N = 1 \leftrightarrow F (z + 1) \gcd N = 1)$
182	181 2	elrab2	$⊢ F (z + 1) \in S \leftrightarrow (F (z + 1) \in (0 ..^N) \land F (z + 1) \gcd N = 1)$
183	179 182	sylib	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (F (z + 1) \in (0 ..^N) \land F (z + 1) \gcd N = 1)$
184	183	simpld	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to F (z + 1) \in (0 ..^N)$
185		elfzoelz	$⊢ F (z + 1) \in (0 ..^N) \to F (z + 1) \in ℤ$
186	184 185	syl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to F (z + 1) \in ℤ$
187	120 186	zmulcld	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A F (z + 1) \in ℤ$
188	81	adantr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to N \in ℝ^{+}$
189		modmul1	$⊢ ((A^{z} seq 1 (\times F) (z) \in ℝ \land seq 1 (\times G) (z) \in ℝ) \land (A F (z + 1) \in ℤ \land N \in ℝ^{+}) \land A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N) \to A^{z} seq 1 (\times F) (z) A F (z + 1) \mod N = seq 1 (\times G) (z) A F (z + 1) \mod N$
190	189	3expia	$⊢ ((A^{z} seq 1 (\times F) (z) \in ℝ \land seq 1 (\times G) (z) \in ℝ) \land (A F (z + 1) \in ℤ \land N \in ℝ^{+})) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \to A^{z} seq 1 (\times F) (z) A F (z + 1) \mod N = seq 1 (\times G) (z) A F (z + 1) \mod N)$
191	158 168 187 188 190	syl22anc	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \to A^{z} seq 1 (\times F) (z) A F (z + 1) \mod N = seq 1 (\times G) (z) A F (z + 1) \mod N)$
192	124	zcnd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z} \in ℂ$
193	156	zcnd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times F) (z) \in ℂ$
194	93	adantr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A \in ℂ$
195	186	zcnd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to F (z + 1) \in ℂ$
196	192 193 194 195	mul4d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z} seq 1 (\times F) (z) A F (z + 1) = A^{z} A seq 1 (\times F) (z) F (z + 1)$
197	194 122	expp1d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z + 1} = A^{z} A$
198		seqp1	$⊢ z \in ℤ_{\geq 1} \to seq 1 (\times F) (z + 1) = seq 1 (\times F) (z) F (z + 1)$
199	126 198	syl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times F) (z + 1) = seq 1 (\times F) (z) F (z + 1)$
200	197 199	oveq12d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z + 1} seq 1 (\times F) (z + 1) = A^{z} A seq 1 (\times F) (z) F (z + 1)$
201	196 200	eqtr4d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z} seq 1 (\times F) (z) A F (z + 1) = A^{z + 1} seq 1 (\times F) (z + 1)$
202	201	oveq1d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A^{z} seq 1 (\times F) (z) A F (z + 1) \mod N = A^{z + 1} seq 1 (\times F) (z + 1) \mod N$
203	187	zred	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A F (z + 1) \in ℝ$
204	203 188	modcld	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A F (z + 1) \mod N \in ℝ$
205		modabs2	$⊢ (A F (z + 1) \in ℝ \land N \in ℝ^{+}) \to (A F (z + 1) \mod N) \mod N = A F (z + 1) \mod N$
206	203 188 205	syl2anc	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (A F (z + 1) \mod N) \mod N = A F (z + 1) \mod N$
207		modmul1	$⊢ ((A F (z + 1) \mod N \in ℝ \land A F (z + 1) \in ℝ) \land (seq 1 (\times G) (z) \in ℤ \land N \in ℝ^{+}) \land (A F (z + 1) \mod N) \mod N = A F (z + 1) \mod N) \to (A F (z + 1) \mod N) seq 1 (\times G) (z) \mod N = A F (z + 1) seq 1 (\times G) (z) \mod N$
208	204 203 167 188 206 207	syl221anc	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (A F (z + 1) \mod N) seq 1 (\times G) (z) \mod N = A F (z + 1) seq 1 (\times G) (z) \mod N$
209		fveq2	$⊢ x = z + 1 \to F (x) = F (z + 1)$
210	209	oveq2d	$⊢ x = z + 1 \to A F (x) = A F (z + 1)$
211	210	oveq1d	$⊢ x = z + 1 \to A F (x) \mod N = A F (z + 1) \mod N$
212		ovex	$⊢ A F (z + 1) \mod N \in V$
213	211 5 212	fvmpt	$⊢ z + 1 \in T \to G (z + 1) = A F (z + 1) \mod N$
214	178 213	syl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to G (z + 1) = A F (z + 1) \mod N$
215	214	oveq2d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z) G (z + 1) = seq 1 (\times G) (z) (A F (z + 1) \mod N)$
216		seqp1	$⊢ z \in ℤ_{\geq 1} \to seq 1 (\times G) (z + 1) = seq 1 (\times G) (z) G (z + 1)$
217	126 216	syl	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z + 1) = seq 1 (\times G) (z) G (z + 1)$
218	204	recnd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A F (z + 1) \mod N \in ℂ$
219	167	zcnd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z) \in ℂ$
220	218 219	mulcomd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (A F (z + 1) \mod N) seq 1 (\times G) (z) = seq 1 (\times G) (z) (A F (z + 1) \mod N)$
221	215 217 220	3eqtr4d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z + 1) = (A F (z + 1) \mod N) seq 1 (\times G) (z)$
222	221	oveq1d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z + 1) \mod N = (A F (z + 1) \mod N) seq 1 (\times G) (z) \mod N$
223	187	zcnd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to A F (z + 1) \in ℂ$
224	219 223	mulcomd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z) A F (z + 1) = A F (z + 1) seq 1 (\times G) (z)$
225	224	oveq1d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z) A F (z + 1) \mod N = A F (z + 1) seq 1 (\times G) (z) \mod N$
226	208 222 225	3eqtr4rd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to seq 1 (\times G) (z) A F (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N$
227	202 226	eqeq12d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (A^{z} seq 1 (\times F) (z) A F (z + 1) \mod N = seq 1 (\times G) (z) A F (z + 1) \mod N \leftrightarrow A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N)$
228	191 227	sylibd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \to A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N)$
229	102	adantr	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to N \in ℤ$
230	229 186	gcdcomd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to N \gcd F (z + 1) = F (z + 1) \gcd N$
231	183	simprd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to F (z + 1) \gcd N = 1$
232	230 231	eqtrd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to N \gcd F (z + 1) = 1$
233		rpmul	$⊢ (N \in ℤ \land seq 1 (\times F) (z) \in ℤ \land F (z + 1) \in ℤ) \to ((N \gcd seq 1 (\times F) (z) = 1 \land N \gcd F (z + 1) = 1) \to N \gcd seq 1 (\times F) (z) F (z + 1) = 1)$
234	229 156 186 233	syl3anc	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to ((N \gcd seq 1 (\times F) (z) = 1 \land N \gcd F (z + 1) = 1) \to N \gcd seq 1 (\times F) (z) F (z + 1) = 1)$
235	232 234	mpan2d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (N \gcd seq 1 (\times F) (z) = 1 \to N \gcd seq 1 (\times F) (z) F (z + 1) = 1)$
236	199	oveq2d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to N \gcd seq 1 (\times F) (z + 1) = N \gcd seq 1 (\times F) (z) F (z + 1)$
237	236	eqeq1d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (N \gcd seq 1 (\times F) (z + 1) = 1 \leftrightarrow N \gcd seq 1 (\times F) (z) F (z + 1) = 1)$
238	235 237	sylibrd	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to (N \gcd seq 1 (\times F) (z) = 1 \to N \gcd seq 1 (\times F) (z + 1) = 1)$
239	228 238	anim12d	$⊢ (φ \land (z \in ℕ \land z + 1 \leq ϕ (N))) \to ((A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1) \to (A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N \land N \gcd seq 1 (\times F) (z + 1) = 1))$
240	239	an12s	$⊢ (z \in ℕ \land (φ \land z + 1 \leq ϕ (N))) \to ((A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1) \to (A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N \land N \gcd seq 1 (\times F) (z + 1) = 1))$
241	240	ex	$⊢ z \in ℕ \to ((φ \land z + 1 \leq ϕ (N)) \to ((A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1) \to (A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N \land N \gcd seq 1 (\times F) (z + 1) = 1)))$
242	241	a2d	$⊢ z \in ℕ \to (((φ \land z + 1 \leq ϕ (N)) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1)) \to ((φ \land z + 1 \leq ϕ (N)) \to (A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N \land N \gcd seq 1 (\times F) (z + 1) = 1)))$
243	119 242	syld	$⊢ z \in ℕ \to (((φ \land z \leq ϕ (N)) \to (A^{z} seq 1 (\times F) (z) \mod N = seq 1 (\times G) (z) \mod N \land N \gcd seq 1 (\times F) (z) = 1)) \to ((φ \land z + 1 \leq ϕ (N)) \to (A^{z + 1} seq 1 (\times F) (z + 1) \mod N = seq 1 (\times G) (z + 1) \mod N \land N \gcd seq 1 (\times F) (z + 1) = 1)))$
244	23 36 49 62 108 243	nnind	$⊢ ϕ (N) \in ℕ \to ((φ \land ϕ (N) \leq ϕ (N)) \to (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N \land N \gcd seq 1 (\times F) (ϕ (N)) = 1))$
245	10 244	mpcom	$⊢ (φ \land ϕ (N) \leq ϕ (N)) \to (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N \land N \gcd seq 1 (\times F) (ϕ (N)) = 1)$
246	9 245	mpdan	$⊢ φ \to (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N \land N \gcd seq 1 (\times F) (ϕ (N)) = 1)$
247	246	simpld	$⊢ φ \to A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N$
248	7	nnnn0d	$⊢ φ \to ϕ (N) \in ℕ_{0}$
249		zexpcl	$⊢ (A \in ℤ \land ϕ (N) \in ℕ_{0}) \to A^{ϕ (N)} \in ℤ$
250	63 248 249	syl2anc	$⊢ φ \to A^{ϕ (N)} \in ℤ$
251	3	eleq2i	$⊢ x \in T \leftrightarrow x \in (1 \dots ϕ (N))$
252	251 151	sylan2br	$⊢ (φ \land x \in (1 \dots ϕ (N))) \to F (x) \in ℤ$
253	154	adantl	$⊢ (φ \land (x \in ℤ \land y \in ℤ)) \to x y \in ℤ$
254	67 252 253	seqcl	$⊢ φ \to seq 1 (\times F) (ϕ (N)) \in ℤ$
255	250 254	zmulcld	$⊢ φ \to A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \in ℤ$
256		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
257	256	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
258		mulcom	$⊢ (x \in ℂ \land y \in ℂ) \to x y = y x$
259	258	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x y = y x$
260		mulass	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x y z = x y z$
261	260	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x y z = x y z$
262		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
263		f1ocnv	$⊢ F : T \underset{1-1 onto}{⟶} S \to F^{-1} : S \underset{1-1 onto}{⟶} T$
264	4 263	syl	$⊢ φ \to F^{-1} : S \underset{1-1 onto}{⟶} T$
265	6	adantr	$⊢ (φ \land (y \in T \land z \in T)) \to N \in ℕ$
266	63	adantr	$⊢ (φ \land (y \in T \land z \in T)) \to A \in ℤ$
267	65	ffvelcdmda	$⊢ (φ \land y \in T) \to F (y) \in S$
268	267	adantrr	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) \in S$
269	159 268	sselid	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) \in (0 ..^N)$
270		elfzoelz	$⊢ F (y) \in (0 ..^N) \to F (y) \in ℤ$
271	269 270	syl	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) \in ℤ$
272	266 271	zmulcld	$⊢ (φ \land (y \in T \land z \in T)) \to A F (y) \in ℤ$
273	65	ffvelcdmda	$⊢ (φ \land z \in T) \to F (z) \in S$
274	273	adantrl	$⊢ (φ \land (y \in T \land z \in T)) \to F (z) \in S$
275	159 274	sselid	$⊢ (φ \land (y \in T \land z \in T)) \to F (z) \in (0 ..^N)$
276		elfzoelz	$⊢ F (z) \in (0 ..^N) \to F (z) \in ℤ$
277	275 276	syl	$⊢ (φ \land (y \in T \land z \in T)) \to F (z) \in ℤ$
278	266 277	zmulcld	$⊢ (φ \land (y \in T \land z \in T)) \to A F (z) \in ℤ$
279		moddvds	$⊢ (N \in ℕ \land A F (y) \in ℤ \land A F (z) \in ℤ) \to (A F (y) \mod N = A F (z) \mod N \leftrightarrow N ∥ (A F (y) - A F (z)))$
280	265 272 278 279	syl3anc	$⊢ (φ \land (y \in T \land z \in T)) \to (A F (y) \mod N = A F (z) \mod N \leftrightarrow N ∥ (A F (y) - A F (z)))$
281		fveq2	$⊢ x = y \to F (x) = F (y)$
282	281	oveq2d	$⊢ x = y \to A F (x) = A F (y)$
283	282	oveq1d	$⊢ x = y \to A F (x) \mod N = A F (y) \mod N$
284		ovex	$⊢ A F (y) \mod N \in V$
285	283 5 284	fvmpt	$⊢ y \in T \to G (y) = A F (y) \mod N$
286		fveq2	$⊢ x = z \to F (x) = F (z)$
287	286	oveq2d	$⊢ x = z \to A F (x) = A F (z)$
288	287	oveq1d	$⊢ x = z \to A F (x) \mod N = A F (z) \mod N$
289		ovex	$⊢ A F (z) \mod N \in V$
290	288 5 289	fvmpt	$⊢ z \in T \to G (z) = A F (z) \mod N$
291	285 290	eqeqan12d	$⊢ (y \in T \land z \in T) \to (G (y) = G (z) \leftrightarrow A F (y) \mod N = A F (z) \mod N)$
292	291	adantl	$⊢ (φ \land (y \in T \land z \in T)) \to (G (y) = G (z) \leftrightarrow A F (y) \mod N = A F (z) \mod N)$
293	93	adantr	$⊢ (φ \land (y \in T \land z \in T)) \to A \in ℂ$
294	271	zcnd	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) \in ℂ$
295	277	zcnd	$⊢ (φ \land (y \in T \land z \in T)) \to F (z) \in ℂ$
296	293 294 295	subdid	$⊢ (φ \land (y \in T \land z \in T)) \to A (F (y) - F (z)) = A F (y) - A F (z)$
297	296	breq2d	$⊢ (φ \land (y \in T \land z \in T)) \to (N ∥ A (F (y) - F (z)) \leftrightarrow N ∥ (A F (y) - A F (z)))$
298	280 292 297	3bitr4d	$⊢ (φ \land (y \in T \land z \in T)) \to (G (y) = G (z) \leftrightarrow N ∥ A (F (y) - F (z)))$
299	102 63	gcdcomd	$⊢ φ \to N \gcd A = A \gcd N$
300	1	simp3d	$⊢ φ \to A \gcd N = 1$
301	299 300	eqtrd	$⊢ φ \to N \gcd A = 1$
302	301	adantr	$⊢ (φ \land (y \in T \land z \in T)) \to N \gcd A = 1$
303	102	adantr	$⊢ (φ \land (y \in T \land z \in T)) \to N \in ℤ$
304	271 277	zsubcld	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) - F (z) \in ℤ$
305		coprmdvds	$⊢ (N \in ℤ \land A \in ℤ \land F (y) - F (z) \in ℤ) \to ((N ∥ A (F (y) - F (z)) \land N \gcd A = 1) \to N ∥ (F (y) - F (z)))$
306	303 266 304 305	syl3anc	$⊢ (φ \land (y \in T \land z \in T)) \to ((N ∥ A (F (y) - F (z)) \land N \gcd A = 1) \to N ∥ (F (y) - F (z)))$
307	271	zred	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) \in ℝ$
308	81	adantr	$⊢ (φ \land (y \in T \land z \in T)) \to N \in ℝ^{+}$
309		elfzole1	$⊢ F (y) \in (0 ..^N) \to 0 \leq F (y)$
310	269 309	syl	$⊢ (φ \land (y \in T \land z \in T)) \to 0 \leq F (y)$
311		elfzolt2	$⊢ F (y) \in (0 ..^N) \to F (y) < N$
312	269 311	syl	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) < N$
313		modid	$⊢ ((F (y) \in ℝ \land N \in ℝ^{+}) \land (0 \leq F (y) \land F (y) < N)) \to F (y) \mod N = F (y)$
314	307 308 310 312 313	syl22anc	$⊢ (φ \land (y \in T \land z \in T)) \to F (y) \mod N = F (y)$
315	277	zred	$⊢ (φ \land (y \in T \land z \in T)) \to F (z) \in ℝ$
316		elfzole1	$⊢ F (z) \in (0 ..^N) \to 0 \leq F (z)$
317	275 316	syl	$⊢ (φ \land (y \in T \land z \in T)) \to 0 \leq F (z)$
318		elfzolt2	$⊢ F (z) \in (0 ..^N) \to F (z) < N$
319	275 318	syl	$⊢ (φ \land (y \in T \land z \in T)) \to F (z) < N$
320		modid	$⊢ ((F (z) \in ℝ \land N \in ℝ^{+}) \land (0 \leq F (z) \land F (z) < N)) \to F (z) \mod N = F (z)$
321	315 308 317 319 320	syl22anc	$⊢ (φ \land (y \in T \land z \in T)) \to F (z) \mod N = F (z)$
322	314 321	eqeq12d	$⊢ (φ \land (y \in T \land z \in T)) \to (F (y) \mod N = F (z) \mod N \leftrightarrow F (y) = F (z))$
323		moddvds	$⊢ (N \in ℕ \land F (y) \in ℤ \land F (z) \in ℤ) \to (F (y) \mod N = F (z) \mod N \leftrightarrow N ∥ (F (y) - F (z)))$
324	265 271 277 323	syl3anc	$⊢ (φ \land (y \in T \land z \in T)) \to (F (y) \mod N = F (z) \mod N \leftrightarrow N ∥ (F (y) - F (z)))$
325		f1of1	$⊢ F : T \underset{1-1 onto}{⟶} S \to F : T \underset{1-1}{⟶} S$
326	4 325	syl	$⊢ φ \to F : T \underset{1-1}{⟶} S$
327		f1fveq	$⊢ (F : T \underset{1-1}{⟶} S \land (y \in T \land z \in T)) \to (F (y) = F (z) \leftrightarrow y = z)$
328	326 327	sylan	$⊢ (φ \land (y \in T \land z \in T)) \to (F (y) = F (z) \leftrightarrow y = z)$
329	322 324 328	3bitr3d	$⊢ (φ \land (y \in T \land z \in T)) \to (N ∥ (F (y) - F (z)) \leftrightarrow y = z)$
330	306 329	sylibd	$⊢ (φ \land (y \in T \land z \in T)) \to ((N ∥ A (F (y) - F (z)) \land N \gcd A = 1) \to y = z)$
331	302 330	mpan2d	$⊢ (φ \land (y \in T \land z \in T)) \to (N ∥ A (F (y) - F (z)) \to y = z)$
332	298 331	sylbid	$⊢ (φ \land (y \in T \land z \in T)) \to (G (y) = G (z) \to y = z)$
333	332	ralrimivva	$⊢ φ \to \forall y \in T \forall z \in T (G (y) = G (z) \to y = z)$
334		dff13	$⊢ G : T \underset{1-1}{⟶} S \leftrightarrow (G : T ⟶ S \land \forall y \in T \forall z \in T (G (y) = G (z) \to y = z))$
335	160 333 334	sylanbrc	$⊢ φ \to G : T \underset{1-1}{⟶} S$
336	3	ovexi	$⊢ T \in V$
337	336	f1oen	$⊢ F : T \underset{1-1 onto}{⟶} S \to T \approx S$
338	4 337	syl	$⊢ φ \to T \approx S$
339		fzofi	$⊢ (0 ..^N) \in Fin$
340		ssfi	$⊢ ((0 ..^N) \in Fin \land S \subseteq (0 ..^N)) \to S \in Fin$
341	339 159 340	mp2an	$⊢ S \in Fin$
342		f1finf1o	$⊢ (T \approx S \land S \in Fin) \to (G : T \underset{1-1}{⟶} S \leftrightarrow G : T \underset{1-1 onto}{⟶} S)$
343	338 341 342	sylancl	$⊢ φ \to (G : T \underset{1-1}{⟶} S \leftrightarrow G : T \underset{1-1 onto}{⟶} S)$
344	335 343	mpbid	$⊢ φ \to G : T \underset{1-1 onto}{⟶} S$
345		f1oco	$⊢ (F^{-1} : S \underset{1-1 onto}{⟶} T \land G : T \underset{1-1 onto}{⟶} S) \to (F^{-1} \circ G) : T \underset{1-1 onto}{⟶} T$
346	264 344 345	syl2anc	$⊢ φ \to (F^{-1} \circ G) : T \underset{1-1 onto}{⟶} T$
347		f1oeq23	$⊢ (T = (1 \dots ϕ (N)) \land T = (1 \dots ϕ (N))) \to ((F^{-1} \circ G) : T \underset{1-1 onto}{⟶} T \leftrightarrow (F^{-1} \circ G) : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} (1 \dots ϕ (N)))$
348	3 3 347	mp2an	$⊢ (F^{-1} \circ G) : T \underset{1-1 onto}{⟶} T \leftrightarrow (F^{-1} \circ G) : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} (1 \dots ϕ (N))$
349	346 348	sylib	$⊢ φ \to (F^{-1} \circ G) : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} (1 \dots ϕ (N))$
350	252	zcnd	$⊢ (φ \land x \in (1 \dots ϕ (N))) \to F (x) \in ℂ$
351	3	eleq2i	$⊢ w \in T \leftrightarrow w \in (1 \dots ϕ (N))$
352		fvco3	$⊢ (G : T ⟶ S \land w \in T) \to (F^{-1} \circ G) (w) = F^{-1} (G (w))$
353	160 352	sylan	$⊢ (φ \land w \in T) \to (F^{-1} \circ G) (w) = F^{-1} (G (w))$
354	353	fveq2d	$⊢ (φ \land w \in T) \to F ((F^{-1} \circ G) (w)) = F (F^{-1} (G (w)))$
355	4	adantr	$⊢ (φ \land w \in T) \to F : T \underset{1-1 onto}{⟶} S$
356	160	ffvelcdmda	$⊢ (φ \land w \in T) \to G (w) \in S$
357		f1ocnvfv2	$⊢ (F : T \underset{1-1 onto}{⟶} S \land G (w) \in S) \to F (F^{-1} (G (w))) = G (w)$
358	355 356 357	syl2anc	$⊢ (φ \land w \in T) \to F (F^{-1} (G (w))) = G (w)$
359	354 358	eqtr2d	$⊢ (φ \land w \in T) \to G (w) = F ((F^{-1} \circ G) (w))$
360	351 359	sylan2br	$⊢ (φ \land w \in (1 \dots ϕ (N))) \to G (w) = F ((F^{-1} \circ G) (w))$
361	257 259 261 67 262 349 350 360	seqf1o	$⊢ φ \to seq 1 (\times G) (ϕ (N)) = seq 1 (\times F) (ϕ (N))$
362	361 254	eqeltrd	$⊢ φ \to seq 1 (\times G) (ϕ (N)) \in ℤ$
363		moddvds	$⊢ (N \in ℕ \land A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \in ℤ \land seq 1 (\times G) (ϕ (N)) \in ℤ) \to (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N \leftrightarrow N ∥ (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - seq 1 (\times G) (ϕ (N))))$
364	6 255 362 363	syl3anc	$⊢ φ \to (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) \mod N = seq 1 (\times G) (ϕ (N)) \mod N \leftrightarrow N ∥ (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - seq 1 (\times G) (ϕ (N))))$
365	247 364	mpbid	$⊢ φ \to N ∥ (A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - seq 1 (\times G) (ϕ (N)))$
366	254	zcnd	$⊢ φ \to seq 1 (\times F) (ϕ (N)) \in ℂ$
367	366	mullidd	$⊢ φ \to 1 seq 1 (\times F) (ϕ (N)) = seq 1 (\times F) (ϕ (N))$
368	361 367	eqtr4d	$⊢ φ \to seq 1 (\times G) (ϕ (N)) = 1 seq 1 (\times F) (ϕ (N))$
369	368	oveq2d	$⊢ φ \to A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - seq 1 (\times G) (ϕ (N)) = A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - 1 seq 1 (\times F) (ϕ (N))$
370	250	zcnd	$⊢ φ \to A^{ϕ (N)} \in ℂ$
371		ax-1cn	$⊢ 1 \in ℂ$
372		subdir	$⊢ (A^{ϕ (N)} \in ℂ \land 1 \in ℂ \land seq 1 (\times F) (ϕ (N)) \in ℂ) \to (A^{ϕ (N)} - 1) seq 1 (\times F) (ϕ (N)) = A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - 1 seq 1 (\times F) (ϕ (N))$
373	371 372	mp3an2	$⊢ (A^{ϕ (N)} \in ℂ \land seq 1 (\times F) (ϕ (N)) \in ℂ) \to (A^{ϕ (N)} - 1) seq 1 (\times F) (ϕ (N)) = A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - 1 seq 1 (\times F) (ϕ (N))$
374	370 366 373	syl2anc	$⊢ φ \to (A^{ϕ (N)} - 1) seq 1 (\times F) (ϕ (N)) = A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - 1 seq 1 (\times F) (ϕ (N))$
375		zsubcl	$⊢ (A^{ϕ (N)} \in ℤ \land 1 \in ℤ) \to A^{ϕ (N)} - 1 \in ℤ$
376	250 84 375	sylancl	$⊢ φ \to A^{ϕ (N)} - 1 \in ℤ$
377	376	zcnd	$⊢ φ \to A^{ϕ (N)} - 1 \in ℂ$
378	377 366	mulcomd	$⊢ φ \to (A^{ϕ (N)} - 1) seq 1 (\times F) (ϕ (N)) = seq 1 (\times F) (ϕ (N)) (A^{ϕ (N)} - 1)$
379	369 374 378	3eqtr2d	$⊢ φ \to A^{ϕ (N)} seq 1 (\times F) (ϕ (N)) - seq 1 (\times G) (ϕ (N)) = seq 1 (\times F) (ϕ (N)) (A^{ϕ (N)} - 1)$
380	365 379	breqtrd	$⊢ φ \to N ∥ seq 1 (\times F) (ϕ (N)) (A^{ϕ (N)} - 1)$
381	246	simprd	$⊢ φ \to N \gcd seq 1 (\times F) (ϕ (N)) = 1$
382		coprmdvds	$⊢ (N \in ℤ \land seq 1 (\times F) (ϕ (N)) \in ℤ \land A^{ϕ (N)} - 1 \in ℤ) \to ((N ∥ seq 1 (\times F) (ϕ (N)) (A^{ϕ (N)} - 1) \land N \gcd seq 1 (\times F) (ϕ (N)) = 1) \to N ∥ (A^{ϕ (N)} - 1))$
383	102 254 376 382	syl3anc	$⊢ φ \to ((N ∥ seq 1 (\times F) (ϕ (N)) (A^{ϕ (N)} - 1) \land N \gcd seq 1 (\times F) (ϕ (N)) = 1) \to N ∥ (A^{ϕ (N)} - 1))$
384	380 381 383	mp2and	$⊢ φ \to N ∥ (A^{ϕ (N)} - 1)$
385		moddvds	$⊢ (N \in ℕ \land A^{ϕ (N)} \in ℤ \land 1 \in ℤ) \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
386	84 385	mp3an3	$⊢ (N \in ℕ \land A^{ϕ (N)} \in ℤ) \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
387	6 250 386	syl2anc	$⊢ φ \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
388	384 387	mpbird	$⊢ φ \to A^{ϕ (N)} \mod N = 1 \mod N$

Metamath Proof Explorer

Theorem eulerthlem2

Proof