Metamath Proof Explorer

Theorem ablfacrplem

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

Ref Expression
Hypotheses ablfacrp.b ⊢ B = Base G
ablfacrp.o ⊢ O = od ⁡ G
ablfacrp.k ⊢ K = x ∈ B | O ⁡ x ∥ M
ablfacrp.l ⊢ L = x ∈ B | O ⁡ x ∥ N
ablfacrp.g ⊢ φ → G ∈ Abel
ablfacrp.m ⊢ φ → M ∈ ℕ
ablfacrp.n ⊢ φ → N ∈ ℕ
ablfacrp.1 ⊢ φ → M gcd N = 1
ablfacrp.2 ⊢ φ → B = M ⋅ N
Assertion ablfacrplem ⊢ φ → K gcd N = 1

Proof

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