Step |
Hyp |
Ref |
Expression |
1 |
|
lgsdchr.g |
|- G = ( DChr ` N ) |
2 |
|
lgsdchr.z |
|- Z = ( Z/nZ ` N ) |
3 |
|
lgsdchr.d |
|- D = ( Base ` G ) |
4 |
|
lgsdchr.b |
|- B = ( Base ` Z ) |
5 |
|
lgsdchr.l |
|- L = ( ZRHom ` Z ) |
6 |
|
lgsdchr.x |
|- X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) ) |
7 |
|
iotaex |
|- ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) e. _V |
8 |
7
|
a1i |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ y e. B ) -> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) e. _V ) |
9 |
6
|
a1i |
|- ( ( N e. NN /\ -. 2 || N ) -> X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) ) ) |
10 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
11 |
10
|
adantr |
|- ( ( N e. NN /\ -. 2 || N ) -> N e. NN0 ) |
12 |
2 4 5
|
znzrhfo |
|- ( N e. NN0 -> L : ZZ -onto-> B ) |
13 |
11 12
|
syl |
|- ( ( N e. NN /\ -. 2 || N ) -> L : ZZ -onto-> B ) |
14 |
|
foelrn |
|- ( ( L : ZZ -onto-> B /\ x e. B ) -> E. a e. ZZ x = ( L ` a ) ) |
15 |
13 14
|
sylan |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ x e. B ) -> E. a e. ZZ x = ( L ` a ) ) |
16 |
1 2 3 4 5 6
|
lgsdchrval |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( X ` ( L ` a ) ) = ( a /L N ) ) |
17 |
|
simpr |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> a e. ZZ ) |
18 |
|
nnz |
|- ( N e. NN -> N e. ZZ ) |
19 |
18
|
ad2antrr |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> N e. ZZ ) |
20 |
|
lgscl |
|- ( ( a e. ZZ /\ N e. ZZ ) -> ( a /L N ) e. ZZ ) |
21 |
17 19 20
|
syl2anc |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( a /L N ) e. ZZ ) |
22 |
21
|
zred |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( a /L N ) e. RR ) |
23 |
16 22
|
eqeltrd |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( X ` ( L ` a ) ) e. RR ) |
24 |
|
fveq2 |
|- ( x = ( L ` a ) -> ( X ` x ) = ( X ` ( L ` a ) ) ) |
25 |
24
|
eleq1d |
|- ( x = ( L ` a ) -> ( ( X ` x ) e. RR <-> ( X ` ( L ` a ) ) e. RR ) ) |
26 |
23 25
|
syl5ibrcom |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( x = ( L ` a ) -> ( X ` x ) e. RR ) ) |
27 |
26
|
rexlimdva |
|- ( ( N e. NN /\ -. 2 || N ) -> ( E. a e. ZZ x = ( L ` a ) -> ( X ` x ) e. RR ) ) |
28 |
27
|
imp |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ E. a e. ZZ x = ( L ` a ) ) -> ( X ` x ) e. RR ) |
29 |
15 28
|
syldan |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ x e. B ) -> ( X ` x ) e. RR ) |
30 |
8 9 29
|
fmpt2d |
|- ( ( N e. NN /\ -. 2 || N ) -> X : B --> RR ) |
31 |
|
ax-resscn |
|- RR C_ CC |
32 |
|
fss |
|- ( ( X : B --> RR /\ RR C_ CC ) -> X : B --> CC ) |
33 |
30 31 32
|
sylancl |
|- ( ( N e. NN /\ -. 2 || N ) -> X : B --> CC ) |
34 |
|
eqid |
|- ( Unit ` Z ) = ( Unit ` Z ) |
35 |
4 34
|
unitss |
|- ( Unit ` Z ) C_ B |
36 |
|
foelrn |
|- ( ( L : ZZ -onto-> B /\ y e. B ) -> E. b e. ZZ y = ( L ` b ) ) |
37 |
13 36
|
sylan |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ y e. B ) -> E. b e. ZZ y = ( L ` b ) ) |
38 |
15 37
|
anim12dan |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( x e. B /\ y e. B ) ) -> ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) ) |
39 |
|
reeanv |
|- ( E. a e. ZZ E. b e. ZZ ( x = ( L ` a ) /\ y = ( L ` b ) ) <-> ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) ) |
40 |
17
|
adantrr |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ ) |
41 |
|
simprr |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ ) |
42 |
11
|
adantr |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> N e. NN0 ) |
43 |
|
lgsdirnn0 |
|- ( ( a e. ZZ /\ b e. ZZ /\ N e. NN0 ) -> ( ( a x. b ) /L N ) = ( ( a /L N ) x. ( b /L N ) ) ) |
44 |
40 41 42 43
|
syl3anc |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a x. b ) /L N ) = ( ( a /L N ) x. ( b /L N ) ) ) |
45 |
2
|
zncrng |
|- ( N e. NN0 -> Z e. CRing ) |
46 |
11 45
|
syl |
|- ( ( N e. NN /\ -. 2 || N ) -> Z e. CRing ) |
47 |
|
crngring |
|- ( Z e. CRing -> Z e. Ring ) |
48 |
46 47
|
syl |
|- ( ( N e. NN /\ -. 2 || N ) -> Z e. Ring ) |
49 |
48
|
adantr |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> Z e. Ring ) |
50 |
5
|
zrhrhm |
|- ( Z e. Ring -> L e. ( ZZring RingHom Z ) ) |
51 |
49 50
|
syl |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> L e. ( ZZring RingHom Z ) ) |
52 |
|
zringbas |
|- ZZ = ( Base ` ZZring ) |
53 |
|
zringmulr |
|- x. = ( .r ` ZZring ) |
54 |
|
eqid |
|- ( .r ` Z ) = ( .r ` Z ) |
55 |
52 53 54
|
rhmmul |
|- ( ( L e. ( ZZring RingHom Z ) /\ a e. ZZ /\ b e. ZZ ) -> ( L ` ( a x. b ) ) = ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) |
56 |
51 40 41 55
|
syl3anc |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( L ` ( a x. b ) ) = ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) |
57 |
56
|
fveq2d |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` ( a x. b ) ) ) = ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) ) |
58 |
|
zmulcl |
|- ( ( a e. ZZ /\ b e. ZZ ) -> ( a x. b ) e. ZZ ) |
59 |
1 2 3 4 5 6
|
lgsdchrval |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a x. b ) e. ZZ ) -> ( X ` ( L ` ( a x. b ) ) ) = ( ( a x. b ) /L N ) ) |
60 |
58 59
|
sylan2 |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` ( a x. b ) ) ) = ( ( a x. b ) /L N ) ) |
61 |
57 60
|
eqtr3d |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) = ( ( a x. b ) /L N ) ) |
62 |
16
|
adantrr |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` a ) ) = ( a /L N ) ) |
63 |
1 2 3 4 5 6
|
lgsdchrval |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ b e. ZZ ) -> ( X ` ( L ` b ) ) = ( b /L N ) ) |
64 |
63
|
adantrl |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` b ) ) = ( b /L N ) ) |
65 |
62 64
|
oveq12d |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) = ( ( a /L N ) x. ( b /L N ) ) ) |
66 |
44 61 65
|
3eqtr4d |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) = ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) ) |
67 |
|
oveq12 |
|- ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( x ( .r ` Z ) y ) = ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) |
68 |
67
|
fveq2d |
|- ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) ) |
69 |
|
fveq2 |
|- ( y = ( L ` b ) -> ( X ` y ) = ( X ` ( L ` b ) ) ) |
70 |
24 69
|
oveqan12d |
|- ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( ( X ` x ) x. ( X ` y ) ) = ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) ) |
71 |
68 70
|
eqeq12d |
|- ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) = ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) ) ) |
72 |
66 71
|
syl5ibrcom |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) |
73 |
72
|
rexlimdvva |
|- ( ( N e. NN /\ -. 2 || N ) -> ( E. a e. ZZ E. b e. ZZ ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) |
74 |
39 73
|
syl5bir |
|- ( ( N e. NN /\ -. 2 || N ) -> ( ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) |
75 |
74
|
imp |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) |
76 |
38 75
|
syldan |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ ( x e. B /\ y e. B ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) |
77 |
76
|
ralrimivva |
|- ( ( N e. NN /\ -. 2 || N ) -> A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) |
78 |
|
ss2ralv |
|- ( ( Unit ` Z ) C_ B -> ( A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) -> A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) |
79 |
35 77 78
|
mpsyl |
|- ( ( N e. NN /\ -. 2 || N ) -> A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) |
80 |
|
1z |
|- 1 e. ZZ |
81 |
1 2 3 4 5 6
|
lgsdchrval |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ 1 e. ZZ ) -> ( X ` ( L ` 1 ) ) = ( 1 /L N ) ) |
82 |
80 81
|
mpan2 |
|- ( ( N e. NN /\ -. 2 || N ) -> ( X ` ( L ` 1 ) ) = ( 1 /L N ) ) |
83 |
|
eqid |
|- ( 1r ` Z ) = ( 1r ` Z ) |
84 |
5 83
|
zrh1 |
|- ( Z e. Ring -> ( L ` 1 ) = ( 1r ` Z ) ) |
85 |
48 84
|
syl |
|- ( ( N e. NN /\ -. 2 || N ) -> ( L ` 1 ) = ( 1r ` Z ) ) |
86 |
85
|
fveq2d |
|- ( ( N e. NN /\ -. 2 || N ) -> ( X ` ( L ` 1 ) ) = ( X ` ( 1r ` Z ) ) ) |
87 |
18
|
adantr |
|- ( ( N e. NN /\ -. 2 || N ) -> N e. ZZ ) |
88 |
|
1lgs |
|- ( N e. ZZ -> ( 1 /L N ) = 1 ) |
89 |
87 88
|
syl |
|- ( ( N e. NN /\ -. 2 || N ) -> ( 1 /L N ) = 1 ) |
90 |
82 86 89
|
3eqtr3d |
|- ( ( N e. NN /\ -. 2 || N ) -> ( X ` ( 1r ` Z ) ) = 1 ) |
91 |
|
lgsne0 |
|- ( ( a e. ZZ /\ N e. ZZ ) -> ( ( a /L N ) =/= 0 <-> ( a gcd N ) = 1 ) ) |
92 |
17 19 91
|
syl2anc |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( a /L N ) =/= 0 <-> ( a gcd N ) = 1 ) ) |
93 |
92
|
biimpd |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( a /L N ) =/= 0 -> ( a gcd N ) = 1 ) ) |
94 |
16
|
neeq1d |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( X ` ( L ` a ) ) =/= 0 <-> ( a /L N ) =/= 0 ) ) |
95 |
2 34 5
|
znunit |
|- ( ( N e. NN0 /\ a e. ZZ ) -> ( ( L ` a ) e. ( Unit ` Z ) <-> ( a gcd N ) = 1 ) ) |
96 |
11 95
|
sylan |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( L ` a ) e. ( Unit ` Z ) <-> ( a gcd N ) = 1 ) ) |
97 |
93 94 96
|
3imtr4d |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( X ` ( L ` a ) ) =/= 0 -> ( L ` a ) e. ( Unit ` Z ) ) ) |
98 |
24
|
neeq1d |
|- ( x = ( L ` a ) -> ( ( X ` x ) =/= 0 <-> ( X ` ( L ` a ) ) =/= 0 ) ) |
99 |
|
eleq1 |
|- ( x = ( L ` a ) -> ( x e. ( Unit ` Z ) <-> ( L ` a ) e. ( Unit ` Z ) ) ) |
100 |
98 99
|
imbi12d |
|- ( x = ( L ` a ) -> ( ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) <-> ( ( X ` ( L ` a ) ) =/= 0 -> ( L ` a ) e. ( Unit ` Z ) ) ) ) |
101 |
97 100
|
syl5ibrcom |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( x = ( L ` a ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) ) |
102 |
101
|
rexlimdva |
|- ( ( N e. NN /\ -. 2 || N ) -> ( E. a e. ZZ x = ( L ` a ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) ) |
103 |
102
|
imp |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ E. a e. ZZ x = ( L ` a ) ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) |
104 |
15 103
|
syldan |
|- ( ( ( N e. NN /\ -. 2 || N ) /\ x e. B ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) |
105 |
104
|
ralrimiva |
|- ( ( N e. NN /\ -. 2 || N ) -> A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) |
106 |
79 90 105
|
3jca |
|- ( ( N e. NN /\ -. 2 || N ) -> ( A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) ) |
107 |
|
simpl |
|- ( ( N e. NN /\ -. 2 || N ) -> N e. NN ) |
108 |
1 2 4 34 107 3
|
dchrelbas3 |
|- ( ( N e. NN /\ -. 2 || N ) -> ( X e. D <-> ( X : B --> CC /\ ( A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) ) ) ) |
109 |
33 106 108
|
mpbir2and |
|- ( ( N e. NN /\ -. 2 || N ) -> X e. D ) |
110 |
109 30
|
jca |
|- ( ( N e. NN /\ -. 2 || N ) -> ( X e. D /\ X : B --> RR ) ) |