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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 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 ∧ ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) ) )