Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion	pgpfi1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) → 𝑃 pGrp 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		pgpfi1.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		simpl2	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → 𝑃 ∈ ℙ )
3		simpl1	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → 𝐺 ∈ Grp )
4		simpll3	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑁 ∈ ℕ0 )
5	3	adantr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐺 ∈ Grp )
6		simplr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) )
7	2	adantr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ ℙ )
8		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9	7 8	syl	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ ℕ )
10	9 4	nnexpcld	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 ↑ 𝑁 ) ∈ ℕ )
11	10	nnnn0d	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 ↑ 𝑁 ) ∈ ℕ0 )
12	6 11	eqeltrd	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
13	1	fvexi	⊢ 𝑋 ∈ V
14		hashclb	⊢ ( 𝑋 ∈ V → ( 𝑋 ∈ Fin ↔ ( ♯ ‘ 𝑋 ) ∈ ℕ0 ) )
15	13 14	ax-mp	⊢ ( 𝑋 ∈ Fin ↔ ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
16	12 15	sylibr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ Fin )
17		simpr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
18		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
19	1 18	oddvds2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
20	5 16 17 19	syl3anc	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
21	20 6	breqtrd	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑁 ) )
22		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑁 ) )
23	22	breq2d	⊢ ( 𝑛 = 𝑁 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑁 ) ) )
24	23	rspcev	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) )
25	4 21 24	syl2anc	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) )
26	1 18	odcl2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ )
27	5 16 17 26	syl3anc	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ )
28		pcprmpw2	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
29		pcprmpw	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
30	28 29	bitr4d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
31	7 27 30	syl2anc	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
32	25 31	mpbid	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) )
33	32	ralrimiva	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) )
34	1 18	ispgp	⊢ ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
35	2 3 33 34	syl3anbrc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → 𝑃 pGrp 𝐺 )
36	35	ex	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) → 𝑃 pGrp 𝐺 ) )