pgpfi1

Description: A finite group with order a power of a prime P is a P -group. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Hypothesis	pgpfi1.1	$⊢ X = {Base}_{G}$
	Assertion	pgpfi1	$⊢ (G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \to (\|X\| = P^{N} \to P pGrp G)$

Proof

Step	Hyp	Ref	Expression
1		pgpfi1.1	$⊢ X = {Base}_{G}$
2		simpl2	$⊢ ((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \to P \in ℙ$
3		simpl1	$⊢ ((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \to G \in Grp$
4		simpll3	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to N \in ℕ_{0}$
5	3	adantr	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to G \in Grp$
6		simplr	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to \|X\| = P^{N}$
7	2	adantr	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to P \in ℙ$
8		prmnn	$⊢ P \in ℙ \to P \in ℕ$
9	7 8	syl	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to P \in ℕ$
10	9 4	nnexpcld	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to P^{N} \in ℕ$
11	10	nnnn0d	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to P^{N} \in ℕ_{0}$
12	6 11	eqeltrd	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to \|X\| \in ℕ_{0}$
13	1	fvexi	$⊢ X \in V$
14		hashclb	$⊢ X \in V \to (X \in Fin \leftrightarrow \|X\| \in ℕ_{0})$
15	13 14	ax-mp	$⊢ X \in Fin \leftrightarrow \|X\| \in ℕ_{0}$
16	12 15	sylibr	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to X \in Fin$
17		simpr	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to x \in X$
18		eqid	$⊢ od (G) = od (G)$
19	1 18	oddvds2	$⊢ (G \in Grp \land X \in Fin \land x \in X) \to od (G) (x) ∥ \|X\|$
20	5 16 17 19	syl3anc	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to od (G) (x) ∥ \|X\|$
21	20 6	breqtrd	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to od (G) (x) ∥ P^{N}$
22		oveq2	$⊢ n = N \to P^{n} = P^{N}$
23	22	breq2d	$⊢ n = N \to (od (G) (x) ∥ P^{n} \leftrightarrow od (G) (x) ∥ P^{N})$
24	23	rspcev	$⊢ (N \in ℕ_{0} \land od (G) (x) ∥ P^{N}) \to \exists n \in ℕ_{0} od (G) (x) ∥ P^{n}$
25	4 21 24	syl2anc	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to \exists n \in ℕ_{0} od (G) (x) ∥ P^{n}$
26	1 18	odcl2	$⊢ (G \in Grp \land X \in Fin \land x \in X) \to od (G) (x) \in ℕ$
27	5 16 17 26	syl3anc	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to od (G) (x) \in ℕ$
28		pcprmpw2	$⊢ (P \in ℙ \land od (G) (x) \in ℕ) \to (\exists n \in ℕ_{0} od (G) (x) ∥ P^{n} \leftrightarrow od (G) (x) = P^{P pCnt od (G) (x)})$
29		pcprmpw	$⊢ (P \in ℙ \land od (G) (x) \in ℕ) \to (\exists n \in ℕ_{0} od (G) (x) = P^{n} \leftrightarrow od (G) (x) = P^{P pCnt od (G) (x)})$
30	28 29	bitr4d	$⊢ (P \in ℙ \land od (G) (x) \in ℕ) \to (\exists n \in ℕ_{0} od (G) (x) ∥ P^{n} \leftrightarrow \exists n \in ℕ_{0} od (G) (x) = P^{n})$
31	7 27 30	syl2anc	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to (\exists n \in ℕ_{0} od (G) (x) ∥ P^{n} \leftrightarrow \exists n \in ℕ_{0} od (G) (x) = P^{n})$
32	25 31	mpbid	$⊢ (((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \land x \in X) \to \exists n \in ℕ_{0} od (G) (x) = P^{n}$
33	32	ralrimiva	$⊢ ((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \to \forall x \in X \exists n \in ℕ_{0} od (G) (x) = P^{n}$
34	1 18	ispgp	$⊢ P pGrp G \leftrightarrow (P \in ℙ \land G \in Grp \land \forall x \in X \exists n \in ℕ_{0} od (G) (x) = P^{n})$
35	2 3 33 34	syl3anbrc	$⊢ ((G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \land \|X\| = P^{N}) \to P pGrp G$
36	35	ex	$⊢ (G \in Grp \land P \in ℙ \land N \in ℕ_{0}) \to (\|X\| = P^{N} \to P pGrp G)$

Metamath Proof Explorer

Theorem pgpfi1

Proof