Step |
Hyp |
Ref |
Expression |
1 |
|
ablfac1.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
ablfac1.o |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
3 |
|
ablfac1.s |
⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) |
4 |
|
ablfac1.g |
⊢ ( 𝜑 → 𝐺 ∈ Abel ) |
5 |
|
ablfac1.f |
⊢ ( 𝜑 → 𝐵 ∈ Fin ) |
6 |
|
ablfac1.1 |
⊢ ( 𝜑 → 𝐴 ⊆ ℙ ) |
7 |
|
ablfac1.m |
⊢ 𝑀 = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) |
8 |
|
ablfac1.n |
⊢ 𝑁 = ( ( ♯ ‘ 𝐵 ) / 𝑀 ) |
9 |
6
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ ℙ ) |
10 |
|
prmnn |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
11 |
9 10
|
syl |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ ℕ ) |
12 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
13 |
1
|
grpbn0 |
⊢ ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ ) |
14 |
4 12 13
|
3syl |
⊢ ( 𝜑 → 𝐵 ≠ ∅ ) |
15 |
|
hashnncl |
⊢ ( 𝐵 ∈ Fin → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) ) |
16 |
5 15
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) ) |
17 |
14 16
|
mpbird |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ ) |
18 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ ) |
19 |
9 18
|
pccld |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) |
20 |
11 19
|
nnexpcld |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ ) |
21 |
7 20
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑀 ∈ ℕ ) |
22 |
|
pcdvds |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
23 |
9 18 22
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
24 |
7 23
|
eqbrtrid |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑀 ∥ ( ♯ ‘ 𝐵 ) ) |
25 |
|
nndivdvds |
⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝑀 ) ∈ ℕ ) ) |
26 |
18 21 25
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝑀 ) ∈ ℕ ) ) |
27 |
24 26
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) / 𝑀 ) ∈ ℕ ) |
28 |
8 27
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑁 ∈ ℕ ) |
29 |
21 28
|
jca |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) |
30 |
7
|
oveq1i |
⊢ ( 𝑀 gcd 𝑁 ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd 𝑁 ) |
31 |
|
pcndvds2 |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ¬ 𝑃 ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) |
32 |
9 18 31
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑃 ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) |
33 |
7
|
oveq2i |
⊢ ( ( ♯ ‘ 𝐵 ) / 𝑀 ) = ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
34 |
8 33
|
eqtri |
⊢ 𝑁 = ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
35 |
34
|
breq2i |
⊢ ( 𝑃 ∥ 𝑁 ↔ 𝑃 ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) |
36 |
32 35
|
sylnibr |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ¬ 𝑃 ∥ 𝑁 ) |
37 |
28
|
nnzd |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑁 ∈ ℤ ) |
38 |
|
coprm |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑁 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) ) |
39 |
9 37 38
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ∥ 𝑁 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) ) |
40 |
36 39
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 gcd 𝑁 ) = 1 ) |
41 |
|
prmz |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) |
42 |
9 41
|
syl |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ ℤ ) |
43 |
|
rpexp1i |
⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) → ( ( 𝑃 gcd 𝑁 ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd 𝑁 ) = 1 ) ) |
44 |
42 37 19 43
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑃 gcd 𝑁 ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd 𝑁 ) = 1 ) ) |
45 |
40 44
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd 𝑁 ) = 1 ) |
46 |
30 45
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 gcd 𝑁 ) = 1 ) |
47 |
8
|
oveq2i |
⊢ ( 𝑀 · 𝑁 ) = ( 𝑀 · ( ( ♯ ‘ 𝐵 ) / 𝑀 ) ) |
48 |
18
|
nncnd |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℂ ) |
49 |
21
|
nncnd |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑀 ∈ ℂ ) |
50 |
21
|
nnne0d |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝑀 ≠ 0 ) |
51 |
48 49 50
|
divcan2d |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 · ( ( ♯ ‘ 𝐵 ) / 𝑀 ) ) = ( ♯ ‘ 𝐵 ) ) |
52 |
47 51
|
eqtr2id |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) ) |
53 |
29 46 52
|
3jca |
⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ∧ ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) ) ) |