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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	gexid.4	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	gexdvds	$⊢ (G \in Grp \land N \in ℤ) \to (E ∥ N \leftrightarrow \forall x \in X N \underset{˙}{\cdot} x = \underset{˙}{0})$

Proof

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

Metamath Proof Explorer

Theorem gexdvds

Proof