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 ) )