Theorem eulerthlem2

Description: Lemma for eulerth . (Contributed by Mario Carneiro, 28-Feb-2014)

	Ref	Expression
Hypotheses	eulerth.1	|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )
	eulerth.2	|- S = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 }
	eulerth.3	|- T = ( 1 ... ( phi ` N ) )
	eulerth.4	|- ( ph -> F : T -1-1-onto-> S )
	eulerth.5	|- G = ( x e. T |-> ( ( A x. ( F ` x ) ) mod N ) )
Assertion	eulerthlem2	|- ( ph -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )

Proof

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