Metamath Proof Explorer

Theorem gexdvds

Description: The only N that annihilate all the elements of the group are the multiples of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexcl.1 
|- X = ( Base ` G )
gexcl.2 
|- E = ( gEx ` G )
gexid.3 
|- .x. = ( .g ` G )
gexid.4 
|- .0. = ( 0g ` G )
Assertion gexdvds 
|- ( ( G e. Grp /\ N e. ZZ ) -> ( E || N <-> A. x e. X ( N .x. x ) = .0. ) )

Proof

Step Hyp Ref Expression
1 gexcl.1 
 |-  X = ( Base ` G )
2 gexcl.2 
 |-  E = ( gEx ` G )
3 gexid.3 
 |-  .x. = ( .g ` G )
4 gexid.4 
 |-  .0. = ( 0g ` G )
5 1 2 3 4 gexdvdsi 
 |-  ( ( G e. Grp /\ x e. X /\ E || N ) -> ( N .x. x ) = .0. )
6 5 3expia 
 |-  ( ( G e. Grp /\ x e. X ) -> ( E || N -> ( N .x. x ) = .0. ) )
7 6 ralrimdva 
 |-  ( G e. Grp -> ( E || N -> A. x e. X ( N .x. x ) = .0. ) )
8 7 adantr 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> ( E || N -> A. x e. X ( N .x. x ) = .0. ) )
9 noel 
 |-  -. ( abs ` N ) e. (/)
10 simprr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) )
11 10 eleq2d 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( ( abs ` N ) e. { y e. NN | A. x e. X ( y .x. x ) = .0. } <-> ( abs ` N ) e. (/) ) )
12 oveq1 
 |-  ( y = ( abs ` N ) -> ( y .x. x ) = ( ( abs ` N ) .x. x ) )
13 12 eqeq1d 
 |-  ( y = ( abs ` N ) -> ( ( y .x. x ) = .0. <-> ( ( abs ` N ) .x. x ) = .0. ) )
14 13 ralbidv 
 |-  ( y = ( abs ` N ) -> ( A. x e. X ( y .x. x ) = .0. <-> A. x e. X ( ( abs ` N ) .x. x ) = .0. ) )
15 14 elrab 
 |-  ( ( abs ` N ) e. { y e. NN | A. x e. X ( y .x. x ) = .0. } <-> ( ( abs ` N ) e. NN /\ A. x e. X ( ( abs ` N ) .x. x ) = .0. ) )
16 11 15 bitr3di 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( ( abs ` N ) e. (/) <-> ( ( abs ` N ) e. NN /\ A. x e. X ( ( abs ` N ) .x. x ) = .0. ) ) )
17 16 rbaibd 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) /\ A. x e. X ( ( abs ` N ) .x. x ) = .0. ) -> ( ( abs ` N ) e. (/) <-> ( abs ` N ) e. NN ) )
18 9 17 mtbii 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) /\ A. x e. X ( ( abs ` N ) .x. x ) = .0. ) -> -. ( abs ` N ) e. NN )
19 18 ex 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( A. x e. X ( ( abs ` N ) .x. x ) = .0. -> -. ( abs ` N ) e. NN ) )
20 nn0abscl 
 |-  ( N e. ZZ -> ( abs ` N ) e. NN0 )
21 20 ad2antlr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( abs ` N ) e. NN0 )
22 elnn0 
 |-  ( ( abs ` N ) e. NN0 <-> ( ( abs ` N ) e. NN \/ ( abs ` N ) = 0 ) )
23 21 22 sylib 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( ( abs ` N ) e. NN \/ ( abs ` N ) = 0 ) )
24 23 ord 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( -. ( abs ` N ) e. NN -> ( abs ` N ) = 0 ) )
25 19 24 syld 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( A. x e. X ( ( abs ` N ) .x. x ) = .0. -> ( abs ` N ) = 0 ) )
26 simpr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) /\ ( abs ` N ) = N ) -> ( abs ` N ) = N )
27 26 oveq1d 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) /\ ( abs ` N ) = N ) -> ( ( abs ` N ) .x. x ) = ( N .x. x ) )
28 27 eqeq1d 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) /\ ( abs ` N ) = N ) -> ( ( ( abs ` N ) .x. x ) = .0. <-> ( N .x. x ) = .0. ) )
29 oveq1 
 |-  ( ( abs ` N ) = -u N -> ( ( abs ` N ) .x. x ) = ( -u N .x. x ) )
30 29 eqeq1d 
 |-  ( ( abs ` N ) = -u N -> ( ( ( abs ` N ) .x. x ) = .0. <-> ( -u N .x. x ) = .0. ) )
31 eqid 
 |-  ( invg ` G ) = ( invg ` G )
32 1 3 31 mulgneg 
 |-  ( ( G e. Grp /\ N e. ZZ /\ x e. X ) -> ( -u N .x. x ) = ( ( invg ` G ) ` ( N .x. x ) ) )
33 32 3expa 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( -u N .x. x ) = ( ( invg ` G ) ` ( N .x. x ) ) )
34 4 31 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
35 34 ad2antrr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( ( invg ` G ) ` .0. ) = .0. )
36 35 eqcomd 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> .0. = ( ( invg ` G ) ` .0. ) )
37 33 36 eqeq12d 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( ( -u N .x. x ) = .0. <-> ( ( invg ` G ) ` ( N .x. x ) ) = ( ( invg ` G ) ` .0. ) ) )
38 simpll 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> G e. Grp )
39 1 3 mulgcl 
 |-  ( ( G e. Grp /\ N e. ZZ /\ x e. X ) -> ( N .x. x ) e. X )
40 39 3expa 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( N .x. x ) e. X )
41 1 4 grpidcl 
 |-  ( G e. Grp -> .0. e. X )
42 41 ad2antrr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> .0. e. X )
43 1 31 38 40 42 grpinv11 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( ( ( invg ` G ) ` ( N .x. x ) ) = ( ( invg ` G ) ` .0. ) <-> ( N .x. x ) = .0. ) )
44 37 43 bitrd 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( ( -u N .x. x ) = .0. <-> ( N .x. x ) = .0. ) )
45 30 44 sylan9bbr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) /\ ( abs ` N ) = -u N ) -> ( ( ( abs ` N ) .x. x ) = .0. <-> ( N .x. x ) = .0. ) )
46 zre 
 |-  ( N e. ZZ -> N e. RR )
47 46 ad2antlr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> N e. RR )
48 47 absord 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) )
49 28 45 48 mpjaodan 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ x e. X ) -> ( ( ( abs ` N ) .x. x ) = .0. <-> ( N .x. x ) = .0. ) )
50 49 ralbidva 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> ( A. x e. X ( ( abs ` N ) .x. x ) = .0. <-> A. x e. X ( N .x. x ) = .0. ) )
51 50 adantr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( A. x e. X ( ( abs ` N ) .x. x ) = .0. <-> A. x e. X ( N .x. x ) = .0. ) )
52 0dvds 
 |-  ( N e. ZZ -> ( 0 || N <-> N = 0 ) )
53 52 ad2antlr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( 0 || N <-> N = 0 ) )
54 simprl 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> E = 0 )
55 54 breq1d 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( E || N <-> 0 || N ) )
56 zcn 
 |-  ( N e. ZZ -> N e. CC )
57 56 ad2antlr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> N e. CC )
58 57 abs00ad 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( ( abs ` N ) = 0 <-> N = 0 ) )
59 53 55 58 3bitr4rd 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( ( abs ` N ) = 0 <-> E || N ) )
60 25 51 59 3imtr3d 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( A. x e. X ( N .x. x ) = .0. -> E || N ) )
61 elrabi 
 |-  ( E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> E e. NN )
62 46 adantl 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> N e. RR )
63 nnrp 
 |-  ( E e. NN -> E e. RR+ )
64 modval 
 |-  ( ( N e. RR /\ E e. RR+ ) -> ( N mod E ) = ( N - ( E x. ( |_ ` ( N / E ) ) ) ) )
65 62 63 64 syl2an 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( N mod E ) = ( N - ( E x. ( |_ ` ( N / E ) ) ) ) )
66 65 adantr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( N mod E ) = ( N - ( E x. ( |_ ` ( N / E ) ) ) ) )
67 66 oveq1d 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( ( N mod E ) .x. x ) = ( ( N - ( E x. ( |_ ` ( N / E ) ) ) ) .x. x ) )
68 simplll 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> G e. Grp )
69 simpllr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> N e. ZZ )
70 nnz 
 |-  ( E e. NN -> E e. ZZ )
71 70 ad2antlr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> E e. ZZ )
72 rerpdivcl 
 |-  ( ( N e. RR /\ E e. RR+ ) -> ( N / E ) e. RR )
73 62 63 72 syl2an 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( N / E ) e. RR )
74 73 flcld 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( |_ ` ( N / E ) ) e. ZZ )
75 74 adantr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( |_ ` ( N / E ) ) e. ZZ )
76 71 75 zmulcld 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( E x. ( |_ ` ( N / E ) ) ) e. ZZ )
77 simprl 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> x e. X )
78 eqid 
 |-  ( -g ` G ) = ( -g ` G )
79 1 3 78 mulgsubdir 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ ( E x. ( |_ ` ( N / E ) ) ) e. ZZ /\ x e. X ) ) -> ( ( N - ( E x. ( |_ ` ( N / E ) ) ) ) .x. x ) = ( ( N .x. x ) ( -g ` G ) ( ( E x. ( |_ ` ( N / E ) ) ) .x. x ) ) )
80 68 69 76 77 79 syl13anc 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( ( N - ( E x. ( |_ ` ( N / E ) ) ) ) .x. x ) = ( ( N .x. x ) ( -g ` G ) ( ( E x. ( |_ ` ( N / E ) ) ) .x. x ) ) )
81 simprr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( N .x. x ) = .0. )
82 dvdsmul1 
 |-  ( ( E e. ZZ /\ ( |_ ` ( N / E ) ) e. ZZ ) -> E || ( E x. ( |_ ` ( N / E ) ) ) )
83 71 75 82 syl2anc 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> E || ( E x. ( |_ ` ( N / E ) ) ) )
84 1 2 3 4 gexdvdsi 
 |-  ( ( G e. Grp /\ x e. X /\ E || ( E x. ( |_ ` ( N / E ) ) ) ) -> ( ( E x. ( |_ ` ( N / E ) ) ) .x. x ) = .0. )
85 68 77 83 84 syl3anc 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( ( E x. ( |_ ` ( N / E ) ) ) .x. x ) = .0. )
86 81 85 oveq12d 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( ( N .x. x ) ( -g ` G ) ( ( E x. ( |_ ` ( N / E ) ) ) .x. x ) ) = ( .0. ( -g ` G ) .0. ) )
87 simpll 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> G e. Grp )
88 1 4 78 grpsubid 
 |-  ( ( G e. Grp /\ .0. e. X ) -> ( .0. ( -g ` G ) .0. ) = .0. )
89 87 41 88 syl2anc2 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( .0. ( -g ` G ) .0. ) = .0. )
90 89 adantr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( .0. ( -g ` G ) .0. ) = .0. )
91 86 90 eqtrd 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( ( N .x. x ) ( -g ` G ) ( ( E x. ( |_ ` ( N / E ) ) ) .x. x ) ) = .0. )
92 67 80 91 3eqtrd 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ ( x e. X /\ ( N .x. x ) = .0. ) ) -> ( ( N mod E ) .x. x ) = .0. )
93 92 expr 
 |-  ( ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) /\ x e. X ) -> ( ( N .x. x ) = .0. -> ( ( N mod E ) .x. x ) = .0. ) )
94 93 ralimdva 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( A. x e. X ( N .x. x ) = .0. -> A. x e. X ( ( N mod E ) .x. x ) = .0. ) )
95 modlt 
 |-  ( ( N e. RR /\ E e. RR+ ) -> ( N mod E ) < E )
96 62 63 95 syl2an 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( N mod E ) < E )
97 zmodcl 
 |-  ( ( N e. ZZ /\ E e. NN ) -> ( N mod E ) e. NN0 )
98 97 adantll 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( N mod E ) e. NN0 )
99 98 nn0red 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( N mod E ) e. RR )
100 nnre 
 |-  ( E e. NN -> E e. RR )
101 100 adantl 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> E e. RR )
102 99 101 ltnled 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( ( N mod E ) < E <-> -. E <_ ( N mod E ) ) )
103 96 102 mpbid 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> -. E <_ ( N mod E ) )
104 1 2 3 4 gexlem2 
 |-  ( ( G e. Grp /\ ( N mod E ) e. NN /\ A. x e. X ( ( N mod E ) .x. x ) = .0. ) -> E e. ( 1 ... ( N mod E ) ) )
105 elfzle2 
 |-  ( E e. ( 1 ... ( N mod E ) ) -> E <_ ( N mod E ) )
106 104 105 syl 
 |-  ( ( G e. Grp /\ ( N mod E ) e. NN /\ A. x e. X ( ( N mod E ) .x. x ) = .0. ) -> E <_ ( N mod E ) )
107 106 3expia 
 |-  ( ( G e. Grp /\ ( N mod E ) e. NN ) -> ( A. x e. X ( ( N mod E ) .x. x ) = .0. -> E <_ ( N mod E ) ) )
108 107 impancom 
 |-  ( ( G e. Grp /\ A. x e. X ( ( N mod E ) .x. x ) = .0. ) -> ( ( N mod E ) e. NN -> E <_ ( N mod E ) ) )
109 108 con3d 
 |-  ( ( G e. Grp /\ A. x e. X ( ( N mod E ) .x. x ) = .0. ) -> ( -. E <_ ( N mod E ) -> -. ( N mod E ) e. NN ) )
110 109 ex 
 |-  ( G e. Grp -> ( A. x e. X ( ( N mod E ) .x. x ) = .0. -> ( -. E <_ ( N mod E ) -> -. ( N mod E ) e. NN ) ) )
111 110 ad2antrr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( A. x e. X ( ( N mod E ) .x. x ) = .0. -> ( -. E <_ ( N mod E ) -> -. ( N mod E ) e. NN ) ) )
112 103 111 mpid 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( A. x e. X ( ( N mod E ) .x. x ) = .0. -> -. ( N mod E ) e. NN ) )
113 elnn0 
 |-  ( ( N mod E ) e. NN0 <-> ( ( N mod E ) e. NN \/ ( N mod E ) = 0 ) )
114 98 113 sylib 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( ( N mod E ) e. NN \/ ( N mod E ) = 0 ) )
115 114 ord 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( -. ( N mod E ) e. NN -> ( N mod E ) = 0 ) )
116 94 112 115 3syld 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( A. x e. X ( N .x. x ) = .0. -> ( N mod E ) = 0 ) )
117 simpr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> E e. NN )
118 simplr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> N e. ZZ )
119 dvdsval3 
 |-  ( ( E e. NN /\ N e. ZZ ) -> ( E || N <-> ( N mod E ) = 0 ) )
120 117 118 119 syl2anc 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( E || N <-> ( N mod E ) = 0 ) )
121 116 120 sylibrd 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. NN ) -> ( A. x e. X ( N .x. x ) = .0. -> E || N ) )
122 61 121 sylan2 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> ( A. x e. X ( N .x. x ) = .0. -> E || N ) )
123 eqid 
 |-  { y e. NN | A. x e. X ( y .x. x ) = .0. } = { y e. NN | A. x e. X ( y .x. x ) = .0. }
124 1 3 4 2 123 gexlem1 
 |-  ( G e. Grp -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) \/ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) )
125 124 adantr 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) \/ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) )
126 60 122 125 mpjaodan 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> ( A. x e. X ( N .x. x ) = .0. -> E || N ) )
127 8 126 impbid 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> ( E || N <-> A. x e. X ( N .x. x ) = .0. ) )