| Step | Hyp | Ref
| Expression |
| 1 | | pgpfi.1 |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
| 2 | | eqid 2737 |
. . . 4
⊢
(od‘𝐺) =
(od‘𝐺) |
| 3 | 1, 2 | ispgp 19610 |
. . 3
⊢ (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) |
| 4 | | simprl 771 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑃 ∈ ℙ) |
| 5 | 1 | grpbn0 18984 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
| 6 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑋 ≠ ∅) |
| 7 | | hashnncl 14405 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
((♯‘𝑋) ∈
ℕ ↔ 𝑋 ≠
∅)) |
| 8 | 7 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
| 9 | 6, 8 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (♯‘𝑋) ∈ ℕ) |
| 10 | 4, 9 | pccld 16888 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) |
| 11 | 10 | nn0red 12588 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (♯‘𝑋)) ∈ ℝ) |
| 12 | 11 | leidd 11829 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (♯‘𝑋)) ≤ (𝑃 pCnt (♯‘𝑋))) |
| 13 | 10 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (♯‘𝑋)) ∈ ℤ) |
| 14 | | pcid 16911 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 pCnt (♯‘𝑋)) ∈ ℤ) → (𝑃 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋)))) = (𝑃 pCnt (♯‘𝑋))) |
| 15 | 4, 13, 14 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋)))) = (𝑃 pCnt (♯‘𝑋))) |
| 16 | 12, 15 | breqtrrd 5171 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (♯‘𝑋)) ≤ (𝑃 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 17 | 16 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑃 pCnt (♯‘𝑋)) ≤ (𝑃 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 18 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
| 19 | 18 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt (♯‘𝑋)) = (𝑃 pCnt (♯‘𝑋))) |
| 20 | 18 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋)))) = (𝑃 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 21 | 17, 19, 20 | 3brtr4d 5175 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt (♯‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 22 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) → 𝐺 ∈ Grp) |
| 23 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑋 ∈ Fin) |
| 24 | 23 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) → 𝑋 ∈ Fin) |
| 25 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) → 𝑝 ∈ ℙ) |
| 26 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) → 𝑝 ∥ (♯‘𝑋)) |
| 27 | 1, 2 | odcau 19622 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) → ∃𝑔 ∈ 𝑋 ((od‘𝐺)‘𝑔) = 𝑝) |
| 28 | 22, 24, 25, 26, 27 | syl31anc 1375 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) → ∃𝑔 ∈ 𝑋 ((od‘𝐺)‘𝑔) = 𝑝) |
| 29 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∈ ℙ) |
| 30 | | prmz 16712 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
| 31 | | iddvds 16307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℤ → 𝑝 ∥ 𝑝) |
| 32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∥ 𝑝) |
| 33 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ((od‘𝐺)‘𝑔) = 𝑝) |
| 34 | 32, 33 | breqtrrd 5171 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∥ ((od‘𝐺)‘𝑔)) |
| 35 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚)) |
| 36 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑔 → (((od‘𝐺)‘𝑥) = (𝑃↑𝑚) ↔ ((od‘𝐺)‘𝑔) = (𝑃↑𝑚))) |
| 37 | 36 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑔 → (∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚) ↔ ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚))) |
| 38 | 37 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑥 ∈
𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚) ∧ 𝑔 ∈ 𝑋) → ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚)) |
| 39 | 35, 38 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑔 ∈ 𝑋) → ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚)) |
| 40 | 39 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚)) |
| 41 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑃 ∈ ℙ) |
| 42 | | prmnn 16711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 43 | 29, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∈ ℕ) |
| 44 | 33, 43 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ((od‘𝐺)‘𝑔) ∈ ℕ) |
| 45 | | pcprmpw 16921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧
((od‘𝐺)‘𝑔) ∈ ℕ) →
(∃𝑚 ∈
ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚) ↔ ((od‘𝐺)‘𝑔) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))))) |
| 46 | 41, 44, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → (∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚) ↔ ((od‘𝐺)‘𝑔) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))))) |
| 47 | 40, 46 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ((od‘𝐺)‘𝑔) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔)))) |
| 48 | 34, 47 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∥ (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔)))) |
| 49 | 41, 44 | pccld 16888 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → (𝑃 pCnt ((od‘𝐺)‘𝑔)) ∈
ℕ0) |
| 50 | | prmdvdsexpr 16754 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ (𝑃 pCnt ((od‘𝐺)‘𝑔)) ∈ ℕ0) → (𝑝 ∥ (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))) → 𝑝 = 𝑃)) |
| 51 | 29, 41, 49, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → (𝑝 ∥ (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))) → 𝑝 = 𝑃)) |
| 52 | 48, 51 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 = 𝑃) |
| 53 | 28, 52 | rexlimddv 3161 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝑋)) → 𝑝 = 𝑃) |
| 54 | 53 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (♯‘𝑋) → 𝑝 = 𝑃)) |
| 55 | 54 | necon3ad 2953 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → (𝑝 ≠ 𝑃 → ¬ 𝑝 ∥ (♯‘𝑋))) |
| 56 | 55 | imp 406 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → ¬ 𝑝 ∥ (♯‘𝑋)) |
| 57 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → 𝑝 ∈ ℙ) |
| 58 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (♯‘𝑋) ∈ ℕ) |
| 59 | | pceq0 16909 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧
(♯‘𝑋) ∈
ℕ) → ((𝑝 pCnt
(♯‘𝑋)) = 0
↔ ¬ 𝑝 ∥
(♯‘𝑋))) |
| 60 | 57, 58, 59 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → ((𝑝 pCnt (♯‘𝑋)) = 0 ↔ ¬ 𝑝 ∥ (♯‘𝑋))) |
| 61 | 56, 60 | mpbird 257 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt (♯‘𝑋)) = 0) |
| 62 | | prmnn 16711 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 63 | 62 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑃 ∈ ℕ) |
| 64 | 63, 10 | nnexpcld 14284 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃↑(𝑃 pCnt (♯‘𝑋))) ∈ ℕ) |
| 65 | 64 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑃↑(𝑃 pCnt (♯‘𝑋))) ∈ ℕ) |
| 66 | 57, 65 | pccld 16888 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋)))) ∈
ℕ0) |
| 67 | 66 | nn0ge0d 12590 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → 0 ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 68 | 61, 67 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt (♯‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 69 | 21, 68 | pm2.61dane 3029 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (♯‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 70 | 69 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ∀𝑝 ∈ ℙ (𝑝 pCnt (♯‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 71 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ Fin →
(♯‘𝑋) ∈
ℕ0) |
| 72 | 71 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (♯‘𝑋) ∈
ℕ0) |
| 73 | 72 | nn0zd 12639 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (♯‘𝑋) ∈ ℤ) |
| 74 | 64 | nnzd 12640 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃↑(𝑃 pCnt (♯‘𝑋))) ∈ ℤ) |
| 75 | | pc2dvds 16917 |
. . . . . . . . . 10
⊢
(((♯‘𝑋)
∈ ℤ ∧ (𝑃↑(𝑃 pCnt (♯‘𝑋))) ∈ ℤ) →
((♯‘𝑋) ∥
(𝑃↑(𝑃 pCnt (♯‘𝑋))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (♯‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋)))))) |
| 76 | 73, 74, 75 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ((♯‘𝑋) ∥ (𝑃↑(𝑃 pCnt (♯‘𝑋))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (♯‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (♯‘𝑋)))))) |
| 77 | 70, 76 | mpbird 257 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (♯‘𝑋) ∥ (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 78 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑃 pCnt (♯‘𝑋)) → (𝑃↑𝑛) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 79 | 78 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑛 = (𝑃 pCnt (♯‘𝑋)) → ((♯‘𝑋) ∥ (𝑃↑𝑛) ↔ (♯‘𝑋) ∥ (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 80 | 79 | rspcev 3622 |
. . . . . . . 8
⊢ (((𝑃 pCnt (♯‘𝑋)) ∈ ℕ0
∧ (♯‘𝑋)
∥ (𝑃↑(𝑃 pCnt (♯‘𝑋)))) → ∃𝑛 ∈ ℕ0
(♯‘𝑋) ∥
(𝑃↑𝑛)) |
| 81 | 10, 77, 80 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ∃𝑛 ∈ ℕ0
(♯‘𝑋) ∥
(𝑃↑𝑛)) |
| 82 | | pcprmpw2 16920 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑋) ∈
ℕ) → (∃𝑛
∈ ℕ0 (♯‘𝑋) ∥ (𝑃↑𝑛) ↔ (♯‘𝑋) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 83 | | pcprmpw 16921 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑋) ∈
ℕ) → (∃𝑛
∈ ℕ0 (♯‘𝑋) = (𝑃↑𝑛) ↔ (♯‘𝑋) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 84 | 82, 83 | bitr4d 282 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑋) ∈
ℕ) → (∃𝑛
∈ ℕ0 (♯‘𝑋) ∥ (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛))) |
| 85 | 4, 9, 84 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (∃𝑛 ∈ ℕ0
(♯‘𝑋) ∥
(𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛))) |
| 86 | 81, 85 | mpbid 232 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)) |
| 87 | 4, 86 | jca 511 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛))) |
| 88 | 87 | 3adantr2 1171 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛))) |
| 89 | 88 | ex 412 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → ((𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚)) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)))) |
| 90 | 3, 89 | biimtrid 242 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)))) |
| 91 | 1 | pgpfi1 19613 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
→ ((♯‘𝑋) =
(𝑃↑𝑛) → 𝑃 pGrp 𝐺)) |
| 92 | 91 | 3expia 1122 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ) → (𝑛 ∈ ℕ0
→ ((♯‘𝑋) =
(𝑃↑𝑛) → 𝑃 pGrp 𝐺))) |
| 93 | 92 | rexlimdv 3153 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ) →
(∃𝑛 ∈
ℕ0 (♯‘𝑋) = (𝑃↑𝑛) → 𝑃 pGrp 𝐺)) |
| 94 | 93 | expimpd 453 |
. . 3
⊢ (𝐺 ∈ Grp → ((𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (♯‘𝑋) = (𝑃↑𝑛)) → 𝑃 pGrp 𝐺)) |
| 95 | 94 | adantr 480 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → ((𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (♯‘𝑋) = (𝑃↑𝑛)) → 𝑃 pGrp 𝐺)) |
| 96 | 90, 95 | impbid 212 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)))) |