MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eulerthlem2 Unicode version

Theorem eulerthlem2 12850
Description: Lemma for eulerth 12851. (Contributed by Mario Carneiro, 28-Feb-2014.)
Hypotheses
Ref Expression
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
Ref Expression
eulerthlem2  |-  ( ph  ->  ( ( A ^
( phi `  N
) )  mod  N
)  =  ( 1  mod  N ) )
Distinct variable groups:    x, y, A    x, F, y    x, G, y    x, N, y   
x, S    ph, x, y   
x, T, y
Allowed substitution hint:    S( y)

Proof of Theorem eulerthlem2
Dummy variables  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eulerth.1 . . . . . . . . . . 11  |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 ) )
21simp1d 967 . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
32phicld 12840 . . . . . . . . 9  |-  ( ph  ->  ( phi `  N
)  e.  NN )
43nnred 9761 . . . . . . . 8  |-  ( ph  ->  ( phi `  N
)  e.  RR )
54leidd 9339 . . . . . . 7  |-  ( ph  ->  ( phi `  N
)  <_  ( phi `  N ) )
63adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( phi `  N )  <_  ( phi `  N ) )  ->  ( phi `  N )  e.  NN )
7 breq1 4026 . . . . . . . . . . 11  |-  ( x  =  1  ->  (
x  <_  ( phi `  N )  <->  1  <_  ( phi `  N ) ) )
87anbi2d 684 . . . . . . . . . 10  |-  ( x  =  1  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  1  <_  ( phi `  N ) ) ) )
9 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( x  =  1  ->  ( A ^ x )  =  ( A ^ 1 ) )
10 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( x  =  1  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  1
) )
119, 10oveq12d 5876 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ 1 )  x.  (  seq  1 (  x.  ,  F ) `  1
) ) )
1211oveq1d 5873 . . . . . . . . . . . 12  |-  ( x  =  1  ->  (
( ( A ^
x )  x.  (  seq  1 (  x.  ,  F ) `  x
) )  mod  N
)  =  ( ( ( A ^ 1 )  x.  (  seq  1 (  x.  ,  F ) `  1
) )  mod  N
) )
13 fveq2 5525 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  1
) )
1413oveq1d 5873 . . . . . . . . . . . 12  |-  ( x  =  1  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 1 )  mod 
N ) )
1512, 14eqeq12d 2297 . . . . . . . . . . 11  |-  ( 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
) ) )
1610oveq2d 5874 . . . . . . . . . . . 12  |-  ( x  =  1  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  1 )
) )
1716eqeq1d 2291 . . . . . . . . . . 11  |-  ( x  =  1  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  1
) )  =  1 ) )
1815, 17anbi12d 691 . . . . . . . . . 10  |-  ( 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 ) ) )
198, 18imbi12d 311 . . . . . . . . 9  |-  ( 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 ) ) ) )
20 breq1 4026 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
x  <_  ( phi `  N )  <->  z  <_  ( phi `  N ) ) )
2120anbi2d 684 . . . . . . . . . 10  |-  ( x  =  z  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  z  <_  ( phi `  N ) ) ) )
22 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( x  =  z  ->  ( A ^ x )  =  ( A ^ z
) )
23 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( x  =  z  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  z
) )
2422, 23oveq12d 5876 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ z
)  x.  (  seq  1 (  x.  ,  F ) `  z
) ) )
2524oveq1d 5873 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( ( A ^
x )  x.  (  seq  1 (  x.  ,  F ) `  x
) )  mod  N
)  =  ( ( ( A ^ z
)  x.  (  seq  1 (  x.  ,  F ) `  z
) )  mod  N
) )
26 fveq2 5525 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  z
) )
2726oveq1d 5873 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 z )  mod 
N ) )
2825, 27eqeq12d 2297 . . . . . . . . . . 11  |-  ( 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
) ) )
2923oveq2d 5874 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  z )
) )
3029eqeq1d 2291 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  z
) )  =  1 ) )
3128, 30anbi12d 691 . . . . . . . . . 10  |-  ( 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 ) ) )
3221, 31imbi12d 311 . . . . . . . . 9  |-  ( 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 ) ) ) )
33 breq1 4026 . . . . . . . . . . 11  |-  ( x  =  ( z  +  1 )  ->  (
x  <_  ( phi `  N )  <->  ( z  +  1 )  <_ 
( phi `  N
) ) )
3433anbi2d 684 . . . . . . . . . 10  |-  ( x  =  ( z  +  1 )  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  ( z  +  1 )  <_  ( phi `  N ) ) ) )
35 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( x  =  ( z  +  1 )  ->  ( A ^ x )  =  ( A ^ (
z  +  1 ) ) )
36 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( x  =  ( z  +  1 )  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) ) )
3735, 36oveq12d 5876 . . . . . . . . . . . . 13  |-  ( x  =  ( z  +  1 )  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ (
z  +  1 ) )  x.  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) ) ) )
3837oveq1d 5873 . . . . . . . . . . . 12  |-  ( 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
) )
39 fveq2 5525 . . . . . . . . . . . . 13  |-  ( x  =  ( z  +  1 )  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  (
z  +  1 ) ) )
4039oveq1d 5873 . . . . . . . . . . . 12  |-  ( x  =  ( z  +  1 )  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 ( z  +  1 ) )  mod 
N ) )
4138, 40eqeq12d 2297 . . . . . . . . . . 11  |-  ( 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
) ) )
4236oveq2d 5874 . . . . . . . . . . . 12  |-  ( x  =  ( z  +  1 )  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  ( z  +  1 ) ) ) )
4342eqeq1d 2291 . . . . . . . . . . 11  |-  ( x  =  ( z  +  1 )  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) ) )  =  1 ) )
4441, 43anbi12d 691 . . . . . . . . . 10  |-  ( 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 ) ) )
4534, 44imbi12d 311 . . . . . . . . 9  |-  ( 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 ) ) ) )
46 breq1 4026 . . . . . . . . . . 11  |-  ( x  =  ( phi `  N )  ->  (
x  <_  ( phi `  N )  <->  ( phi `  N )  <_  ( phi `  N ) ) )
4746anbi2d 684 . . . . . . . . . 10  |-  ( x  =  ( phi `  N )  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  ( phi `  N
)  <_  ( phi `  N ) ) ) )
48 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( x  =  ( phi `  N )  ->  ( A ^ x )  =  ( A ^ ( phi `  N ) ) )
49 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( x  =  ( phi `  N )  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )
5048, 49oveq12d 5876 . . . . . . . . . . . . 13  |-  ( x  =  ( phi `  N )  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ ( phi `  N ) )  x.  (  seq  1
(  x.  ,  F
) `  ( phi `  N ) ) ) )
5150oveq1d 5873 . . . . . . . . . . . 12  |-  ( 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 ) )
52 fveq2 5525 . . . . . . . . . . . . 13  |-  ( x  =  ( phi `  N )  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  ( phi `  N ) ) )
5352oveq1d 5873 . . . . . . . . . . . 12  |-  ( x  =  ( phi `  N )  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 ( phi `  N ) )  mod 
N ) )
5451, 53eqeq12d 2297 . . . . . . . . . . 11  |-  ( 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 ) ) )
5549oveq2d 5874 . . . . . . . . . . . 12  |-  ( x  =  ( phi `  N )  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  ( phi `  N ) ) ) )
5655eqeq1d 2291 . . . . . . . . . . 11  |-  ( x  =  ( phi `  N )  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )  =  1 ) )
5754, 56anbi12d 691 . . . . . . . . . 10  |-  ( 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 ) ) )
5847, 57imbi12d 311 . . . . . . . . 9  |-  ( 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 ) ) ) )
591simp2d 968 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  ZZ )
60 eulerth.4 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F : T -1-1-onto-> S )
61 f1of 5472 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : T -1-1-onto-> S  ->  F : T
--> S )
6260, 61syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : T --> S )
63 nnuz 10263 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN  =  ( ZZ>= `  1 )
643, 63syl6eleq 2373 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( phi `  N
)  e.  ( ZZ>= ` 
1 ) )
65 eluzfz1 10803 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( phi `  N )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( phi `  N ) ) )
6664, 65syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  1  e.  ( 1 ... ( phi `  N ) ) )
67 eulerth.3 . . . . . . . . . . . . . . . . . . . 20  |-  T  =  ( 1 ... ( phi `  N ) )
6866, 67syl6eleqr 2374 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  1  e.  T )
69 ffvelrn 5663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : T --> S  /\  1  e.  T )  ->  ( F `  1
)  e.  S )
7062, 68, 69syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F `  1
)  e.  S )
71 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( F ` 
1 )  ->  (
y  gcd  N )  =  ( ( F `
 1 )  gcd 
N ) )
7271eqeq1d 2291 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( F ` 
1 )  ->  (
( y  gcd  N
)  =  1  <->  (
( F `  1
)  gcd  N )  =  1 ) )
73 eulerth.2 . . . . . . . . . . . . . . . . . . 19  |-  S  =  { y  e.  ( 0..^ N )  |  ( y  gcd  N
)  =  1 }
7472, 73elrab2 2925 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  1 )  e.  S  <->  ( ( F `  1 )  e.  ( 0..^ N )  /\  ( ( F `
 1 )  gcd 
N )  =  1 ) )
7570, 74sylib 188 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( F ` 
1 )  e.  ( 0..^ N )  /\  ( ( F ` 
1 )  gcd  N
)  =  1 ) )
7675simpld 445 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F `  1
)  e.  ( 0..^ N ) )
77 elfzoelz 10875 . . . . . . . . . . . . . . . 16  |-  ( ( F `  1 )  e.  ( 0..^ N )  ->  ( F `  1 )  e.  ZZ )
7876, 77syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  1
)  e.  ZZ )
7959, 78zmulcld 10123 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  x.  ( F `  1 )
)  e.  ZZ )
8079zred 10117 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  x.  ( F `  1 )
)  e.  RR )
812nnrpd 10389 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  RR+ )
82 modabs2 10998 . . . . . . . . . . . . 13  |-  ( ( ( A  x.  ( F `  1 )
)  e.  RR  /\  N  e.  RR+ )  -> 
( ( ( A  x.  ( F ` 
1 ) )  mod 
N )  mod  N
)  =  ( ( A  x.  ( F `
 1 ) )  mod  N ) )
8380, 81, 82syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  x.  ( F ` 
1 ) )  mod 
N )  mod  N
)  =  ( ( A  x.  ( F `
 1 ) )  mod  N ) )
84 1z 10053 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
85 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  1  ->  ( F `  x )  =  ( F ` 
1 ) )
8685oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( x  =  1  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  1 )
) )
8786oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( x  =  1  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F ` 
1 ) )  mod 
N ) )
88 eulerth.5 . . . . . . . . . . . . . . . 16  |-  G  =  ( x  e.  T  |->  ( ( A  x.  ( F `  x ) )  mod  N ) )
89 ovex 5883 . . . . . . . . . . . . . . . 16  |-  ( ( A  x.  ( F `
 1 ) )  mod  N )  e. 
_V
9087, 88, 89fvmpt 5602 . . . . . . . . . . . . . . 15  |-  ( 1  e.  T  ->  ( G `  1 )  =  ( ( A  x.  ( F ` 
1 ) )  mod 
N ) )
9168, 90syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  1
)  =  ( ( A  x.  ( F `
 1 ) )  mod  N ) )
9284, 91seq1i 11060 . . . . . . . . . . . . 13  |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `
 1 )  =  ( ( A  x.  ( F `  1 ) )  mod  N ) )
9392oveq1d 5873 . . . . . . . . . . . 12  |-  ( ph  ->  ( (  seq  1
(  x.  ,  G
) `  1 )  mod  N )  =  ( ( ( A  x.  ( F `  1 ) )  mod  N )  mod  N ) )
9459zcnd 10118 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  CC )
9594exp1d 11240 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A ^ 1 )  =  A )
96 seq1 11059 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  ->  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 ) )
9784, 96ax-mp 8 . . . . . . . . . . . . . . 15  |-  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 )
9897a1i 10 . . . . . . . . . . . . . 14  |-  ( ph  ->  (  seq  1 (  x.  ,  F ) `
 1 )  =  ( F `  1
) )
9995, 98oveq12d 5876 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A ^
1 )  x.  (  seq  1 (  x.  ,  F ) `  1
) )  =  ( A  x.  ( F `
 1 ) ) )
10099oveq1d 5873 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A ^ 1 )  x.  (  seq  1 (  x.  ,  F ) `
 1 ) )  mod  N )  =  ( ( A  x.  ( F `  1 ) )  mod  N ) )
10183, 93, 1003eqtr4rd 2326 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( A ^ 1 )  x.  (  seq  1 (  x.  ,  F ) `
 1 ) )  mod  N )  =  ( (  seq  1
(  x.  ,  G
) `  1 )  mod  N ) )
10297oveq2i 5869 . . . . . . . . . . . 12  |-  ( N  gcd  (  seq  1
(  x.  ,  F
) `  1 )
)  =  ( N  gcd  ( F ` 
1 ) )
1032nnzd 10116 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ZZ )
104 gcdcom 12699 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ZZ  /\  ( F `  1 )  e.  ZZ )  -> 
( N  gcd  ( F `  1 )
)  =  ( ( F `  1 )  gcd  N ) )
105103, 78, 104syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  gcd  ( F `  1 )
)  =  ( ( F `  1 )  gcd  N ) )
10675simprd 449 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( F ` 
1 )  gcd  N
)  =  1 )
107105, 106eqtrd 2315 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  gcd  ( F `  1 )
)  =  1 )
108102, 107syl5eq 2327 . . . . . . . . . . 11  |-  ( ph  ->  ( N  gcd  (  seq  1 (  x.  ,  F ) `  1
) )  =  1 )
109101, 108jca 518 . . . . . . . . . 10  |-  ( 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 ) )
110109adantr 451 . . . . . . . . 9  |-  ( (
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 ) )
111 nnre 9753 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN  ->  z  e.  RR )
112111adantr 451 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  ph )  ->  z  e.  RR )
113112lep1d 9688 . . . . . . . . . . . . 13  |-  ( ( z  e.  NN  /\  ph )  ->  z  <_  ( z  +  1 ) )
114 peano2re 8985 . . . . . . . . . . . . . . 15  |-  ( z  e.  RR  ->  (
z  +  1 )  e.  RR )
115112, 114syl 15 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  ph )  ->  ( z  +  1 )  e.  RR )
1164adantl 452 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  ph )  ->  ( phi `  N )  e.  RR )
117 letr 8914 . . . . . . . . . . . . . 14  |-  ( ( z  e.  RR  /\  ( z  +  1 )  e.  RR  /\  ( phi `  N )  e.  RR )  -> 
( ( z  <_ 
( z  +  1 )  /\  ( z  +  1 )  <_ 
( phi `  N
) )  ->  z  <_  ( phi `  N
) ) )
118112, 115, 116, 117syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( z  e.  NN  /\  ph )  ->  ( (
z  <_  ( z  +  1 )  /\  ( z  +  1 )  <_  ( phi `  N ) )  -> 
z  <_  ( phi `  N ) ) )
119113, 118mpand 656 . . . . . . . . . . . 12  |-  ( ( z  e.  NN  /\  ph )  ->  ( (
z  +  1 )  <_  ( phi `  N )  ->  z  <_  ( phi `  N
) ) )
120119imdistanda 674 . . . . . . . . . . 11  |-  ( z  e.  NN  ->  (
( ph  /\  (
z  +  1 )  <_  ( phi `  N ) )  -> 
( ph  /\  z  <_  ( phi `  N
) ) ) )
121120imim1d 69 . . . . . . . . . 10  |-  ( 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 ) ) ) )
12259adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  A  e.  ZZ )
123 nnnn0 9972 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  NN  ->  z  e.  NN0 )
124123ad2antrl 708 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  NN0 )
125 zexpcl 11118 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ZZ  /\  z  e.  NN0 )  -> 
( A ^ z
)  e.  ZZ )
126122, 124, 125syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A ^ z
)  e.  ZZ )
127 simprl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  NN )
128127, 63syl6eleq 2373 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  ( ZZ>= ` 
1 ) )
129111ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  RR )
130129, 114syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  RR )
1314adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( phi `  N
)  e.  RR )
132129lep1d 9688 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  <_  ( z  +  1 ) )
133 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  <_  ( phi `  N ) )
134129, 130, 131, 132, 133letrd 8973 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  <_  ( phi `  N ) )
135 nnz 10045 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  NN  ->  z  e.  ZZ )
136135ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  ZZ )
1373nnzd 10116 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( phi `  N
)  e.  ZZ )
138137adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( phi `  N
)  e.  ZZ )
139 eluz 10241 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( z  e.  ZZ  /\  ( phi `  N )  e.  ZZ )  -> 
( ( phi `  N )  e.  (
ZZ>= `  z )  <->  z  <_  ( phi `  N ) ) )
140136, 138, 139syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( phi `  N )  e.  (
ZZ>= `  z )  <->  z  <_  ( phi `  N ) ) )
141134, 140mpbird 223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( phi `  N
)  e.  ( ZZ>= `  z ) )
142 fzss2 10831 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( phi `  N )  e.  ( ZZ>= `  z
)  ->  ( 1 ... z )  C_  ( 1 ... ( phi `  N ) ) )
143141, 142syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( 1 ... z
)  C_  ( 1 ... ( phi `  N ) ) )
144143, 67syl6sseqr 3225 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( 1 ... z
)  C_  T )
145144sselda 3180 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  ( 1 ... z ) )  ->  x  e.  T )
146 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : T --> S  /\  x  e.  T )  ->  ( F `  x
)  e.  S )
14762, 146sylan 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  T )  ->  ( F `  x )  e.  S )
148 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( F `  x )  ->  (
y  gcd  N )  =  ( ( F `
 x )  gcd 
N ) )
149148eqeq1d 2291 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( F `  x )  ->  (
( y  gcd  N
)  =  1  <->  (
( F `  x
)  gcd  N )  =  1 ) )
150149, 73elrab2 2925 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  x )  e.  S  <->  ( ( F `  x )  e.  ( 0..^ N )  /\  ( ( F `
 x )  gcd 
N )  =  1 ) )
151147, 150sylib 188 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  T )  ->  (
( F `  x
)  e.  ( 0..^ N )  /\  (
( F `  x
)  gcd  N )  =  1 ) )
152151simpld 445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  T )  ->  ( F `  x )  e.  ( 0..^ N ) )
153 elfzoelz 10875 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  x )  e.  ( 0..^ N )  ->  ( F `  x )  e.  ZZ )
154152, 153syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  T )  ->  ( F `  x )  e.  ZZ )
155154adantlr 695 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  T
)  ->  ( F `  x )  e.  ZZ )
156145, 155syldan 456 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  ( 1 ... z ) )  ->  ( F `  x )  e.  ZZ )
157 zmulcl 10066 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ZZ  /\  y  e.  ZZ )  ->  ( x  x.  y
)  e.  ZZ )
158157adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  ( x  e.  ZZ  /\  y  e.  ZZ ) )  -> 
( x  x.  y
)  e.  ZZ )
159128, 156, 158seqcl 11066 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  F ) `
 z )  e.  ZZ )
160126, 159zmulcld 10123 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A ^
z )  x.  (  seq  1 (  x.  ,  F ) `  z
) )  e.  ZZ )
161160zred 10117 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A ^
z )  x.  (  seq  1 (  x.  ,  F ) `  z
) )  e.  RR )
162 ssrab2 3258 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }  C_  (
0..^ N )
16373, 162eqsstri 3208 . . . . . . . . . . . . . . . . . . . . . 22  |-  S  C_  ( 0..^ N )
1641, 73, 67, 60, 88eulerthlem1 12849 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  G : T --> S )
165 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( G : T --> S  /\  x  e.  T )  ->  ( G `  x
)  e.  S )
166164, 165sylan 457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  T )  ->  ( G `  x )  e.  S )
167163, 166sseldi 3178 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  T )  ->  ( G `  x )  e.  ( 0..^ N ) )
168 elfzoelz 10875 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  x )  e.  ( 0..^ N )  ->  ( G `  x )  e.  ZZ )
169167, 168syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  T )  ->  ( G `  x )  e.  ZZ )
170169adantlr 695 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  T
)  ->  ( G `  x )  e.  ZZ )
171145, 170syldan 456 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  ( 1 ... z ) )  ->  ( G `  x )  e.  ZZ )
172128, 171, 158seqcl 11066 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 z )  e.  ZZ )
173172zred 10117 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 z )  e.  RR )
17462adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  F : T --> S )
175 peano2nn 9758 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  NN  ->  (
z  +  1 )  e.  NN )
176175ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  NN )
177176nnge1d 9788 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
1  <_  ( z  +  1 ) )
178176nnzd 10116 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  ZZ )
179 elfz 10788 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( z  +  1 )  e.  ZZ  /\  1  e.  ZZ  /\  ( phi `  N )  e.  ZZ )  ->  (
( z  +  1 )  e.  ( 1 ... ( phi `  N ) )  <->  ( 1  <_  ( z  +  1 )  /\  (
z  +  1 )  <_  ( phi `  N ) ) ) )
18084, 179mp3an2 1265 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( z  +  1 )  e.  ZZ  /\  ( phi `  N )  e.  ZZ )  -> 
( ( z  +  1 )  e.  ( 1 ... ( phi `  N ) )  <->  ( 1  <_  ( z  +  1 )  /\  (
z  +  1 )  <_  ( phi `  N ) ) ) )
181178, 138, 180syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( z  +  1 )  e.  ( 1 ... ( phi `  N ) )  <->  ( 1  <_  ( z  +  1 )  /\  (
z  +  1 )  <_  ( phi `  N ) ) ) )
182177, 133, 181mpbir2and 888 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  ( 1 ... ( phi `  N ) ) )
183182, 67syl6eleqr 2374 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  T )
184 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : T --> S  /\  ( z  +  1 )  e.  T )  ->  ( F `  ( z  +  1 ) )  e.  S
)
185174, 183, 184syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  S )
186 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( F `  ( z  +  1 ) )  ->  (
y  gcd  N )  =  ( ( F `
 ( z  +  1 ) )  gcd 
N ) )
187186eqeq1d 2291 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( F `  ( z  +  1 ) )  ->  (
( y  gcd  N
)  =  1  <->  (
( F `  (
z  +  1 ) )  gcd  N )  =  1 ) )
188187, 73elrab2 2925 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  ( z  +  1 ) )  e.  S  <->  ( ( F `  ( z  +  1 ) )  e.  ( 0..^ N )  /\  ( ( F `  ( z  +  1 ) )  gcd  N )  =  1 ) )
189185, 188sylib 188 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( F `  ( z  +  1 ) )  e.  ( 0..^ N )  /\  ( ( F `  ( z  +  1 ) )  gcd  N
)  =  1 ) )
190189simpld 445 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  ( 0..^ N ) )
191 elfzoelz 10875 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  ( z  +  1 ) )  e.  ( 0..^ N )  ->  ( F `  ( z  +  1 ) )  e.  ZZ )
192190, 191syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  ZZ )
193122, 192zmulcld 10123 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A  x.  ( F `  ( z  +  1 ) ) )  e.  ZZ )
19481adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  N  e.  RR+ )
195 modmul1 11002 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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
) )
1961953expia 1153 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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
) ) )
197161, 173, 193, 194, 196syl22anc 1183 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) )
198126zcnd 10118 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A ^ z
)  e.  CC )
199159zcnd 10118 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  F ) `
 z )  e.  CC )
20094adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  A  e.  CC )
201192zcnd 10118 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  CC )
202198, 199, 200, 201mul4d 9024 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) ) ) ) )
203200, 124expp1d 11246 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A ^ (
z  +  1 ) )  =  ( ( A ^ z )  x.  A ) )
204 seqp1 11061 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ZZ>= `  1
)  ->  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) )  =  ( (  seq  1 (  x.  ,  F ) `  z )  x.  ( F `  ( z  +  1 ) ) ) )
205128, 204syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  F ) `
 ( z  +  1 ) )  =  ( (  seq  1
(  x.  ,  F
) `  z )  x.  ( F `  (
z  +  1 ) ) ) )
206203, 205oveq12d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) ) ) ) )
207202, 206eqtr4d 2318 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) ) ) )
208207oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) )
209193zred 10117 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A  x.  ( F `  ( z  +  1 ) ) )  e.  RR )
210209, 194modcld 10977 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A  x.  ( F `  ( z  +  1 ) ) )  mod  N )  e.  RR )
211 modabs2 10998 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) )
212209, 194, 211syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( ( A  x.  ( F `  ( z  +  1 ) ) )  mod 
N )  mod  N
)  =  ( ( A  x.  ( F `
 ( z  +  1 ) ) )  mod  N ) )
213 modmul1 11002 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 )
)
214210, 209, 172, 194, 212, 213syl221anc 1193 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) )
215 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( z  +  1 )  ->  ( F `  x )  =  ( F `  ( z  +  1 ) ) )
216215oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( z  +  1 )  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  ( z  +  1 ) ) ) )
217216oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( z  +  1 )  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F `  ( z  +  1 ) ) )  mod 
N ) )
218 ovex 5883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  x.  ( F `
 ( z  +  1 ) ) )  mod  N )  e. 
_V
219217, 88, 218fvmpt 5602 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  +  1 )  e.  T  ->  ( G `  ( z  +  1 ) )  =  ( ( A  x.  ( F `  ( z  +  1 ) ) )  mod 
N ) )
220183, 219syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( G `  (
z  +  1 ) )  =  ( ( A  x.  ( F `
 ( z  +  1 ) ) )  mod  N ) )
221220oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) )
222 seqp1 11061 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ZZ>= `  1
)  ->  (  seq  1 (  x.  ,  G ) `  (
z  +  1 ) )  =  ( (  seq  1 (  x.  ,  G ) `  z )  x.  ( G `  ( z  +  1 ) ) ) )
223128, 222syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 ( z  +  1 ) )  =  ( (  seq  1
(  x.  ,  G
) `  z )  x.  ( G `  (
z  +  1 ) ) ) )
224210recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A  x.  ( F `  ( z  +  1 ) ) )  mod  N )  e.  CC )
225172zcnd 10118 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 z )  e.  CC )
226224, 225mulcomd 8856 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) )
227221, 223, 2263eqtr4d 2325 . . . . . . . . . . . . . . . . . 18  |-  ( (
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
) ) )
228227oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) )
229193zcnd 10118 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A  x.  ( F `  ( z  +  1 ) ) )  e.  CC )
230225, 229mulcomd 8856 . . . . . . . . . . . . . . . . . 18  |-  ( (
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
) ) )
231230oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) )
232214, 228, 2313eqtr4rd 2326 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) )
233208, 232eqeq12d 2297 . . . . . . . . . . . . . . 15  |-  ( (
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
) ) )
234197, 233sylibd 205 . . . . . . . . . . . . . 14  |-  ( (
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 ) ) )
235103adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  N  e.  ZZ )
236 gcdcom 12699 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ZZ  /\  ( F `  ( z  +  1 ) )  e.  ZZ )  -> 
( N  gcd  ( F `  ( z  +  1 ) ) )  =  ( ( F `  ( z  +  1 ) )  gcd  N ) )
237235, 192, 236syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( N  gcd  ( F `  ( z  +  1 ) ) )  =  ( ( F `  ( z  +  1 ) )  gcd  N ) )
238189simprd 449 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( F `  ( z  +  1 ) )  gcd  N
)  =  1 )
239237, 238eqtrd 2315 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( N  gcd  ( F `  ( z  +  1 ) ) )  =  1 )
240 rpmul 12802 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) )
241235, 159, 192, 240syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) )
242239, 241mpan2d 655 . . . . . . . . . . . . . . 15  |-  ( (
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 ) )
243205oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) ) ) ) )
244243eqeq1d 2291 . . . . . . . . . . . . . . 15  |-  ( (
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 ) )
245242, 244sylibrd 225 . . . . . . . . . . . . . 14  |-  ( (
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 ) )
246234, 245anim12d 546 . . . . . . . . . . . . 13  |-  ( (
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 ) ) )
247246an12s 776 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
248247ex 423 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
249248a2d 23 . . . . . . . . . 10  |-  ( 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 ) ) ) )
250121, 249syld 40 . . . . . . . . 9  |-  ( 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 ) ) ) )
25119, 32, 45, 58, 110, 250nnind 9764 . . . . . . . 8  |-  ( ( 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 ) ) )
2526, 251mpcom 32 . . . . . . 7  |-  ( (
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 ) )
2535, 252mpdan 649 . . . . . 6  |-  ( 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 ) )
254253simpld 445 . . . . 5  |-  ( ph  ->  ( ( ( A ^ ( phi `  N ) )  x.  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) ) )  mod  N )  =  ( (  seq  1
(  x.  ,  G
) `  ( phi `  N ) )  mod 
N ) )
2553nnnn0d 10018 . . . . . . . 8  |-  ( ph  ->  ( phi `  N
)  e.  NN0 )
256 zexpcl 11118 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  ( phi `  N )  e.  NN0 )  -> 
( A ^ ( phi `  N ) )  e.  ZZ )
25759, 255, 256syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( A ^ ( phi `  N ) )  e.  ZZ )
25867eleq2i 2347 . . . . . . . . 9  |-  ( x  e.  T  <->  x  e.  ( 1 ... ( phi `  N ) ) )
259258, 154sylan2br 462 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( phi `  N ) ) )  ->  ( F `  x )  e.  ZZ )
260157adantl 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ZZ  /\  y  e.  ZZ ) )  -> 
( x  x.  y
)  e.  ZZ )
26164, 259, 260seqcl 11066 . . . . . . 7  |-  ( ph  ->  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) )  e.  ZZ )
262257, 261zmulcld 10123 . . . . . 6  |-  ( ph  ->  ( ( A ^
( phi `  N
) )  x.  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )  e.  ZZ )
263 mulcl 8821 . . . . . . . . 9  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
264263adantl 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  e.  CC )
265 mulcom 8823 . . . . . . . . 9  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  =  ( y  x.  x ) )
266265adantl 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  =  ( y  x.  x ) )
267 mulass 8825 . . . . . . . . 9  |-  ( ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC )  ->  (
( x  x.  y
)  x.  z )  =  ( x  x.  ( y  x.  z
) ) )
268267adantl 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC ) )  -> 
( ( x  x.  y )  x.  z
)  =  ( x  x.  ( y  x.  z ) ) )
269 ssid 3197 . . . . . . . . 9  |-  CC  C_  CC
270269a1i 10 . . . . . . . 8  |-  ( ph  ->  CC  C_  CC )
271 f1ocnv 5485 . . . . . . . . . . 11  |-  ( F : T -1-1-onto-> S  ->  `' F : S -1-1-onto-> T )
27260, 271syl 15 . . . . . . . . . 10  |-  ( ph  ->  `' F : S -1-1-onto-> T )
2732adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  N  e.  NN )
27459adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  A  e.  ZZ )
275 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : T --> S  /\  y  e.  T )  ->  ( F `  y
)  e.  S )
27662, 275sylan 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  T )  ->  ( F `  y )  e.  S )
277276adantrr 697 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  S )
278163, 277sseldi 3178 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  ( 0..^ N ) )
279 elfzoelz 10875 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  ( 0..^ N )  ->  ( F `  y )  e.  ZZ )
280278, 279syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  ZZ )
281274, 280zmulcld 10123 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( A  x.  ( F `  y )
)  e.  ZZ )
282 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : T --> S  /\  z  e.  T )  ->  ( F `  z
)  e.  S )
28362, 282sylan 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  T )  ->  ( F `  z )  e.  S )
284283adantrl 696 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  S )
285163, 284sseldi 3178 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  ( 0..^ N ) )
286 elfzoelz 10875 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  z )  e.  ( 0..^ N )  ->  ( F `  z )  e.  ZZ )
287285, 286syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  ZZ )
288274, 287zmulcld 10123 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( A  x.  ( F `  z )
)  e.  ZZ )
289 moddvds 12538 . . . . . . . . . . . . . . . 16  |-  ( ( 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 )
) ) ) )
290273, 281, 288, 289syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
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 )
) ) ) )
291 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
292291oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  y )
) )
293292oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F `  y ) )  mod 
N ) )
294 ovex 5883 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  x.  ( F `
 y ) )  mod  N )  e. 
_V
295293, 88, 294fvmpt 5602 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  T  ->  ( G `  y )  =  ( ( A  x.  ( F `  y ) )  mod 
N ) )
296 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
297296oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  z )
) )
298297oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  z  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) )
299 ovex 5883 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  x.  ( F `
 z ) )  mod  N )  e. 
_V
300298, 88, 299fvmpt 5602 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  T  ->  ( G `  z )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) )
301295, 300eqeqan12d 2298 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  T  /\  z  e.  T )  ->  ( ( G `  y )  =  ( G `  z )  <-> 
( ( A  x.  ( F `  y ) )  mod  N )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) ) )
302301adantl 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( G `  y )  =  ( G `  z )  <-> 
( ( A  x.  ( F `  y ) )  mod  N )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) ) )
30394adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  A  e.  CC )
304280zcnd 10118 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  CC )
305287zcnd 10118 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  CC )
306303, 304, 305subdid 9235 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( A  x.  (
( F `  y
)  -  ( F `
 z ) ) )  =  ( ( A  x.  ( F `
 y ) )  -  ( A  x.  ( F `  z ) ) ) )
307306breq2d 4035 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  ||  ( A  x.  ( ( F `  y )  -  ( F `  z ) ) )  <-> 
N  ||  ( ( A  x.  ( F `  y ) )  -  ( A  x.  ( F `  z )
) ) ) )
308290, 302, 3073bitr4d 276 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( G `  y )  =  ( G `  z )  <-> 
N  ||  ( A  x.  ( ( F `  y )  -  ( F `  z )
) ) ) )
309 gcdcom 12699 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ZZ  /\  A  e.  ZZ )  ->  ( N  gcd  A
)  =  ( A  gcd  N ) )
310103, 59, 309syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  gcd  A
)  =  ( A  gcd  N ) )
3111simp3d 969 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  gcd  N
)  =  1 )
312310, 311eqtrd 2315 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  gcd  A
)  =  1 )
313312adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  gcd  A
)  =  1 )
314103adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  N  e.  ZZ )
315280, 287zsubcld 10122 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  y )  -  ( F `  z )
)  e.  ZZ )
316 coprmdvds 12781 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
) ) )
317314, 274, 315, 316syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( N  ||  ( A  x.  (
( F `  y
)  -  ( F `
 z ) ) )  /\  ( N  gcd  A )  =  1 )  ->  N  ||  ( ( F `  y )  -  ( F `  z )
) ) )
318280zred 10117 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  RR )
31981adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  N  e.  RR+ )
320 elfzole1 10882 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  y )  e.  ( 0..^ N )  ->  0  <_  ( F `  y ) )
321278, 320syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
0  <_  ( F `  y ) )
322 elfzolt2 10883 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  y )  e.  ( 0..^ N )  ->  ( F `  y )  <  N
)
323278, 322syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  <  N )
324 modid 10993 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  y )  e.  RR  /\  N  e.  RR+ )  /\  ( 0  <_  ( F `  y )  /\  ( F `  y
)  <  N )
)  ->  ( ( F `  y )  mod  N )  =  ( F `  y ) )
325318, 319, 321, 323, 324syl22anc 1183 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  y )  mod  N
)  =  ( F `
 y ) )
326287zred 10117 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  RR )
327 elfzole1 10882 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z )  e.  ( 0..^ N )  ->  0  <_  ( F `  z ) )
328285, 327syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
0  <_  ( F `  z ) )
329 elfzolt2 10883 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z )  e.  ( 0..^ N )  ->  ( F `  z )  <  N
)
330285, 329syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  <  N )
331 modid 10993 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  z )  e.  RR  /\  N  e.  RR+ )  /\  ( 0  <_  ( F `  z )  /\  ( F `  z
)  <  N )
)  ->  ( ( F `  z )  mod  N )  =  ( F `  z ) )
332326, 319, 328, 330, 331syl22anc 1183 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  z )  mod  N
)  =  ( F `
 z ) )
333325, 332eqeq12d 2297 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( ( F `
 y )  mod 
N )  =  ( ( F `  z
)  mod  N )  <->  ( F `  y )  =  ( F `  z ) ) )
334 moddvds 12538 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  NN  /\  ( F `  y )  e.  ZZ  /\  ( F `  z )  e.  ZZ )  ->  (
( ( F `  y )  mod  N
)  =  ( ( F `  z )  mod  N )  <->  N  ||  (
( F `  y
)  -  ( F `
 z ) ) ) )
335273, 280, 287, 334syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( ( F `
 y )  mod 
N )  =  ( ( F `  z
)  mod  N )  <->  N 
||  ( ( F `
 y )  -  ( F `  z ) ) ) )
336 f1of1 5471 . . . . . . . . . . . . . . . . . . 19  |-  ( F : T -1-1-onto-> S  ->  F : T -1-1-> S )
33760, 336syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : T -1-1-> S
)
338 f1fveq 5786 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : T -1-1-> S  /\  ( y  e.  T  /\  z  e.  T
) )  ->  (
( F `  y
)  =  ( F `
 z )  <->  y  =  z ) )
339337, 338sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  y )  =  ( F `  z )  <-> 
y  =  z ) )
340333, 335, 3393bitr3d 274 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  ||  (
( F `  y
)  -  ( F `
 z ) )  <-> 
y  =  z ) )
341317, 340sylibd 205 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( N  ||  ( A  x.  (
( F `  y
)  -  ( F `
 z ) ) )  /\  ( N  gcd  A )  =  1 )  ->  y  =  z ) )
342313, 341mpan2d 655 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  ||  ( A  x.  ( ( F `  y )  -  ( F `  z ) ) )  ->  y  =  z ) )
343308, 342sylbid 206 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( G `  y )  =  ( G `  z )  ->  y  =  z ) )
344343ralrimivva 2635 . . . . . . . . . . . 12  |-  ( ph  ->  A. y  e.  T  A. z  e.  T  ( ( G `  y )  =  ( G `  z )  ->  y  =  z ) )
345 dff13 5783 . . . . . . . . . . . 12  |-  ( G : T -1-1-> S  <->  ( G : T --> S  /\  A. y  e.  T  A. z  e.  T  (
( G `  y
)  =  ( G `
 z )  -> 
y  =  z ) ) )
346164, 344, 345sylanbrc 645 . . . . . . . . . . 11  |-  ( ph  ->  G : T -1-1-> S
)
347 ovex 5883 . . . . . . . . . . . . . . 15  |-  ( 1 ... ( phi `  N ) )  e. 
_V
34867, 347eqeltri 2353 . . . . . . . . . . . . . 14  |-  T  e. 
_V
349348f1oen 6882 . . . . . . . . . . . . 13  |-  ( F : T -1-1-onto-> S  ->  T  ~~  S )
35060, 349syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  T  ~~  S )
351 fzofi 11036 . . . . . . . . . . . . 13  |-  ( 0..^ N )  e.  Fin
352 ssfi 7083 . . . . . . . . . . . . 13  |-  ( ( ( 0..^ N )  e.  Fin  /\  S  C_  ( 0..^ N ) )  ->  S  e.  Fin )
353351, 163, 352mp2an 653 . . . . . . . . . . . 12  |-  S  e. 
Fin
354 f1finf1o 7086 . . . . . . . . . . . 12  |-  ( ( T  ~~  S  /\  S  e.  Fin )  ->  ( G : T -1-1-> S  <-> 
G : T -1-1-onto-> S ) )
355350, 353, 354sylancl 643 . . . . . . . . . . 11  |-  ( ph  ->  ( G : T -1-1-> S  <-> 
G : T -1-1-onto-> S ) )
356346, 355mpbid 201 . . . . . . . . . 10  |-  ( ph  ->  G : T -1-1-onto-> S )
357 f1oco 5496 . . . . . . . . . 10  |-  ( ( `' F : S -1-1-onto-> T  /\  G : T -1-1-onto-> S )  ->  ( `' F  o.  G
) : T -1-1-onto-> T )
358272, 356, 357syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( `' F  o.  G ) : T -1-1-onto-> T
)
359 f1oeq23 5466 . . . . . . . . . 10  |-  ( ( 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 ) ) ) )
36067, 67, 359mp2an 653 . . . . . . . . 9  |-  ( ( `' F  o.  G
) : T -1-1-onto-> T  <->  ( `' F  o.  G ) : ( 1 ... ( phi `  N
) ) -1-1-onto-> ( 1 ... ( phi `  N ) ) )
361358, 360sylib 188 . . . . . . . 8  |-  ( ph  ->  ( `' F  o.  G ) : ( 1 ... ( phi `  N ) ) -1-1-onto-> ( 1 ... ( phi `  N ) ) )
362259zcnd 10118 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( phi `  N ) ) )  ->  ( F `  x )  e.  CC )
36367eleq2i 2347 . . . . . . . . 9  |-  ( w  e.  T  <->  w  e.  ( 1 ... ( phi `  N ) ) )
364 fvco3 5596 . . . . . . . . . . . 12  |-  ( ( G : T --> S  /\  w  e.  T )  ->  ( ( `' F  o.  G ) `  w
)  =  ( `' F `  ( G `
 w ) ) )
365164, 364sylan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  T )  ->  (
( `' F  o.  G ) `  w
)  =  ( `' F `  ( G `
 w ) ) )
366365fveq2d 5529 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  T )  ->  ( F `  ( ( `' F  o.  G
) `  w )
)  =  ( F `
 ( `' F `  ( G `  w
) ) ) )
36760adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  T )  ->  F : T -1-1-onto-> S )
368 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( ( G : T --> S  /\  w  e.  T )  ->  ( G `  w
)  e.  S )
369164, 368sylan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  T )  ->  ( G `  w )  e.  S )
370 f1ocnvfv2 5793 . . . . . . . . . . 11  |-  ( ( F : T -1-1-onto-> S  /\  ( G `  w )  e.  S )  -> 
( F `  ( `' F `  ( G `
 w ) ) )  =  ( G `
 w ) )
371367, 369, 370syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  T )  ->  ( F `  ( `' F `  ( G `  w ) ) )  =  ( G `  w ) )
372366, 371eqtr2d 2316 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  T )  ->  ( G `  w )  =  ( F `  ( ( `' F  o.  G ) `  w
) ) )
373363, 372sylan2br 462 . . . . . . . 8  |-  ( (
ph  /\  w  e.  ( 1 ... ( phi `  N ) ) )  ->  ( G `  w )  =  ( F `  ( ( `' F  o.  G
) `  w )
) )
374264, 266, 268, 64, 270, 361, 362, 373seqf1o 11087 . . . . . . 7  |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `
 ( phi `  N ) )  =  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) ) )
375374, 261eqeltrd 2357 . . . . . 6  |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `
 ( phi `  N ) )  e.  ZZ )
376 moddvds 12538 . . . . . 6  |-  ( ( 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 ) ) ) ) )
3772, 262, 375, 376syl3anc 1182 . . . . 5  |-  ( ph  ->  ( ( ( (