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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexcl.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
gexid.3 ⊢ · = ( .g ‘ 𝐺 )
gexid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion gexdvds ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → ( 𝐸 ∥ 𝑁 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑁 · 𝑥 ) = 0 ) )

Proof

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