Metamath Proof Explorer

Theorem ablfacrplem

Description: Lemma for ablfacrp2 . (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses ablfacrp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfacrp.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfacrp.k ⊢ 𝐾 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 }
ablfacrp.l ⊢ 𝐿 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 }
ablfacrp.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfacrp.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
ablfacrp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ablfacrp.1 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
ablfacrp.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) )
Assertion ablfacrplem ( 𝜑 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 ablfacrp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfacrp.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 ablfacrp.k ⊢ 𝐾 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 }
4 ablfacrp.l ⊢ 𝐿 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 }
5 ablfacrp.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
6 ablfacrp.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 ablfacrp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8 ablfacrp.1 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
9 ablfacrp.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) )
10 nprmdvds1 ⊢ ( 𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1 )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ¬ 𝑝 ∥ 1 )
12 8 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑀 gcd 𝑁 ) = 1 )
13 12 breq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝑀 gcd 𝑁 ) ↔ 𝑝 ∥ 1 ) )
14 11 13 mtbird ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ¬ 𝑝 ∥ ( 𝑀 gcd 𝑁 ) )
15 6 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
16 2 1 oddvdssubg ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∈ ( SubGrp ‘ 𝐺 ) )
17 5 15 16 syl2anc ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∈ ( SubGrp ‘ 𝐺 ) )
18 3 17 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
20 eqid ⊢ ( 𝐺 ↾s 𝐾 ) = ( 𝐺 ↾s 𝐾 )
21 20 subggrp ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝐾 ) ∈ Grp )
22 19 21 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ( 𝐺 ↾s 𝐾 ) ∈ Grp )
23 20 subgbas ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 = ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) )
24 19 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝐾 = ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) )
25 6 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
26 7 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
27 25 26 nn0mulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℕ0 )
28 9 27 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
29 1 fvexi ⊢ 𝐵 ∈ V
30 hashclb ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) )
31 29 30 ax-mp ⊢ ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
32 28 31 sylibr ⊢ ( 𝜑 → 𝐵 ∈ Fin )
33 3 ssrab3 ⊢ 𝐾 ⊆ 𝐵
34 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐾 ⊆ 𝐵 ) → 𝐾 ∈ Fin )
35 32 33 34 sylancl ⊢ ( 𝜑 → 𝐾 ∈ Fin )
36 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝐾 ∈ Fin )
37 24 36 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ∈ Fin )
38 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝑝 ∈ ℙ )
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝑝 ∥ ( ♯ ‘ 𝐾 ) )
40 24 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ( ♯ ‘ 𝐾 ) = ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ) )
41 39 40 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝑝 ∥ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ) )
42 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) = ( Base ‘ ( 𝐺 ↾s 𝐾 ) )
43 eqid ⊢ ( od ‘ ( 𝐺 ↾s 𝐾 ) ) = ( od ‘ ( 𝐺 ↾s 𝐾 ) )
44 42 43 odcau ⊢ ( ( ( ( 𝐺 ↾s 𝐾 ) ∈ Grp ∧ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ∈ Fin ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ) ) → ∃ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 )
45 22 37 38 41 44 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ∃ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 )
46 24 rexeqdv ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ( ∃ 𝑔 ∈ 𝐾 ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 ↔ ∃ 𝑔 ∈ ( Base ‘ ( 𝐺 ↾s 𝐾 ) ) ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 ) )
47 45 46 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ∃ 𝑔 ∈ 𝐾 ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 )
48 20 2 43 subgod ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑂 ‘ 𝑔 ) = ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) )
49 19 48 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑂 ‘ 𝑔 ) = ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) )
50 fveq2 ⊢ ( 𝑥 = 𝑔 → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑔 ) )
51 50 breq1d ⊢ ( 𝑥 = 𝑔 → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ↔ ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 ) )
52 51 3 elrab2 ⊢ ( 𝑔 ∈ 𝐾 ↔ ( 𝑔 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 ) )
53 52 simprbi ⊢ ( 𝑔 ∈ 𝐾 → ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 )
54 53 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 )
55 49 54 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) ∥ 𝑀 )
56 breq1 ⊢ ( ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 → ( ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) ∥ 𝑀 ↔ 𝑝 ∥ 𝑀 ) )
57 55 56 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 → 𝑝 ∥ 𝑀 ) )
58 57 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ( ∃ 𝑔 ∈ 𝐾 ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 → 𝑝 ∥ 𝑀 ) )
59 47 58 mpd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝑝 ∥ 𝑀 )
60 59 ex ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) → 𝑝 ∥ 𝑀 ) )
61 60 anim1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) ∧ 𝑝 ∥ 𝑁 ) → ( 𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁 ) ) )
62 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
63 62 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
64 hashcl ⊢ ( 𝐾 ∈ Fin → ( ♯ ‘ 𝐾 ) ∈ ℕ0 )
65 35 64 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℕ0 )
66 65 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℤ )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ♯ ‘ 𝐾 ) ∈ ℤ )
68 7 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℤ )
70 dvdsgcdb ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ) )
71 63 67 69 70 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ) )
72 15 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑀 ∈ ℤ )
73 dvdsgcdb ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( 𝑀 gcd 𝑁 ) ) )
74 63 72 69 73 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( 𝑀 gcd 𝑁 ) ) )
75 61 71 74 3imtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) → 𝑝 ∥ ( 𝑀 gcd 𝑁 ) ) )
76 14 75 mtod ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ¬ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) )
77 76 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) )
78 exprmfct ⊢ ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) )
79 77 78 nsyl ⊢ ( 𝜑 → ¬ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) )
80 7 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
81 simpr ⊢ ( ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
82 81 necon3ai ⊢ ( 𝑁 ≠ 0 → ¬ ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) )
83 80 82 syl ⊢ ( 𝜑 → ¬ ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) )
84 gcdn0cl ⊢ ( ( ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) ) → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ℕ )
85 66 68 83 84 syl21anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ℕ )
86 elnn1uz2 ⊢ ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ℕ ↔ ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 ∨ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ) )
87 85 86 sylib ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 ∨ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ) )
88 87 ord ⊢ ( 𝜑 → ( ¬ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ) )
89 79 88 mt3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 )