This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 45 24 rexeqtrrdv ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ∃ 𝑔 ∈ 𝐾 ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 )
47 20 2 43 subgod ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑂 ‘ 𝑔 ) = ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) )
48 19 47 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑂 ‘ 𝑔 ) = ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) )
49 fveq2 ⊢ ( 𝑥 = 𝑔 → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑔 ) )
50 49 breq1d ⊢ ( 𝑥 = 𝑔 → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ↔ ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 ) )
51 50 3 elrab2 ⊢ ( 𝑔 ∈ 𝐾 ↔ ( 𝑔 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 ) )
52 51 simprbi ⊢ ( 𝑔 ∈ 𝐾 → ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 )
53 52 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( 𝑂 ‘ 𝑔 ) ∥ 𝑀 )
54 48 53 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) ∥ 𝑀 )
55 breq1 ⊢ ( ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 → ( ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) ∥ 𝑀 ↔ 𝑝 ∥ 𝑀 ) )
56 54 55 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) ∧ 𝑔 ∈ 𝐾 ) → ( ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 → 𝑝 ∥ 𝑀 ) )
57 56 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → ( ∃ 𝑔 ∈ 𝐾 ( ( od ‘ ( 𝐺 ↾s 𝐾 ) ) ‘ 𝑔 ) = 𝑝 → 𝑝 ∥ 𝑀 ) )
58 46 57 mpd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ ( ♯ ‘ 𝐾 ) ) → 𝑝 ∥ 𝑀 )
59 58 ex ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) → 𝑝 ∥ 𝑀 ) )
60 59 anim1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) ∧ 𝑝 ∥ 𝑁 ) → ( 𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁 ) ) )
61 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
63 hashcl ⊢ ( 𝐾 ∈ Fin → ( ♯ ‘ 𝐾 ) ∈ ℕ0 )
64 35 63 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℕ0 )
65 64 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℤ )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ♯ ‘ 𝐾 ) ∈ ℤ )
67 7 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℤ )
69 dvdsgcdb ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ) )
70 62 66 68 69 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( ♯ ‘ 𝐾 ) ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ) )
71 15 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑀 ∈ ℤ )
72 dvdsgcdb ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( 𝑀 gcd 𝑁 ) ) )
73 62 71 68 72 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁 ) ↔ 𝑝 ∥ ( 𝑀 gcd 𝑁 ) ) )
74 60 70 73 3imtr3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) → 𝑝 ∥ ( 𝑀 gcd 𝑁 ) ) )
75 14 74 mtod ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ¬ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) )
76 75 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) )
77 exprmfct ⊢ ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) )
78 76 77 nsyl ⊢ ( 𝜑 → ¬ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) )
79 7 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
80 simpr ⊢ ( ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
81 80 necon3ai ⊢ ( 𝑁 ≠ 0 → ¬ ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) )
82 79 81 syl ⊢ ( 𝜑 → ¬ ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) )
83 gcdn0cl ⊢ ( ( ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( ( ♯ ‘ 𝐾 ) = 0 ∧ 𝑁 = 0 ) ) → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ℕ )
84 65 67 82 83 syl21anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ℕ )
85 elnn1uz2 ⊢ ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ℕ ↔ ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 ∨ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ) )
86 84 85 sylib ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 ∨ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ) )
87 86 ord ⊢ ( 𝜑 → ( ¬ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ) )
88 78 87 mt3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 )