Metamath Proof Explorer

Theorem pgpfi

Description: The converse to pgpfi1 . A finite group is a P -group iff it has size some power of P . (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis pgpfi.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion pgpfi ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 pgpfi.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
3 1 2 ispgp ⊢ ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) )
4 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → 𝑃 ∈ ℙ )
5 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
6 5 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → 𝑋 ≠ ∅ )
7 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
8 7 ad2antlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
9 6 8 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
10 4 9 pccld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 )
11 10 nn0red ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℝ )
12 11 leidd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) )
13 10 nn0zd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℤ )
14 pcid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) )
15 4 13 14 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) )
16 12 15 breqtrrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
17 16 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
18 simpr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
19 18 oveq1d ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) )
20 18 oveq1d ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) = ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
21 17 19 20 3brtr4d ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 = 𝑃 ) → ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
22 simp-4l ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) → 𝐺 ∈ Grp )
23 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → 𝑋 ∈ Fin )
24 23 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑋 ∈ Fin )
25 simplr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑝 ∈ ℙ )
26 simpr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑝 ∥ ( ♯ ‘ 𝑋 ) )
27 1 2 odcau ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) → ∃ 𝑔 ∈ 𝑋 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 )
28 22 24 25 26 27 syl31anc ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) → ∃ 𝑔 ∈ 𝑋 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 )
29 25 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → 𝑝 ∈ ℙ )
30 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
31 iddvds ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∥ 𝑝 )
32 29 30 31 3syl ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → 𝑝 ∥ 𝑝 )
33 simprr ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 )
34 32 33 breqtrrd ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → 𝑝 ∥ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) )
35 simplrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) )
36 fveqeq2 ⊢ ( 𝑥 = 𝑔 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ 𝑚 ) ) )
37 36 rexbidv ⊢ ( 𝑥 = 𝑔 → ( ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ↔ ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ 𝑚 ) ) )
38 37 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ∧ 𝑔 ∈ 𝑋 ) → ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ 𝑚 ) )
39 35 38 sylan ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑔 ∈ 𝑋 ) → ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ 𝑚 ) )
40 39 ad2ant2r ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ 𝑚 ) )
41 4 ad3antrrr ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → 𝑃 ∈ ℙ )
42 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
43 29 42 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → 𝑝 ∈ ℕ )
44 33 43 eqeltrd ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ∈ ℕ )
45 pcprmpw ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ∈ ℕ ) → ( ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ 𝑚 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ) ) )
46 41 44 45 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → ( ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ 𝑚 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ) ) )
47 40 46 mpbid ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ) )
48 34 47 breqtrd ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → 𝑝 ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ) )
49 41 44 pccld ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ∈ ℕ0 )
50 prmdvdsexpr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ∈ ℕ0 ) → ( 𝑝 ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ) → 𝑝 = 𝑃 ) )
51 29 41 49 50 syl3anc ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → ( 𝑝 ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑔 ) ) ) → 𝑝 = 𝑃 ) )
52 48 51 mpd ⊢ ( ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑔 ) = 𝑝 ) ) → 𝑝 = 𝑃 )
53 28 52 rexlimddv ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑝 = 𝑃 )
54 53 ex ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ♯ ‘ 𝑋 ) → 𝑝 = 𝑃 ) )
55 54 necon3ad ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≠ 𝑃 → ¬ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) )
56 55 imp ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ¬ 𝑝 ∥ ( ♯ ‘ 𝑋 ) )
57 simplr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → 𝑝 ∈ ℙ )
58 9 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
59 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) = 0 ↔ ¬ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) )
60 57 58 59 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) = 0 ↔ ¬ 𝑝 ∥ ( ♯ ‘ 𝑋 ) ) )
61 56 60 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) = 0 )
62 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
63 62 ad2antrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → 𝑃 ∈ ℕ )
64 63 10 nnexpcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ∈ ℕ )
65 64 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ∈ ℕ )
66 57 65 pccld ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℕ0 )
67 66 nn0ge0d ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → 0 ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
68 61 67 eqbrtrd ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 𝑃 ) → ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
69 21 68 pm2.61dane ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
70 69 ralrimiva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
71 hashcl ⊢ ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
72 71 ad2antlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
73 72 nn0zd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( ♯ ‘ 𝑋 ) ∈ ℤ )
74 64 nnzd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ∈ ℤ )
75 pc2dvds ⊢ ( ( ( ♯ ‘ 𝑋 ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ∈ ℤ ) → ( ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) )
76 73 74 75 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ♯ ‘ 𝑋 ) ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) )
77 70 76 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
78 oveq2 ⊢ ( 𝑛 = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
79 78 breq2d ⊢ ( 𝑛 = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) → ( ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
80 79 rspcev ⊢ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ 𝑛 ) )
81 10 77 80 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ 𝑛 ) )
82 pcprmpw2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
83 pcprmpw ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
84 82 83 bitr4d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) )
85 4 9 84 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) )
86 81 85 mpbid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) )
87 4 86 jca ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) )
88 87 3adantr2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) ) → ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) )
89 88 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑚 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑚 ) ) → ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ) )
90 3 89 syl5bi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝑃 pGrp 𝐺 → ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ) )
91 1 pgpfi1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) → 𝑃 pGrp 𝐺 ) )
92 91 3expia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → ( 𝑛 ∈ ℕ0 → ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) → 𝑃 pGrp 𝐺 ) ) )
93 92 rexlimdv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) → 𝑃 pGrp 𝐺 ) )
94 93 expimpd ⊢ ( 𝐺 ∈ Grp → ( ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) → 𝑃 pGrp 𝐺 ) )
95 94 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) → 𝑃 pGrp 𝐺 ) )
96 90 95 impbid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ) )