Metamath Proof Explorer


Theorem ablfac1lem

Description: Lemma for ablfac1b . Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses ablfac1.b 𝐵 = ( Base ‘ 𝐺 )
ablfac1.o 𝑂 = ( od ‘ 𝐺 )
ablfac1.s 𝑆 = ( 𝑝𝐴 ↦ { 𝑥𝐵 ∣ ( 𝑂𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
ablfac1.g ( 𝜑𝐺 ∈ Abel )
ablfac1.f ( 𝜑𝐵 ∈ Fin )
ablfac1.1 ( 𝜑𝐴 ⊆ ℙ )
ablfac1.m 𝑀 = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) )
ablfac1.n 𝑁 = ( ( ♯ ‘ 𝐵 ) / 𝑀 )
Assertion ablfac1lem ( ( 𝜑𝑃𝐴 ) → ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ∧ ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) ) )

Proof

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 ∧ ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) ) )