gexex

Description: In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if E = 0 , for example in an infinite p-group, where there are elements of arbitrarily large orders (so E is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexex.1	$⊢ X = {Base}_{G}$
	gexex.2	$⊢ E = gEx (G)$
	gexex.3	$⊢ O = od (G)$
Assertion	gexex	$⊢ (G \in Abel \land E \in ℕ) \to \exists x \in X O (x) = E$

Proof

Step	Hyp	Ref	Expression
1		gexex.1	$⊢ X = {Base}_{G}$
2		gexex.2	$⊢ E = gEx (G)$
3		gexex.3	$⊢ O = od (G)$
4		simpll	$⊢ ((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \to G \in Abel$
5		simplr	$⊢ ((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \to E \in ℕ$
6		simprl	$⊢ ((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \to x \in X$
7	1 3	odf	$⊢ O : X ⟶ ℕ_{0}$
8		frn	$⊢ O : X ⟶ ℕ_{0} \to ran O \subseteq ℕ_{0}$
9	7 8	ax-mp	$⊢ ran O \subseteq ℕ_{0}$
10		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
11	9 10	sstri	$⊢ ran O \subseteq ℤ$
12		nnz	$⊢ E \in ℕ \to E \in ℤ$
13	12	adantl	$⊢ (G \in Abel \land E \in ℕ) \to E \in ℤ$
14		ablgrp	$⊢ G \in Abel \to G \in Grp$
15	14	adantr	$⊢ (G \in Abel \land E \in ℕ) \to G \in Grp$
16	1 2 3	gexod	$⊢ (G \in Grp \land x \in X) \to O (x) ∥ E$
17	15 16	sylan	$⊢ ((G \in Abel \land E \in ℕ) \land x \in X) \to O (x) ∥ E$
18	1 3	odcl	$⊢ x \in X \to O (x) \in ℕ_{0}$
19	18	adantl	$⊢ ((G \in Abel \land E \in ℕ) \land x \in X) \to O (x) \in ℕ_{0}$
20	19	nn0zd	$⊢ ((G \in Abel \land E \in ℕ) \land x \in X) \to O (x) \in ℤ$
21		simplr	$⊢ ((G \in Abel \land E \in ℕ) \land x \in X) \to E \in ℕ$
22		dvdsle	$⊢ (O (x) \in ℤ \land E \in ℕ) \to (O (x) ∥ E \to O (x) \leq E)$
23	20 21 22	syl2anc	$⊢ ((G \in Abel \land E \in ℕ) \land x \in X) \to (O (x) ∥ E \to O (x) \leq E)$
24	17 23	mpd	$⊢ ((G \in Abel \land E \in ℕ) \land x \in X) \to O (x) \leq E$
25	24	ralrimiva	$⊢ (G \in Abel \land E \in ℕ) \to \forall x \in X O (x) \leq E$
26		ffn	$⊢ O : X ⟶ ℕ_{0} \to O Fn X$
27	7 26	ax-mp	$⊢ O Fn X$
28		breq1	$⊢ y = O (x) \to (y \leq E \leftrightarrow O (x) \leq E)$
29	28	ralrn	$⊢ O Fn X \to (\forall y \in ran O y \leq E \leftrightarrow \forall x \in X O (x) \leq E)$
30	27 29	ax-mp	$⊢ \forall y \in ran O y \leq E \leftrightarrow \forall x \in X O (x) \leq E$
31	25 30	sylibr	$⊢ (G \in Abel \land E \in ℕ) \to \forall y \in ran O y \leq E$
32		brralrspcev	$⊢ (E \in ℤ \land \forall y \in ran O y \leq E) \to \exists n \in ℤ \forall y \in ran O y \leq n$
33	13 31 32	syl2anc	$⊢ (G \in Abel \land E \in ℕ) \to \exists n \in ℤ \forall y \in ran O y \leq n$
34	33	ad2antrr	$⊢ (((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \land y \in X) \to \exists n \in ℤ \forall y \in ran O y \leq n$
35	27	a1i	$⊢ ((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \to O Fn X$
36		fnfvelrn	$⊢ (O Fn X \land y \in X) \to O (y) \in ran O$
37	35 36	sylan	$⊢ (((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \land y \in X) \to O (y) \in ran O$
38		suprzub	$⊢ (ran O \subseteq ℤ \land \exists n \in ℤ \forall y \in ran O y \leq n \land O (y) \in ran O) \to O (y) \leq sup (ran O ℝ <)$
39	11 34 37 38	mp3an2i	$⊢ (((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \land y \in X) \to O (y) \leq sup (ran O ℝ <)$
40		simplrr	$⊢ (((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \land y \in X) \to O (x) = sup (ran O ℝ <)$
41	39 40	breqtrrd	$⊢ (((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \land y \in X) \to O (y) \leq O (x)$
42	1 2 3 4 5 6 41	gexexlem	$⊢ ((G \in Abel \land E \in ℕ) \land (x \in X \land O (x) = sup (ran O ℝ <))) \to O (x) = E$
43	1	grpbn0	$⊢ G \in Grp \to X \neq \emptyset$
44	15 43	syl	$⊢ (G \in Abel \land E \in ℕ) \to X \neq \emptyset$
45	7	fdmi	$⊢ dom O = X$
46	45	eqeq1i	$⊢ dom O = \emptyset \leftrightarrow X = \emptyset$
47		dm0rn0	$⊢ dom O = \emptyset \leftrightarrow ran O = \emptyset$
48	46 47	bitr3i	$⊢ X = \emptyset \leftrightarrow ran O = \emptyset$
49	48	necon3bii	$⊢ X \neq \emptyset \leftrightarrow ran O \neq \emptyset$
50	44 49	sylib	$⊢ (G \in Abel \land E \in ℕ) \to ran O \neq \emptyset$
51		suprzcl2	$⊢ (ran O \subseteq ℤ \land ran O \neq \emptyset \land \exists n \in ℤ \forall y \in ran O y \leq n) \to sup (ran O ℝ <) \in ran O$
52	11 50 33 51	mp3an2i	$⊢ (G \in Abel \land E \in ℕ) \to sup (ran O ℝ <) \in ran O$
53		fvelrnb	$⊢ O Fn X \to (sup (ran O ℝ <) \in ran O \leftrightarrow \exists x \in X O (x) = sup (ran O ℝ <))$
54	27 53	ax-mp	$⊢ sup (ran O ℝ <) \in ran O \leftrightarrow \exists x \in X O (x) = sup (ran O ℝ <)$
55	52 54	sylib	$⊢ (G \in Abel \land E \in ℕ) \to \exists x \in X O (x) = sup (ran O ℝ <)$
56	42 55	reximddv	$⊢ (G \in Abel \land E \in ℕ) \to \exists x \in X O (x) = E$

Metamath Proof Explorer

Theorem gexex

Proof