Step | Hyp | Ref
| Expression |
1 | | simpl2 1065 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) → 𝑃 ∈ ℙ) |
2 | | simpl1 1064 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) → 𝐺 ∈ Grp) |
3 | | simpll3 1102 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → 𝑁 ∈
ℕ0) |
4 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → 𝐺 ∈ Grp) |
5 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → (#‘𝑋) = (𝑃↑𝑁)) |
6 | 1 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → 𝑃 ∈ ℙ) |
7 | | prmnn 15388 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → 𝑃 ∈ ℕ) |
9 | 8, 3 | nnexpcld 13030 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → (𝑃↑𝑁) ∈ ℕ) |
10 | 9 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → (𝑃↑𝑁) ∈
ℕ0) |
11 | 5, 10 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → (#‘𝑋) ∈
ℕ0) |
12 | | pgpfi1.1 |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
13 | | fvex 6201 |
. . . . . . . . . . 11
⊢
(Base‘𝐺)
∈ V |
14 | 12, 13 | eqeltri 2697 |
. . . . . . . . . 10
⊢ 𝑋 ∈ V |
15 | | hashclb 13149 |
. . . . . . . . . 10
⊢ (𝑋 ∈ V → (𝑋 ∈ Fin ↔
(#‘𝑋) ∈
ℕ0)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑋 ∈ Fin ↔
(#‘𝑋) ∈
ℕ0) |
17 | 11, 16 | sylibr 224 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ Fin) |
18 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
19 | | eqid 2622 |
. . . . . . . . 9
⊢
(od‘𝐺) =
(od‘𝐺) |
20 | 12, 19 | oddvds2 17983 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋) → ((od‘𝐺)‘𝑥) ∥ (#‘𝑋)) |
21 | 4, 17, 18, 20 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → ((od‘𝐺)‘𝑥) ∥ (#‘𝑋)) |
22 | 21, 5 | breqtrd 4679 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑁)) |
23 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑃↑𝑛) = (𝑃↑𝑁)) |
24 | 23 | breq2d 4665 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑁))) |
25 | 24 | rspcev 3309 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑁)) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑛)) |
26 | 3, 22, 25 | syl2anc 693 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑛)) |
27 | 12, 19 | odcl2 17982 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋) → ((od‘𝐺)‘𝑥) ∈ ℕ) |
28 | 4, 17, 18, 27 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → ((od‘𝐺)‘𝑥) ∈ ℕ) |
29 | | pcprmpw2 15586 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧
((od‘𝐺)‘𝑥) ∈ ℕ) →
(∃𝑛 ∈
ℕ0 ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑥))))) |
30 | | pcprmpw 15587 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧
((od‘𝐺)‘𝑥) ∈ ℕ) →
(∃𝑛 ∈
ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (𝑃↑(𝑃 pCnt ((od‘𝐺)‘𝑥))))) |
31 | 29, 30 | bitr4d 271 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
((od‘𝐺)‘𝑥) ∈ ℕ) →
(∃𝑛 ∈
ℕ0 ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑛))) |
32 | 6, 28, 31 | syl2anc 693 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → (∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑛))) |
33 | 26, 32 | mpbid 222 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) ∧ 𝑥 ∈ 𝑋) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑛)) |
34 | 33 | ralrimiva 2966 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) → ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑛)) |
35 | 12, 19 | ispgp 18007 |
. . 3
⊢ (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) = (𝑃↑𝑛))) |
36 | 1, 2, 34, 35 | syl3anbrc 1246 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ (#‘𝑋) = (𝑃↑𝑁)) → 𝑃 pGrp 𝐺) |
37 | 36 | ex 450 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ ((#‘𝑋) =
(𝑃↑𝑁) → 𝑃 pGrp 𝐺)) |