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

Theorem eulerthlem2 13171
Description: Lemma for eulerth 13172. (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 969 . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
32phicld 13161 . . . . . . . . 9  |-  ( ph  ->  ( phi `  N
)  e.  NN )
43nnred 10015 . . . . . . . 8  |-  ( ph  ->  ( phi `  N
)  e.  RR )
54leidd 9593 . . . . . . 7  |-  ( ph  ->  ( phi `  N
)  <_  ( phi `  N ) )
63adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( phi `  N )  <_  ( phi `  N ) )  ->  ( phi `  N )  e.  NN )
7 breq1 4215 . . . . . . . . . . 11  |-  ( x  =  1  ->  (
x  <_  ( phi `  N )  <->  1  <_  ( phi `  N ) ) )
87anbi2d 685 . . . . . . . . . 10  |-  ( x  =  1  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  1  <_  ( phi `  N ) ) ) )
9 oveq2 6089 . . . . . . . . . . . . . 14  |-  ( x  =  1  ->  ( A ^ x )  =  ( A ^ 1 ) )
10 fveq2 5728 . . . . . . . . . . . . . 14  |-  ( x  =  1  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  1
) )
119, 10oveq12d 6099 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ 1 )  x.  (  seq  1 (  x.  ,  F ) `  1
) ) )
1211oveq1d 6096 . . . . . . . . . . . 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 5728 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  1
) )
1413oveq1d 6096 . . . . . . . . . . . 12  |-  ( x  =  1  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 1 )  mod 
N ) )
1512, 14eqeq12d 2450 . . . . . . . . . . 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 6097 . . . . . . . . . . . 12  |-  ( x  =  1  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  1 )
) )
1716eqeq1d 2444 . . . . . . . . . . 11  |-  ( x  =  1  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  1
) )  =  1 ) )
1815, 17anbi12d 692 . . . . . . . . . 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 312 . . . . . . . . 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 4215 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
x  <_  ( phi `  N )  <->  z  <_  ( phi `  N ) ) )
2120anbi2d 685 . . . . . . . . . 10  |-  ( x  =  z  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  z  <_  ( phi `  N ) ) ) )
22 oveq2 6089 . . . . . . . . . . . . . 14  |-  ( x  =  z  ->  ( A ^ x )  =  ( A ^ z
) )
23 fveq2 5728 . . . . . . . . . . . . . 14  |-  ( x  =  z  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  z
) )
2422, 23oveq12d 6099 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ z
)  x.  (  seq  1 (  x.  ,  F ) `  z
) ) )
2524oveq1d 6096 . . . . . . . . . . . 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 5728 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  z
) )
2726oveq1d 6096 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 z )  mod 
N ) )
2825, 27eqeq12d 2450 . . . . . . . . . . 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 6097 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  z )
) )
3029eqeq1d 2444 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  z
) )  =  1 ) )
3128, 30anbi12d 692 . . . . . . . . . 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 312 . . . . . . . . 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 4215 . . . . . . . . . . 11  |-  ( x  =  ( z  +  1 )  ->  (
x  <_  ( phi `  N )  <->  ( z  +  1 )  <_ 
( phi `  N
) ) )
3433anbi2d 685 . . . . . . . . . 10  |-  ( x  =  ( z  +  1 )  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  ( z  +  1 )  <_  ( phi `  N ) ) ) )
35 oveq2 6089 . . . . . . . . . . . . . 14  |-  ( x  =  ( z  +  1 )  ->  ( A ^ x )  =  ( A ^ (
z  +  1 ) ) )
36 fveq2 5728 . . . . . . . . . . . . . 14  |-  ( x  =  ( z  +  1 )  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) ) )
3735, 36oveq12d 6099 . . . . . . . . . . . . 13  |-  ( x  =  ( z  +  1 )  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ (
z  +  1 ) )  x.  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) ) ) )
3837oveq1d 6096 . . . . . . . . . . . 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 5728 . . . . . . . . . . . . 13  |-  ( x  =  ( z  +  1 )  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  (
z  +  1 ) ) )
4039oveq1d 6096 . . . . . . . . . . . 12  |-  ( x  =  ( z  +  1 )  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 ( z  +  1 ) )  mod 
N ) )
4138, 40eqeq12d 2450 . . . . . . . . . . 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 6097 . . . . . . . . . . . 12  |-  ( x  =  ( z  +  1 )  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  ( z  +  1 ) ) ) )
4342eqeq1d 2444 . . . . . . . . . . 11  |-  ( x  =  ( z  +  1 )  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) ) )  =  1 ) )
4441, 43anbi12d 692 . . . . . . . . . 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 312 . . . . . . . . 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 4215 . . . . . . . . . . 11  |-  ( x  =  ( phi `  N )  ->  (
x  <_  ( phi `  N )  <->  ( phi `  N )  <_  ( phi `  N ) ) )
4746anbi2d 685 . . . . . . . . . 10  |-  ( x  =  ( phi `  N )  ->  (
( ph  /\  x  <_  ( phi `  N
) )  <->  ( ph  /\  ( phi `  N
)  <_  ( phi `  N ) ) ) )
48 oveq2 6089 . . . . . . . . . . . . . 14  |-  ( x  =  ( phi `  N )  ->  ( A ^ x )  =  ( A ^ ( phi `  N ) ) )
49 fveq2 5728 . . . . . . . . . . . . . 14  |-  ( x  =  ( phi `  N )  ->  (  seq  1 (  x.  ,  F ) `  x
)  =  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )
5048, 49oveq12d 6099 . . . . . . . . . . . . 13  |-  ( x  =  ( phi `  N )  ->  (
( A ^ x
)  x.  (  seq  1 (  x.  ,  F ) `  x
) )  =  ( ( A ^ ( phi `  N ) )  x.  (  seq  1
(  x.  ,  F
) `  ( phi `  N ) ) ) )
5150oveq1d 6096 . . . . . . . . . . . 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 5728 . . . . . . . . . . . . 13  |-  ( x  =  ( phi `  N )  ->  (  seq  1 (  x.  ,  G ) `  x
)  =  (  seq  1 (  x.  ,  G ) `  ( phi `  N ) ) )
5352oveq1d 6096 . . . . . . . . . . . 12  |-  ( x  =  ( phi `  N )  ->  (
(  seq  1 (  x.  ,  G ) `
 x )  mod 
N )  =  ( (  seq  1 (  x.  ,  G ) `
 ( phi `  N ) )  mod 
N ) )
5451, 53eqeq12d 2450 . . . . . . . . . . 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 6097 . . . . . . . . . . . 12  |-  ( x  =  ( phi `  N )  ->  ( N  gcd  (  seq  1
(  x.  ,  F
) `  x )
)  =  ( N  gcd  (  seq  1
(  x.  ,  F
) `  ( phi `  N ) ) ) )
5655eqeq1d 2444 . . . . . . . . . . 11  |-  ( x  =  ( phi `  N )  ->  (
( N  gcd  (  seq  1 (  x.  ,  F ) `  x
) )  =  1  <-> 
( N  gcd  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )  =  1 ) )
5754, 56anbi12d 692 . . . . . . . . . 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 312 . . . . . . . . 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 970 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  ZZ )
60 eulerth.4 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F : T -1-1-onto-> S )
61 f1of 5674 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : T -1-1-onto-> S  ->  F : T
--> S )
6260, 61syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : T --> S )
63 nnuz 10521 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN  =  ( ZZ>= `  1 )
643, 63syl6eleq 2526 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( phi `  N
)  e.  ( ZZ>= ` 
1 ) )
65 eluzfz1 11064 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( phi `  N )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( phi `  N ) ) )
6664, 65syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  1  e.  ( 1 ... ( phi `  N ) ) )
67 eulerth.3 . . . . . . . . . . . . . . . . . . . 20  |-  T  =  ( 1 ... ( phi `  N ) )
6866, 67syl6eleqr 2527 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  1  e.  T )
6962, 68ffvelrnd 5871 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F `  1
)  e.  S )
70 oveq1 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( F ` 
1 )  ->  (
y  gcd  N )  =  ( ( F `
 1 )  gcd 
N ) )
7170eqeq1d 2444 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( F ` 
1 )  ->  (
( y  gcd  N
)  =  1  <->  (
( F `  1
)  gcd  N )  =  1 ) )
72 eulerth.2 . . . . . . . . . . . . . . . . . . 19  |-  S  =  { y  e.  ( 0..^ N )  |  ( y  gcd  N
)  =  1 }
7371, 72elrab2 3094 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  1 )  e.  S  <->  ( ( F `  1 )  e.  ( 0..^ N )  /\  ( ( F `
 1 )  gcd 
N )  =  1 ) )
7469, 73sylib 189 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( F ` 
1 )  e.  ( 0..^ N )  /\  ( ( F ` 
1 )  gcd  N
)  =  1 ) )
7574simpld 446 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F `  1
)  e.  ( 0..^ N ) )
76 elfzoelz 11140 . . . . . . . . . . . . . . . 16  |-  ( ( F `  1 )  e.  ( 0..^ N )  ->  ( F `  1 )  e.  ZZ )
7775, 76syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  1
)  e.  ZZ )
7859, 77zmulcld 10381 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  x.  ( F `  1 )
)  e.  ZZ )
7978zred 10375 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  x.  ( F `  1 )
)  e.  RR )
802nnrpd 10647 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  RR+ )
81 modabs2 11275 . . . . . . . . . . . . 13  |-  ( ( ( A  x.  ( F `  1 )
)  e.  RR  /\  N  e.  RR+ )  -> 
( ( ( A  x.  ( F ` 
1 ) )  mod 
N )  mod  N
)  =  ( ( A  x.  ( F `
 1 ) )  mod  N ) )
8279, 80, 81syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  x.  ( F ` 
1 ) )  mod 
N )  mod  N
)  =  ( ( A  x.  ( F `
 1 ) )  mod  N ) )
83 1z 10311 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
84 fveq2 5728 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  1  ->  ( F `  x )  =  ( F ` 
1 ) )
8584oveq2d 6097 . . . . . . . . . . . . . . . . 17  |-  ( x  =  1  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  1 )
) )
8685oveq1d 6096 . . . . . . . . . . . . . . . 16  |-  ( x  =  1  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F ` 
1 ) )  mod 
N ) )
87 eulerth.5 . . . . . . . . . . . . . . . 16  |-  G  =  ( x  e.  T  |->  ( ( A  x.  ( F `  x ) )  mod  N ) )
88 ovex 6106 . . . . . . . . . . . . . . . 16  |-  ( ( A  x.  ( F `
 1 ) )  mod  N )  e. 
_V
8986, 87, 88fvmpt 5806 . . . . . . . . . . . . . . 15  |-  ( 1  e.  T  ->  ( G `  1 )  =  ( ( A  x.  ( F ` 
1 ) )  mod 
N ) )
9068, 89syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  1
)  =  ( ( A  x.  ( F `
 1 ) )  mod  N ) )
9183, 90seq1i 11337 . . . . . . . . . . . . 13  |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `
 1 )  =  ( ( A  x.  ( F `  1 ) )  mod  N ) )
9291oveq1d 6096 . . . . . . . . . . . 12  |-  ( ph  ->  ( (  seq  1
(  x.  ,  G
) `  1 )  mod  N )  =  ( ( ( A  x.  ( F `  1 ) )  mod  N )  mod  N ) )
9359zcnd 10376 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  CC )
9493exp1d 11518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A ^ 1 )  =  A )
95 seq1 11336 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  ->  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 ) )
9683, 95ax-mp 8 . . . . . . . . . . . . . . 15  |-  (  seq  1 (  x.  ,  F ) `  1
)  =  ( F `
 1 )
9796a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  (  seq  1 (  x.  ,  F ) `
 1 )  =  ( F `  1
) )
9894, 97oveq12d 6099 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A ^
1 )  x.  (  seq  1 (  x.  ,  F ) `  1
) )  =  ( A  x.  ( F `
 1 ) ) )
9998oveq1d 6096 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A ^ 1 )  x.  (  seq  1 (  x.  ,  F ) `
 1 ) )  mod  N )  =  ( ( A  x.  ( F `  1 ) )  mod  N ) )
10082, 92, 993eqtr4rd 2479 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( A ^ 1 )  x.  (  seq  1 (  x.  ,  F ) `
 1 ) )  mod  N )  =  ( (  seq  1
(  x.  ,  G
) `  1 )  mod  N ) )
10196oveq2i 6092 . . . . . . . . . . . 12  |-  ( N  gcd  (  seq  1
(  x.  ,  F
) `  1 )
)  =  ( N  gcd  ( F ` 
1 ) )
1022nnzd 10374 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ZZ )
103 gcdcom 13020 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ZZ  /\  ( F `  1 )  e.  ZZ )  -> 
( N  gcd  ( F `  1 )
)  =  ( ( F `  1 )  gcd  N ) )
104102, 77, 103syl2anc 643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  gcd  ( F `  1 )
)  =  ( ( F `  1 )  gcd  N ) )
10574simprd 450 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( F ` 
1 )  gcd  N
)  =  1 )
106104, 105eqtrd 2468 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  gcd  ( F `  1 )
)  =  1 )
107101, 106syl5eq 2480 . . . . . . . . . . 11  |-  ( ph  ->  ( N  gcd  (  seq  1 (  x.  ,  F ) `  1
) )  =  1 )
108100, 107jca 519 . . . . . . . . . 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 ) )
109108adantr 452 . . . . . . . . 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 ) )
110 nnre 10007 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN  ->  z  e.  RR )
111110adantr 452 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  ph )  ->  z  e.  RR )
112111lep1d 9942 . . . . . . . . . . . . 13  |-  ( ( z  e.  NN  /\  ph )  ->  z  <_  ( z  +  1 ) )
113 peano2re 9239 . . . . . . . . . . . . . . 15  |-  ( z  e.  RR  ->  (
z  +  1 )  e.  RR )
114111, 113syl 16 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  ph )  ->  ( z  +  1 )  e.  RR )
1154adantl 453 . . . . . . . . . . . . . 14  |-  ( ( z  e.  NN  /\  ph )  ->  ( phi `  N )  e.  RR )
116 letr 9167 . . . . . . . . . . . . . 14  |-  ( ( z  e.  RR  /\  ( z  +  1 )  e.  RR  /\  ( phi `  N )  e.  RR )  -> 
( ( z  <_ 
( z  +  1 )  /\  ( z  +  1 )  <_ 
( phi `  N
) )  ->  z  <_  ( phi `  N
) ) )
117111, 114, 115, 116syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( z  e.  NN  /\  ph )  ->  ( (
z  <_  ( z  +  1 )  /\  ( z  +  1 )  <_  ( phi `  N ) )  -> 
z  <_  ( phi `  N ) ) )
118112, 117mpand 657 . . . . . . . . . . . 12  |-  ( ( z  e.  NN  /\  ph )  ->  ( (
z  +  1 )  <_  ( phi `  N )  ->  z  <_  ( phi `  N
) ) )
119118imdistanda 675 . . . . . . . . . . 11  |-  ( z  e.  NN  ->  (
( ph  /\  (
z  +  1 )  <_  ( phi `  N ) )  -> 
( ph  /\  z  <_  ( phi `  N
) ) ) )
120119imim1d 71 . . . . . . . . . 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 ) ) ) )
12159adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  A  e.  ZZ )
122 nnnn0 10228 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  NN  ->  z  e.  NN0 )
123122ad2antrl 709 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  NN0 )
124 zexpcl 11396 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ZZ  /\  z  e.  NN0 )  -> 
( A ^ z
)  e.  ZZ )
125121, 123, 124syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A ^ z
)  e.  ZZ )
126 simprl 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  NN )
127126, 63syl6eleq 2526 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  ( ZZ>= ` 
1 ) )
128110ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  RR )
129128, 113syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  RR )
1304adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( phi `  N
)  e.  RR )
131128lep1d 9942 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  <_  ( z  +  1 ) )
132 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  <_  ( phi `  N ) )
133128, 129, 130, 131, 132letrd 9227 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  <_  ( phi `  N ) )
134 nnz 10303 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  NN  ->  z  e.  ZZ )
135134ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
z  e.  ZZ )
1363nnzd 10374 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( phi `  N
)  e.  ZZ )
137136adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( phi `  N
)  e.  ZZ )
138 eluz 10499 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( z  e.  ZZ  /\  ( phi `  N )  e.  ZZ )  -> 
( ( phi `  N )  e.  (
ZZ>= `  z )  <->  z  <_  ( phi `  N ) ) )
139135, 137, 138syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( phi `  N )  e.  (
ZZ>= `  z )  <->  z  <_  ( phi `  N ) ) )
140133, 139mpbird 224 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( phi `  N
)  e.  ( ZZ>= `  z ) )
141 fzss2 11092 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( phi `  N )  e.  ( ZZ>= `  z
)  ->  ( 1 ... z )  C_  ( 1 ... ( phi `  N ) ) )
142140, 141syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( 1 ... z
)  C_  ( 1 ... ( phi `  N ) ) )
143142, 67syl6sseqr 3395 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( 1 ... z
)  C_  T )
144143sselda 3348 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  ( 1 ... z ) )  ->  x  e.  T )
14562ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  T )  ->  ( F `  x )  e.  S )
146 oveq1 6088 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( F `  x )  ->  (
y  gcd  N )  =  ( ( F `
 x )  gcd 
N ) )
147146eqeq1d 2444 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( F `  x )  ->  (
( y  gcd  N
)  =  1  <->  (
( F `  x
)  gcd  N )  =  1 ) )
148147, 72elrab2 3094 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  x )  e.  S  <->  ( ( F `  x )  e.  ( 0..^ N )  /\  ( ( F `
 x )  gcd 
N )  =  1 ) )
149145, 148sylib 189 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  T )  ->  (
( F `  x
)  e.  ( 0..^ N )  /\  (
( F `  x
)  gcd  N )  =  1 ) )
150149simpld 446 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  T )  ->  ( F `  x )  e.  ( 0..^ N ) )
151 elfzoelz 11140 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  x )  e.  ( 0..^ N )  ->  ( F `  x )  e.  ZZ )
152150, 151syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  T )  ->  ( F `  x )  e.  ZZ )
153152adantlr 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  T
)  ->  ( F `  x )  e.  ZZ )
154144, 153syldan 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  ( 1 ... z ) )  ->  ( F `  x )  e.  ZZ )
155 zmulcl 10324 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ZZ  /\  y  e.  ZZ )  ->  ( x  x.  y
)  e.  ZZ )
156155adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  ( x  e.  ZZ  /\  y  e.  ZZ ) )  -> 
( x  x.  y
)  e.  ZZ )
157127, 154, 156seqcl 11343 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  F ) `
 z )  e.  ZZ )
158125, 157zmulcld 10381 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A ^
z )  x.  (  seq  1 (  x.  ,  F ) `  z
) )  e.  ZZ )
159158zred 10375 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A ^
z )  x.  (  seq  1 (  x.  ,  F ) `  z
) )  e.  RR )
160 ssrab2 3428 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }  C_  (
0..^ N )
16172, 160eqsstri 3378 . . . . . . . . . . . . . . . . . . . . . 22  |-  S  C_  ( 0..^ N )
1621, 72, 67, 60, 87eulerthlem1 13170 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  G : T --> S )
163162ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  T )  ->  ( G `  x )  e.  S )
164161, 163sseldi 3346 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  T )  ->  ( G `  x )  e.  ( 0..^ N ) )
165 elfzoelz 11140 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  x )  e.  ( 0..^ N )  ->  ( G `  x )  e.  ZZ )
166164, 165syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  T )  ->  ( G `  x )  e.  ZZ )
167166adantlr 696 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  T
)  ->  ( G `  x )  e.  ZZ )
168144, 167syldan 457 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  e.  NN  /\  ( z  +  1 )  <_  ( phi `  N ) ) )  /\  x  e.  ( 1 ... z ) )  ->  ( G `  x )  e.  ZZ )
169127, 168, 156seqcl 11343 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 z )  e.  ZZ )
170169zred 10375 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 z )  e.  RR )
17162adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  F : T --> S )
172 peano2nn 10012 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  NN  ->  (
z  +  1 )  e.  NN )
173172ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  NN )
174173nnge1d 10042 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
1  <_  ( z  +  1 ) )
175173nnzd 10374 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  ZZ )
176 elfz 11049 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
17783, 176mp3an2 1267 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( z  +  1 )  e.  ZZ  /\  ( phi `  N )  e.  ZZ )  -> 
( ( z  +  1 )  e.  ( 1 ... ( phi `  N ) )  <->  ( 1  <_  ( z  +  1 )  /\  (
z  +  1 )  <_  ( phi `  N ) ) ) )
178175, 137, 177syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( z  +  1 )  e.  ( 1 ... ( phi `  N ) )  <->  ( 1  <_  ( z  +  1 )  /\  (
z  +  1 )  <_  ( phi `  N ) ) ) )
179174, 132, 178mpbir2and 889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  ( 1 ... ( phi `  N ) ) )
180179, 67syl6eleqr 2527 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( z  +  1 )  e.  T )
181171, 180ffvelrnd 5871 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  S )
182 oveq1 6088 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( F `  ( z  +  1 ) )  ->  (
y  gcd  N )  =  ( ( F `
 ( z  +  1 ) )  gcd 
N ) )
183182eqeq1d 2444 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( F `  ( z  +  1 ) )  ->  (
( y  gcd  N
)  =  1  <->  (
( F `  (
z  +  1 ) )  gcd  N )  =  1 ) )
184183, 72elrab2 3094 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  ( z  +  1 ) )  e.  S  <->  ( ( F `  ( z  +  1 ) )  e.  ( 0..^ N )  /\  ( ( F `  ( z  +  1 ) )  gcd  N )  =  1 ) )
185181, 184sylib 189 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( F `  ( z  +  1 ) )  e.  ( 0..^ N )  /\  ( ( F `  ( z  +  1 ) )  gcd  N
)  =  1 ) )
186185simpld 446 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  ( 0..^ N ) )
187 elfzoelz 11140 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  ( z  +  1 ) )  e.  ( 0..^ N )  ->  ( F `  ( z  +  1 ) )  e.  ZZ )
188186, 187syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  ZZ )
189121, 188zmulcld 10381 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A  x.  ( F `  ( z  +  1 ) ) )  e.  ZZ )
19080adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  N  e.  RR+ )
191 modmul1 11279 . . . . . . . . . . . . . . . . 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
) )
1921913expia 1155 . . . . . . . . . . . . . . . 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
) ) )
193159, 170, 189, 190, 192syl22anc 1185 . . . . . . . . . . . . . . 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 ) ) )
194125zcnd 10376 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A ^ z
)  e.  CC )
195157zcnd 10376 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  F ) `
 z )  e.  CC )
19693adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  A  e.  CC )
197188zcnd 10376 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( F `  (
z  +  1 ) )  e.  CC )
198194, 195, 196, 197mul4d 9278 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
199196, 123expp1d 11524 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A ^ (
z  +  1 ) )  =  ( ( A ^ z )  x.  A ) )
200 seqp1 11338 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ZZ>= `  1
)  ->  (  seq  1 (  x.  ,  F ) `  (
z  +  1 ) )  =  ( (  seq  1 (  x.  ,  F ) `  z )  x.  ( F `  ( z  +  1 ) ) ) )
201127, 200syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  F ) `
 ( z  +  1 ) )  =  ( (  seq  1
(  x.  ,  F
) `  z )  x.  ( F `  (
z  +  1 ) ) ) )
202199, 201oveq12d 6099 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
203198, 202eqtr4d 2471 . . . . . . . . . . . . . . . . 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 ) ) ) )
204203oveq1d 6096 . . . . . . . . . . . . . . . 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 ) )
205189zred 10375 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A  x.  ( F `  ( z  +  1 ) ) )  e.  RR )
206205, 190modcld 11254 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A  x.  ( F `  ( z  +  1 ) ) )  mod  N )  e.  RR )
207 modabs2 11275 . . . . . . . . . . . . . . . . . . 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 ) )
208205, 190, 207syl2anc 643 . . . . . . . . . . . . . . . . . 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 ) )
209 modmul1 11279 . . . . . . . . . . . . . . . . . 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 )
)
210206, 205, 169, 190, 208, 209syl221anc 1195 . . . . . . . . . . . . . . . . 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 ) )
211 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( z  +  1 )  ->  ( F `  x )  =  ( F `  ( z  +  1 ) ) )
212211oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( z  +  1 )  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  ( z  +  1 ) ) ) )
213212oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( z  +  1 )  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F `  ( z  +  1 ) ) )  mod 
N ) )
214 ovex 6106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  x.  ( F `
 ( z  +  1 ) ) )  mod  N )  e. 
_V
215213, 87, 214fvmpt 5806 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  +  1 )  e.  T  ->  ( G `  ( z  +  1 ) )  =  ( ( A  x.  ( F `  ( z  +  1 ) ) )  mod 
N ) )
216180, 215syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( G `  (
z  +  1 ) )  =  ( ( A  x.  ( F `
 ( z  +  1 ) ) )  mod  N ) )
217216oveq2d 6097 . . . . . . . . . . . . . . . . . . 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 ) ) )
218 seqp1 11338 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ZZ>= `  1
)  ->  (  seq  1 (  x.  ,  G ) `  (
z  +  1 ) )  =  ( (  seq  1 (  x.  ,  G ) `  z )  x.  ( G `  ( z  +  1 ) ) ) )
219127, 218syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 ( z  +  1 ) )  =  ( (  seq  1
(  x.  ,  G
) `  z )  x.  ( G `  (
z  +  1 ) ) ) )
220206recnd 9114 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( A  x.  ( F `  ( z  +  1 ) ) )  mod  N )  e.  CC )
221169zcnd 10376 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
(  seq  1 (  x.  ,  G ) `
 z )  e.  CC )
222220, 221mulcomd 9109 . . . . . . . . . . . . . . . . . . 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 ) ) )
223217, 219, 2223eqtr4d 2478 . . . . . . . . . . . . . . . . . 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
) ) )
224223oveq1d 6096 . . . . . . . . . . . . . . . . 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 ) )
225189zcnd 10376 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( A  x.  ( F `  ( z  +  1 ) ) )  e.  CC )
226221, 225mulcomd 9109 . . . . . . . . . . . . . . . . . 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
) ) )
227226oveq1d 6096 . . . . . . . . . . . . . . . . 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 ) )
228210, 224, 2273eqtr4rd 2479 . . . . . . . . . . . . . . . 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 ) )
229204, 228eqeq12d 2450 . . . . . . . . . . . . . . 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
) ) )
230193, 229sylibd 206 . . . . . . . . . . . . . 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 ) ) )
231102adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  ->  N  e.  ZZ )
232 gcdcom 13020 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ZZ  /\  ( F `  ( z  +  1 ) )  e.  ZZ )  -> 
( N  gcd  ( F `  ( z  +  1 ) ) )  =  ( ( F `  ( z  +  1 ) )  gcd  N ) )
233231, 188, 232syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( N  gcd  ( F `  ( z  +  1 ) ) )  =  ( ( F `  ( z  +  1 ) )  gcd  N ) )
234185simprd 450 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( ( F `  ( z  +  1 ) )  gcd  N
)  =  1 )
235233, 234eqtrd 2468 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  NN  /\  ( z  +  1 )  <_ 
( phi `  N
) ) )  -> 
( N  gcd  ( F `  ( z  +  1 ) ) )  =  1 )
236 rpmul 13123 . . . . . . . . . . . . . . . . 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 ) )
237231, 157, 188, 236syl3anc 1184 . . . . . . . . . . . . . . . 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 ) )
238235, 237mpan2d 656 . . . . . . . . . . . . . . 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 ) )
239201oveq2d 6097 . . . . . . . . . . . . . . . 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 ) ) ) ) )
240239eqeq1d 2444 . . . . . . . . . . . . . . 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 ) )
241238, 240sylibrd 226 . . . . . . . . . . . . . 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 ) )
242230, 241anim12d 547 . . . . . . . . . . . . 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 ) ) )
243242an12s 777 . . . . . . . . . . . 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 ) ) )
244243ex 424 . . . . . . . . . . 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 ) ) ) )
245244a2d 24 . . . . . . . . . 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 ) ) ) )
246120, 245syld 42 . . . . . . . . 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 ) ) ) )
24719, 32, 45, 58, 109, 246nnind 10018 . . . . . . . 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 ) ) )
2486, 247mpcom 34 . . . . . . 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 ) )
2495, 248mpdan 650 . . . . . 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 ) )
250249simpld 446 . . . . 5  |-  ( ph  ->  ( ( ( A ^ ( phi `  N ) )  x.  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) ) )  mod  N )  =  ( (  seq  1
(  x.  ,  G
) `  ( phi `  N ) )  mod 
N ) )
2513nnnn0d 10274 . . . . . . . 8  |-  ( ph  ->  ( phi `  N
)  e.  NN0 )
252 zexpcl 11396 . . . . . . . 8  |-  ( ( A  e.  ZZ  /\  ( phi `  N )  e.  NN0 )  -> 
( A ^ ( phi `  N ) )  e.  ZZ )
25359, 251, 252syl2anc 643 . . . . . . 7  |-  ( ph  ->  ( A ^ ( phi `  N ) )  e.  ZZ )
25467eleq2i 2500 . . . . . . . . 9  |-  ( x  e.  T  <->  x  e.  ( 1 ... ( phi `  N ) ) )
255254, 152sylan2br 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( phi `  N ) ) )  ->  ( F `  x )  e.  ZZ )
256155adantl 453 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ZZ  /\  y  e.  ZZ ) )  -> 
( x  x.  y
)  e.  ZZ )
25764, 255, 256seqcl 11343 . . . . . . 7  |-  ( ph  ->  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) )  e.  ZZ )
258253, 257zmulcld 10381 . . . . . 6  |-  ( ph  ->  ( ( A ^
( phi `  N
) )  x.  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )  e.  ZZ )
259 mulcl 9074 . . . . . . . . 9  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
260259adantl 453 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  e.  CC )
261 mulcom 9076 . . . . . . . . 9  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  =  ( y  x.  x ) )
262261adantl 453 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  =  ( y  x.  x ) )
263 mulass 9078 . . . . . . . . 9  |-  ( ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC )  ->  (
( x  x.  y
)  x.  z )  =  ( x  x.  ( y  x.  z
) ) )
264263adantl 453 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC ) )  -> 
( ( x  x.  y )  x.  z
)  =  ( x  x.  ( y  x.  z ) ) )
265 ssid 3367 . . . . . . . . 9  |-  CC  C_  CC
266265a1i 11 . . . . . . . 8  |-  ( ph  ->  CC  C_  CC )
267 f1ocnv 5687 . . . . . . . . . . 11  |-  ( F : T -1-1-onto-> S  ->  `' F : S -1-1-onto-> T )
26860, 267syl 16 . . . . . . . . . 10  |-  ( ph  ->  `' F : S -1-1-onto-> T )
2692adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  N  e.  NN )
27059adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  A  e.  ZZ )
27162ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  T )  ->  ( F `  y )  e.  S )
272271adantrr 698 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  S )
273161, 272sseldi 3346 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  ( 0..^ N ) )
274 elfzoelz 11140 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  y )  e.  ( 0..^ N )  ->  ( F `  y )  e.  ZZ )
275273, 274syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  ZZ )
276270, 275zmulcld 10381 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( A  x.  ( F `  y )
)  e.  ZZ )
27762ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  T )  ->  ( F `  z )  e.  S )
278277adantrl 697 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  S )
279161, 278sseldi 3346 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  ( 0..^ N ) )
280 elfzoelz 11140 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  z )  e.  ( 0..^ N )  ->  ( F `  z )  e.  ZZ )
281279, 280syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  ZZ )
282270, 281zmulcld 10381 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( A  x.  ( F `  z )
)  e.  ZZ )
283 moddvds 12859 . . . . . . . . . . . . . . . 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 )
) ) ) )
284269, 276, 282, 283syl3anc 1184 . . . . . . . . . . . . . . 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 )
) ) ) )
285 fveq2 5728 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
286285oveq2d 6097 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  y )
) )
287286oveq1d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F `  y ) )  mod 
N ) )
288 ovex 6106 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  x.  ( F `
 y ) )  mod  N )  e. 
_V
289287, 87, 288fvmpt 5806 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  T  ->  ( G `  y )  =  ( ( A  x.  ( F `  y ) )  mod 
N ) )
290 fveq2 5728 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
291290oveq2d 6097 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  ( A  x.  ( F `  x ) )  =  ( A  x.  ( F `  z )
) )
292291oveq1d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  z  ->  (
( A  x.  ( F `  x )
)  mod  N )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) )
293 ovex 6106 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  x.  ( F `
 z ) )  mod  N )  e. 
_V
294292, 87, 293fvmpt 5806 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  T  ->  ( G `  z )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) )
295289, 294eqeqan12d 2451 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  T  /\  z  e.  T )  ->  ( ( G `  y )  =  ( G `  z )  <-> 
( ( A  x.  ( F `  y ) )  mod  N )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) ) )
296295adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( G `  y )  =  ( G `  z )  <-> 
( ( A  x.  ( F `  y ) )  mod  N )  =  ( ( A  x.  ( F `  z ) )  mod 
N ) ) )
29793adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  A  e.  CC )
298275zcnd 10376 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  CC )
299281zcnd 10376 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  CC )
300297, 298, 299subdid 9489 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( A  x.  (
( F `  y
)  -  ( F `
 z ) ) )  =  ( ( A  x.  ( F `
 y ) )  -  ( A  x.  ( F `  z ) ) ) )
301300breq2d 4224 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  ||  ( A  x.  ( ( F `  y )  -  ( F `  z ) ) )  <-> 
N  ||  ( ( A  x.  ( F `  y ) )  -  ( A  x.  ( F `  z )
) ) ) )
302284, 296, 3013bitr4d 277 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( G `  y )  =  ( G `  z )  <-> 
N  ||  ( A  x.  ( ( F `  y )  -  ( F `  z )
) ) ) )
303 gcdcom 13020 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ZZ  /\  A  e.  ZZ )  ->  ( N  gcd  A
)  =  ( A  gcd  N ) )
304102, 59, 303syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  gcd  A
)  =  ( A  gcd  N ) )
3051simp3d 971 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  gcd  N
)  =  1 )
306304, 305eqtrd 2468 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  gcd  A
)  =  1 )
307306adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  gcd  A
)  =  1 )
308102adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  N  e.  ZZ )
309275, 281zsubcld 10380 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  y )  -  ( F `  z )
)  e.  ZZ )
310 coprmdvds 13102 . . . . . . . . . . . . . . . . 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 )
) ) )
311308, 270, 309, 310syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( N  ||  ( A  x.  (
( F `  y
)  -  ( F `
 z ) ) )  /\  ( N  gcd  A )  =  1 )  ->  N  ||  ( ( F `  y )  -  ( F `  z )
) ) )
312275zred 10375 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  e.  RR )
31380adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  ->  N  e.  RR+ )
314 elfzole1 11147 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  y )  e.  ( 0..^ N )  ->  0  <_  ( F `  y ) )
315273, 314syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
0  <_  ( F `  y ) )
316 elfzolt2 11148 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  y )  e.  ( 0..^ N )  ->  ( F `  y )  <  N
)
317273, 316syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  y
)  <  N )
318 modid 11270 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  y )  e.  RR  /\  N  e.  RR+ )  /\  ( 0  <_  ( F `  y )  /\  ( F `  y
)  <  N )
)  ->  ( ( F `  y )  mod  N )  =  ( F `  y ) )
319312, 313, 315, 317, 318syl22anc 1185 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  y )  mod  N
)  =  ( F `
 y ) )
320281zred 10375 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  e.  RR )
321 elfzole1 11147 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z )  e.  ( 0..^ N )  ->  0  <_  ( F `  z ) )
322279, 321syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
0  <_  ( F `  z ) )
323 elfzolt2 11148 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z )  e.  ( 0..^ N )  ->  ( F `  z )  <  N
)
324279, 323syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( F `  z
)  <  N )
325 modid 11270 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  z )  e.  RR  /\  N  e.  RR+ )  /\  ( 0  <_  ( F `  z )  /\  ( F `  z
)  <  N )
)  ->  ( ( F `  z )  mod  N )  =  ( F `  z ) )
326320, 313, 322, 324, 325syl22anc 1185 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  z )  mod  N
)  =  ( F `
 z ) )
327319, 326eqeq12d 2450 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( ( F `
 y )  mod 
N )  =  ( ( F `  z
)  mod  N )  <->  ( F `  y )  =  ( F `  z ) ) )
328 moddvds 12859 . . . . . . . . . . . . . . . . . 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 ) ) ) )
329269, 275, 281, 328syl3anc 1184 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( ( F `
 y )  mod 
N )  =  ( ( F `  z
)  mod  N )  <->  N 
||  ( ( F `
 y )  -  ( F `  z ) ) ) )
330 f1of1 5673 . . . . . . . . . . . . . . . . . . 19  |-  ( F : T -1-1-onto-> S  ->  F : T -1-1-> S )
33160, 330syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : T -1-1-> S
)
332 f1fveq 6008 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : T -1-1-> S  /\  ( y  e.  T  /\  z  e.  T
) )  ->  (
( F `  y
)  =  ( F `
 z )  <->  y  =  z ) )
333331, 332sylan 458 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( F `  y )  =  ( F `  z )  <-> 
y  =  z ) )
334327, 329, 3333bitr3d 275 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  ||  (
( F `  y
)  -  ( F `
 z ) )  <-> 
y  =  z ) )
335311, 334sylibd 206 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( N  ||  ( A  x.  (
( F `  y
)  -  ( F `
 z ) ) )  /\  ( N  gcd  A )  =  1 )  ->  y  =  z ) )
336307, 335mpan2d 656 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( N  ||  ( A  x.  ( ( F `  y )  -  ( F `  z ) ) )  ->  y  =  z ) )
337302, 336sylbid 207 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  T  /\  z  e.  T ) )  -> 
( ( G `  y )  =  ( G `  z )  ->  y  =  z ) )
338337ralrimivva 2798 . . . . . . . . . . . 12  |-  ( ph  ->  A. y  e.  T  A. z  e.  T  ( ( G `  y )  =  ( G `  z )  ->  y  =  z ) )
339 dff13 6004 . . . . . . . . . . . 12  |-  ( G : T -1-1-> S  <->  ( G : T --> S  /\  A. y  e.  T  A. z  e.  T  (
( G `  y
)  =  ( G `
 z )  -> 
y  =  z ) ) )
340162, 338, 339sylanbrc 646 . . . . . . . . . . 11  |-  ( ph  ->  G : T -1-1-> S
)
341 ovex 6106 . . . . . . . . . . . . . . 15  |-  ( 1 ... ( phi `  N ) )  e. 
_V
34267, 341eqeltri 2506 . . . . . . . . . . . . . 14  |-  T  e. 
_V
343342f1oen 7128 . . . . . . . . . . . . 13  |-  ( F : T -1-1-onto-> S  ->  T  ~~  S )
34460, 343syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  T  ~~  S )
345 fzofi 11313 . . . . . . . . . . . . 13  |-  ( 0..^ N )  e.  Fin
346 ssfi 7329 . . . . . . . . . . . . 13  |-  ( ( ( 0..^ N )  e.  Fin  /\  S  C_  ( 0..^ N ) )  ->  S  e.  Fin )
347345, 161, 346mp2an 654 . . . . . . . . . . . 12  |-  S  e. 
Fin
348 f1finf1o 7335 . . . . . . . . . . . 12  |-  ( ( T  ~~  S  /\  S  e.  Fin )  ->  ( G : T -1-1-> S  <-> 
G : T -1-1-onto-> S ) )
349344, 347, 348sylancl 644 . . . . . . . . . . 11  |-  ( ph  ->  ( G : T -1-1-> S  <-> 
G : T -1-1-onto-> S ) )
350340, 349mpbid 202 . . . . . . . . . 10  |-  ( ph  ->  G : T -1-1-onto-> S )
351 f1oco 5698 . . . . . . . . . 10  |-  ( ( `' F : S -1-1-onto-> T  /\  G : T -1-1-onto-> S )  ->  ( `' F  o.  G
) : T -1-1-onto-> T )
352268, 350, 351syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( `' F  o.  G ) : T -1-1-onto-> T
)
353 f1oeq23 5668 . . . . . . . . . 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 ) ) ) )
35467, 67, 353mp2an 654 . . . . . . . . 9  |-  ( ( `' F  o.  G
) : T -1-1-onto-> T  <->  ( `' F  o.  G ) : ( 1 ... ( phi `  N
) ) -1-1-onto-> ( 1 ... ( phi `  N ) ) )
355352, 354sylib 189 . . . . . . . 8  |-  ( ph  ->  ( `' F  o.  G ) : ( 1 ... ( phi `  N ) ) -1-1-onto-> ( 1 ... ( phi `  N ) ) )
356255zcnd 10376 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( phi `  N ) ) )  ->  ( F `  x )  e.  CC )
35767eleq2i 2500 . . . . . . . . 9  |-  ( w  e.  T  <->  w  e.  ( 1 ... ( phi `  N ) ) )
358 fvco3 5800 . . . . . . . . . . . 12  |-  ( ( G : T --> S  /\  w  e.  T )  ->  ( ( `' F  o.  G ) `  w
)  =  ( `' F `  ( G `
 w ) ) )
359162, 358sylan 458 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  T )  ->  (
( `' F  o.  G ) `  w
)  =  ( `' F `  ( G `
 w ) ) )
360359fveq2d 5732 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  T )  ->  ( F `  ( ( `' F  o.  G
) `  w )
)  =  ( F `
 ( `' F `  ( G `  w
) ) ) )
36160adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  T )  ->  F : T -1-1-onto-> S )
362162ffvelrnda 5870 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  T )  ->  ( G `  w )  e.  S )
363 f1ocnvfv2 6015 . . . . . . . . . . 11  |-  ( ( F : T -1-1-onto-> S  /\  ( G `  w )  e.  S )  -> 
( F `  ( `' F `  ( G `
 w ) ) )  =  ( G `
 w ) )
364361, 362, 363syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  T )  ->  ( F `  ( `' F `  ( G `  w ) ) )  =  ( G `  w ) )
365360, 364eqtr2d 2469 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  T )  ->  ( G `  w )  =  ( F `  ( ( `' F  o.  G ) `  w
) ) )
366357, 365sylan2br 463 . . . . . . . 8  |-  ( (
ph  /\  w  e.  ( 1 ... ( phi `  N ) ) )  ->  ( G `  w )  =  ( F `  ( ( `' F  o.  G
) `  w )
) )
367260, 262, 264, 64, 266, 355, 356, 366seqf1o 11364 . . . . . . 7  |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `
 ( phi `  N ) )  =  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) ) )
368367, 257eqeltrd 2510 . . . . . 6  |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `
 ( phi `  N ) )  e.  ZZ )
369 moddvds 12859 . . . . . 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 ) ) ) ) )
3702, 258, 368, 369syl3anc 1184 . . . . 5  |-  ( 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 ) ) ) ) )
371250, 370mpbid 202 . . . 4  |-  ( ph  ->  N  ||  ( ( ( A ^ ( phi `  N ) )  x.  (  seq  1
(  x.  ,  F
) `  ( phi `  N ) ) )  -  (  seq  1
(  x.  ,  G
) `  ( phi `  N ) ) ) )
372257zcnd 10376 . . . . . . . 8  |-  ( ph  ->  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) )  e.  CC )
373372mulid2d 9106 . . . . . . 7  |-  ( ph  ->  ( 1  x.  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )  =  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) )
374367, 373eqtr4d 2471 . . . . . 6  |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `
 ( phi `  N ) )  =  ( 1  x.  (  seq  1 (  x.  ,  F ) `  ( phi `  N ) ) ) )
375374oveq2d 6097 . . . . 5  |-  ( ph  ->  ( ( ( A ^ ( phi `  N ) )  x.  (  seq  1 (  x.  ,  F ) `
 ( phi `  N ) ) )  -  (  seq  1
(  x.  ,  G
) `  ( phi `  N ) ) )