Step | Hyp | Ref
| Expression |
1 | | pgpfi.1 |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
2 | | eqid 2610 |
. . . 4
⊢
(od‘𝐺) =
(od‘𝐺) |
3 | 1, 2 | ispgp 17830 |
. . 3
⊢ (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) |
4 | | simprl 790 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑃 ∈ ℙ) |
5 | 1 | grpbn0 17274 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
6 | 5 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑋 ≠ ∅) |
7 | | hashnncl 13018 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
8 | 7 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
9 | 6, 8 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (#‘𝑋) ∈ ℕ) |
10 | 4, 9 | pccld 15393 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (#‘𝑋)) ∈
ℕ0) |
11 | 10 | nn0red 11229 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (#‘𝑋)) ∈ ℝ) |
12 | 11 | leidd 10473 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (#‘𝑋)) ≤ (𝑃 pCnt (#‘𝑋))) |
13 | 10 | nn0zd 11356 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (#‘𝑋)) ∈ ℤ) |
14 | | pcid 15415 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 pCnt (#‘𝑋)) ∈ ℤ) → (𝑃 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋)))) = (𝑃 pCnt (#‘𝑋))) |
15 | 4, 13, 14 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋)))) = (𝑃 pCnt (#‘𝑋))) |
16 | 12, 15 | breqtrrd 4611 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 pCnt (#‘𝑋)) ≤ (𝑃 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
17 | 16 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑃 pCnt (#‘𝑋)) ≤ (𝑃 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
18 | | simpr 476 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
19 | 18 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt (#‘𝑋)) = (𝑃 pCnt (#‘𝑋))) |
20 | 18 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋)))) = (𝑃 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
21 | 17, 19, 20 | 3brtr4d 4615 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt (#‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
22 | | simp-4l 802 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) → 𝐺 ∈ Grp) |
23 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑋 ∈ Fin) |
24 | 23 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) → 𝑋 ∈ Fin) |
25 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) → 𝑝 ∈ ℙ) |
26 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) → 𝑝 ∥ (#‘𝑋)) |
27 | 1, 2 | odcau 17842 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) → ∃𝑔 ∈ 𝑋 ((od‘𝐺)‘𝑔) = 𝑝) |
28 | 22, 24, 25, 26, 27 | syl31anc 1321 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) → ∃𝑔 ∈ 𝑋 ((od‘𝐺)‘𝑔) = 𝑝) |
29 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∈ ℙ) |
30 | | prmz 15227 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
31 | | iddvds 14833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℤ → 𝑝 ∥ 𝑝) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∥ 𝑝) |
33 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ((od‘𝐺)‘𝑔) = 𝑝) |
34 | 32, 33 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∥ ((od‘𝐺)‘𝑔)) |
35 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚)) |
36 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑔 → ((od‘𝐺)‘𝑥) = ((od‘𝐺)‘𝑔)) |
37 | 36 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑔 → (((od‘𝐺)‘𝑥) = (𝑃↑𝑚) ↔ ((od‘𝐺)‘𝑔) = (𝑃↑𝑚))) |
38 | 37 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑔 → (∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚) ↔ ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚))) |
39 | 38 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑥 ∈
𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚) ∧ 𝑔 ∈ 𝑋) → ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚)) |
40 | 35, 39 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑔 ∈ 𝑋) → ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚)) |
41 | 40 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚)) |
42 | 4 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑃 ∈ ℙ) |
43 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
44 | 29, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∈ ℕ) |
45 | 33, 44 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ((od‘𝐺)‘𝑔) ∈ ℕ) |
46 | | pcprmpw 15425 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℙ ∧
((od‘𝐺)‘𝑔) ∈ ℕ) →
(∃𝑚 ∈
ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚) ↔ ((od‘𝐺)‘𝑔) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))))) |
47 | 42, 45, 46 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → (∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑔) = (𝑃↑𝑚) ↔ ((od‘𝐺)‘𝑔) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))))) |
48 | 41, 47 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → ((od‘𝐺)‘𝑔) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔)))) |
49 | 34, 48 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 ∥ (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔)))) |
50 | 42, 45 | pccld 15393 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → (𝑃 pCnt ((od‘𝐺)‘𝑔)) ∈
ℕ0) |
51 | | prmdvdsexpr 15267 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ (𝑃 pCnt ((od‘𝐺)‘𝑔)) ∈ ℕ0) → (𝑝 ∥ (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))) → 𝑝 = 𝑃)) |
52 | 29, 42, 50, 51 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → (𝑝 ∥ (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑔))) → 𝑝 = 𝑃)) |
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) ∧ (𝑔 ∈ 𝑋 ∧ ((od‘𝐺)‘𝑔) = 𝑝)) → 𝑝 = 𝑃) |
54 | 28, 53 | rexlimddv 3017 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (#‘𝑋)) → 𝑝 = 𝑃) |
55 | 54 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (#‘𝑋) → 𝑝 = 𝑃)) |
56 | 55 | necon3ad 2795 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → (𝑝 ≠ 𝑃 → ¬ 𝑝 ∥ (#‘𝑋))) |
57 | 56 | imp 444 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → ¬ 𝑝 ∥ (#‘𝑋)) |
58 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → 𝑝 ∈ ℙ) |
59 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (#‘𝑋) ∈ ℕ) |
60 | | pceq0 15413 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧
(#‘𝑋) ∈ ℕ)
→ ((𝑝 pCnt
(#‘𝑋)) = 0 ↔
¬ 𝑝 ∥
(#‘𝑋))) |
61 | 58, 59, 60 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → ((𝑝 pCnt (#‘𝑋)) = 0 ↔ ¬ 𝑝 ∥ (#‘𝑋))) |
62 | 57, 61 | mpbird 246 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt (#‘𝑋)) = 0) |
63 | | prmnn 15226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
64 | 63 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → 𝑃 ∈ ℕ) |
65 | 64, 10 | nnexpcld 12892 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃↑(𝑃 pCnt (#‘𝑋))) ∈ ℕ) |
66 | 65 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑃↑(𝑃 pCnt (#‘𝑋))) ∈ ℕ) |
67 | 58, 66 | pccld 15393 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋)))) ∈
ℕ0) |
68 | 67 | nn0ge0d 11231 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → 0 ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
69 | 62, 68 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ Grp
∧ 𝑋 ∈ Fin) ∧
(𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt (#‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
70 | 21, 69 | pm2.61dane 2869 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (#‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
71 | 70 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ∀𝑝 ∈ ℙ (𝑝 pCnt (#‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
72 | | hashcl 13009 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ Fin →
(#‘𝑋) ∈
ℕ0) |
73 | 72 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (#‘𝑋) ∈
ℕ0) |
74 | 73 | nn0zd 11356 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (#‘𝑋) ∈ ℤ) |
75 | 65 | nnzd 11357 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃↑(𝑃 pCnt (#‘𝑋))) ∈ ℤ) |
76 | | pc2dvds 15421 |
. . . . . . . . . 10
⊢
(((#‘𝑋) ∈
ℤ ∧ (𝑃↑(𝑃 pCnt (#‘𝑋))) ∈ ℤ) → ((#‘𝑋) ∥ (𝑃↑(𝑃 pCnt (#‘𝑋))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (#‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋)))))) |
77 | 74, 75, 76 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ((#‘𝑋) ∥ (𝑃↑(𝑃 pCnt (#‘𝑋))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (#‘𝑋)) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt (#‘𝑋)))))) |
78 | 71, 77 | mpbird 246 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (#‘𝑋) ∥ (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
79 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑃 pCnt (#‘𝑋)) → (𝑃↑𝑛) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
80 | 79 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑛 = (𝑃 pCnt (#‘𝑋)) → ((#‘𝑋) ∥ (𝑃↑𝑛) ↔ (#‘𝑋) ∥ (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
81 | 80 | rspcev 3282 |
. . . . . . . 8
⊢ (((𝑃 pCnt (#‘𝑋)) ∈ ℕ0 ∧
(#‘𝑋) ∥ (𝑃↑(𝑃 pCnt (#‘𝑋)))) → ∃𝑛 ∈ ℕ0 (#‘𝑋) ∥ (𝑃↑𝑛)) |
82 | 10, 78, 81 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ∃𝑛 ∈ ℕ0 (#‘𝑋) ∥ (𝑃↑𝑛)) |
83 | | pcprmpw2 15424 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝑋) ∈ ℕ)
→ (∃𝑛 ∈
ℕ0 (#‘𝑋) ∥ (𝑃↑𝑛) ↔ (#‘𝑋) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
84 | | pcprmpw 15425 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝑋) ∈ ℕ)
→ (∃𝑛 ∈
ℕ0 (#‘𝑋) = (𝑃↑𝑛) ↔ (#‘𝑋) = (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
85 | 83, 84 | bitr4d 270 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝑋) ∈ ℕ)
→ (∃𝑛 ∈
ℕ0 (#‘𝑋) ∥ (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0 (#‘𝑋) = (𝑃↑𝑛))) |
86 | 4, 9, 85 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (∃𝑛 ∈ ℕ0 (#‘𝑋) ∥ (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0 (#‘𝑋) = (𝑃↑𝑛))) |
87 | 82, 86 | mpbid 221 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → ∃𝑛 ∈ ℕ0 (#‘𝑋) = (𝑃↑𝑛)) |
88 | 4, 87 | jca 553 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧
∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(#‘𝑋) = (𝑃↑𝑛))) |
89 | 88 | 3adantr2 1214 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚))) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(#‘𝑋) = (𝑃↑𝑛))) |
90 | 89 | ex 449 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → ((𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑚 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑚)) → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(#‘𝑋) = (𝑃↑𝑛)))) |
91 | 3, 90 | syl5bi 231 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(#‘𝑋) = (𝑃↑𝑛)))) |
92 | 1 | pgpfi1 17833 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
→ ((#‘𝑋) =
(𝑃↑𝑛) → 𝑃 pGrp 𝐺)) |
93 | 92 | 3expia 1259 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ) → (𝑛 ∈ ℕ0
→ ((#‘𝑋) =
(𝑃↑𝑛) → 𝑃 pGrp 𝐺))) |
94 | 93 | rexlimdv 3012 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ) →
(∃𝑛 ∈
ℕ0 (#‘𝑋) = (𝑃↑𝑛) → 𝑃 pGrp 𝐺)) |
95 | 94 | expimpd 627 |
. . 3
⊢ (𝐺 ∈ Grp → ((𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (#‘𝑋) = (𝑃↑𝑛)) → 𝑃 pGrp 𝐺)) |
96 | 95 | adantr 480 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → ((𝑃 ∈ ℙ ∧
∃𝑛 ∈
ℕ0 (#‘𝑋) = (𝑃↑𝑛)) → 𝑃 pGrp 𝐺)) |
97 | 91, 96 | impbid 201 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(#‘𝑋) = (𝑃↑𝑛)))) |