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=BaseG
gexcl.2 ⊢E=gEx⁡G
gexid.3 ⊢·˙=⋅G
gexid.4 ⊢0˙=0G
Assertion gexdvds ⊢G∈Grp∧N∈ℤ→E∥N↔∀x∈XN·˙x=0˙

Proof

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