odcau

Description: Cauchy's theorem for the order of an element in a group. A finite group whose order divides a prime P contains an element of order P . (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypotheses	odcau.x	$⊢ X = {Base}_{G}$
	odcau.o	$⊢ O = od (G)$
Assertion	odcau	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to \exists g \in X O (g) = P$

Proof

Step	Hyp	Ref	Expression
1		odcau.x	$⊢ X = {Base}_{G}$
2		odcau.o	$⊢ O = od (G)$
3		simpl1	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to G \in Grp$
4		simpl2	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to X \in Fin$
5		simpl3	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to P \in ℙ$
6		1nn0	$⊢ 1 \in ℕ_{0}$
7	6	a1i	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to 1 \in ℕ_{0}$
8		prmnn	$⊢ P \in ℙ \to P \in ℕ$
9	5 8	syl	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to P \in ℕ$
10	9	nncnd	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to P \in ℂ$
11	10	exp1d	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to P^{1} = P$
12		simpr	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to P ∥ \|X\|$
13	11 12	eqbrtrd	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to P^{1} ∥ \|X\|$
14	1 3 4 5 7 13	sylow1	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to \exists s \in SubGrp (G) \|s\| = P^{1}$
15	11	eqeq2d	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to (\|s\| = P^{1} \leftrightarrow \|s\| = P)$
16	15	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land s \in SubGrp (G)) \to (\|s\| = P^{1} \leftrightarrow \|s\| = P)$
17		fvex	$⊢ 0_{G} \in V$
18		hashsng	$⊢ 0_{G} \in V \to \|\{0_{G}\}\| = 1$
19	17 18	ax-mp	$⊢ \|\{0_{G}\}\| = 1$
20		simprr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to \|s\| = P$
21	5	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to P \in ℙ$
22		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
23	21 22	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to P \in ℤ_{\geq 2}$
24	20 23	eqeltrd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to \|s\| \in ℤ_{\geq 2}$
25		eluz2gt1	$⊢ \|s\| \in ℤ_{\geq 2} \to 1 < \|s\|$
26	24 25	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to 1 < \|s\|$
27	19 26	eqbrtrid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to \|\{0_{G}\}\| < \|s\|$
28		snfi	$⊢ \{0_{G}\} \in Fin$
29	4	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to X \in Fin$
30	1	subgss	$⊢ s \in SubGrp (G) \to s \subseteq X$
31	30	ad2antrl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to s \subseteq X$
32	29 31	ssfid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to s \in Fin$
33		hashsdom	$⊢ (\{0_{G}\} \in Fin \land s \in Fin) \to (\|\{0_{G}\}\| < \|s\| \leftrightarrow \{0_{G}\} ≺ s)$
34	28 32 33	sylancr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to (\|\{0_{G}\}\| < \|s\| \leftrightarrow \{0_{G}\} ≺ s)$
35	27 34	mpbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to \{0_{G}\} ≺ s$
36		sdomdif	$⊢ \{0_{G}\} ≺ s \to s ∖ \{0_{G}\} \neq \emptyset$
37	35 36	syl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to s ∖ \{0_{G}\} \neq \emptyset$
38		n0	$⊢ s ∖ \{0_{G}\} \neq \emptyset \leftrightarrow \exists g g \in (s ∖ \{0_{G}\})$
39	37 38	sylib	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to \exists g g \in (s ∖ \{0_{G}\})$
40		eldifsn	$⊢ g \in (s ∖ \{0_{G}\}) \leftrightarrow (g \in s \land g \neq 0_{G})$
41	31	adantrr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to s \subseteq X$
42		simprrl	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to g \in s$
43	41 42	sseldd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to g \in X$
44		simprrr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to g \neq 0_{G}$
45		simprll	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to s \in SubGrp (G)$
46	32	adantrr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to s \in Fin$
47	2	odsubdvds	$⊢ (s \in SubGrp (G) \land s \in Fin \land g \in s) \to O (g) ∥ \|s\|$
48	45 46 42 47	syl3anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to O (g) ∥ \|s\|$
49		simprlr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to \|s\| = P$
50	48 49	breqtrd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to O (g) ∥ P$
51	3	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to G \in Grp$
52	4	adantr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to X \in Fin$
53	1 2	odcl2	$⊢ (G \in Grp \land X \in Fin \land g \in X) \to O (g) \in ℕ$
54	51 52 43 53	syl3anc	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to O (g) \in ℕ$
55		dvdsprime	$⊢ (P \in ℙ \land O (g) \in ℕ) \to (O (g) ∥ P \leftrightarrow (O (g) = P \lor O (g) = 1))$
56	5 54 55	syl2an2r	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to (O (g) ∥ P \leftrightarrow (O (g) = P \lor O (g) = 1))$
57	50 56	mpbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to (O (g) = P \lor O (g) = 1)$
58	57	ord	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to (\neg O (g) = P \to O (g) = 1)$
59		eqid	$⊢ 0_{G} = 0_{G}$
60	2 59 1	odeq1	$⊢ (G \in Grp \land g \in X) \to (O (g) = 1 \leftrightarrow g = 0_{G})$
61	3 43 60	syl2an2r	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to (O (g) = 1 \leftrightarrow g = 0_{G})$
62	58 61	sylibd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to (\neg O (g) = P \to g = 0_{G})$
63	62	necon1ad	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to (g \neq 0_{G} \to O (g) = P)$
64	44 63	mpd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to O (g) = P$
65	43 64	jca	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land ((s \in SubGrp (G) \land \|s\| = P) \land (g \in s \land g \neq 0_{G}))) \to (g \in X \land O (g) = P)$
66	65	expr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to ((g \in s \land g \neq 0_{G}) \to (g \in X \land O (g) = P))$
67	40 66	biimtrid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to (g \in (s ∖ \{0_{G}\}) \to (g \in X \land O (g) = P))$
68	67	eximdv	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to (\exists g g \in (s ∖ \{0_{G}\}) \to \exists g (g \in X \land O (g) = P))$
69	39 68	mpd	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to \exists g (g \in X \land O (g) = P)$
70		df-rex	$⊢ \exists g \in X O (g) = P \leftrightarrow \exists g (g \in X \land O (g) = P)$
71	69 70	sylibr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land (s \in SubGrp (G) \land \|s\| = P)) \to \exists g \in X O (g) = P$
72	71	expr	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land s \in SubGrp (G)) \to (\|s\| = P \to \exists g \in X O (g) = P)$
73	16 72	sylbid	$⊢ (((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \land s \in SubGrp (G)) \to (\|s\| = P^{1} \to \exists g \in X O (g) = P)$
74	73	rexlimdva	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to (\exists s \in SubGrp (G) \|s\| = P^{1} \to \exists g \in X O (g) = P)$
75	14 74	mpd	$⊢ ((G \in Grp \land X \in Fin \land P \in ℙ) \land P ∥ \|X\|) \to \exists g \in X O (g) = P$

Metamath Proof Explorer

Theorem odcau

Proof