Step | Hyp | Ref
| Expression |
1 | | nprmdvds1 16296 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → ¬
𝑝 ∥
1) |
2 | 1 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ 1) |
3 | | ablfacrp.1 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
4 | 3 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀 gcd 𝑁) = 1) |
5 | 4 | breq2d 5082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝑀 gcd 𝑁) ↔ 𝑝 ∥ 1)) |
6 | 2, 5 | mtbird 328 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ (𝑀 gcd 𝑁)) |
7 | | ablfacrp.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} |
8 | | ablfacrp.g |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Abel) |
9 | | ablfacrp.m |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℕ) |
10 | 9 | nnzd 12311 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) |
11 | | ablfacrp.o |
. . . . . . . . . . . . . . . 16
⊢ 𝑂 = (od‘𝐺) |
12 | | ablfacrp.b |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = (Base‘𝐺) |
13 | 11, 12 | oddvdssubg 19273 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
14 | 8, 10, 13 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
15 | 7, 14 | eqeltrid 2844 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
16 | 15 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 ∈ (SubGrp‘𝐺)) |
17 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢ (𝐺 ↾s 𝐾) = (𝐺 ↾s 𝐾) |
18 | 17 | subggrp 18579 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝐾) ∈ Grp) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (𝐺 ↾s 𝐾) ∈ Grp) |
20 | 17 | subgbas 18580 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
22 | | ablfacrp.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) |
23 | 9 | nnnn0d 12180 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
24 | | ablfacrp.n |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℕ) |
25 | 24 | nnnn0d 12180 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
26 | 23, 25 | nn0mulcld 12185 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 · 𝑁) ∈
ℕ0) |
27 | 22, 26 | eqeltrd 2840 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) |
28 | 12 | fvexi 6753 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 ∈ V |
29 | | hashclb 13958 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0) |
31 | 27, 30 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ Fin) |
32 | 7 | ssrab3 4012 |
. . . . . . . . . . . . . 14
⊢ 𝐾 ⊆ 𝐵 |
33 | | ssfi 8877 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ 𝐾 ⊆ 𝐵) → 𝐾 ∈ Fin) |
34 | 31, 32, 33 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Fin) |
35 | 34 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 ∈ Fin) |
36 | 21, 35 | eqeltrrd 2841 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (Base‘(𝐺 ↾s 𝐾)) ∈ Fin) |
37 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∈ ℙ) |
38 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ (♯‘𝐾)) |
39 | 21 | fveq2d 6743 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (♯‘𝐾) = (♯‘(Base‘(𝐺 ↾s 𝐾)))) |
40 | 38, 39 | breqtrd 5096 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ (♯‘(Base‘(𝐺 ↾s 𝐾)))) |
41 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(Base‘(𝐺
↾s 𝐾)) =
(Base‘(𝐺
↾s 𝐾)) |
42 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(od‘(𝐺
↾s 𝐾)) =
(od‘(𝐺
↾s 𝐾)) |
43 | 41, 42 | odcau 19026 |
. . . . . . . . . . 11
⊢ ((((𝐺 ↾s 𝐾) ∈ Grp ∧
(Base‘(𝐺
↾s 𝐾))
∈ Fin ∧ 𝑝 ∈
ℙ) ∧ 𝑝 ∥
(♯‘(Base‘(𝐺 ↾s 𝐾)))) → ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝) |
44 | 19, 36, 37, 40, 43 | syl31anc 1375 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝) |
45 | 21 | rexeqdv 3341 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (∃𝑔 ∈ 𝐾 ((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝 ↔ ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝)) |
46 | 44, 45 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → ∃𝑔 ∈ 𝐾 ((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝) |
47 | 17, 11, 42 | subgod 18992 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑔 ∈ 𝐾) → (𝑂‘𝑔) = ((od‘(𝐺 ↾s 𝐾))‘𝑔)) |
48 | 16, 47 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → (𝑂‘𝑔) = ((od‘(𝐺 ↾s 𝐾))‘𝑔)) |
49 | | fveq2 6739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑔 → (𝑂‘𝑥) = (𝑂‘𝑔)) |
50 | 49 | breq1d 5080 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑔 → ((𝑂‘𝑥) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ 𝑀)) |
51 | 50, 7 | elrab2 3620 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ 𝐾 ↔ (𝑔 ∈ 𝐵 ∧ (𝑂‘𝑔) ∥ 𝑀)) |
52 | 51 | simprbi 500 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ 𝐾 → (𝑂‘𝑔) ∥ 𝑀) |
53 | 52 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → (𝑂‘𝑔) ∥ 𝑀) |
54 | 48, 53 | eqbrtrrd 5094 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → ((od‘(𝐺 ↾s 𝐾))‘𝑔) ∥ 𝑀) |
55 | | breq1 5073 |
. . . . . . . . . . 11
⊢
(((od‘(𝐺
↾s 𝐾))‘𝑔) = 𝑝 → (((od‘(𝐺 ↾s 𝐾))‘𝑔) ∥ 𝑀 ↔ 𝑝 ∥ 𝑀)) |
56 | 54, 55 | syl5ibcom 248 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → (((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝 → 𝑝 ∥ 𝑀)) |
57 | 56 | rexlimdva 3213 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (∃𝑔 ∈ 𝐾 ((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝 → 𝑝 ∥ 𝑀)) |
58 | 46, 57 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ 𝑀) |
59 | 58 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (♯‘𝐾) → 𝑝 ∥ 𝑀)) |
60 | 59 | anim1d 614 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (♯‘𝐾) ∧ 𝑝 ∥ 𝑁) → (𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁))) |
61 | | prmz 16265 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
62 | 61 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ) |
63 | | hashcl 13956 |
. . . . . . . . . 10
⊢ (𝐾 ∈ Fin →
(♯‘𝐾) ∈
ℕ0) |
64 | 34, 63 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐾) ∈
ℕ0) |
65 | 64 | nn0zd 12310 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐾) ∈
ℤ) |
66 | 65 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (♯‘𝐾) ∈
ℤ) |
67 | 24 | nnzd 12311 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
68 | 67 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ) |
69 | | dvdsgcdb 16138 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
(♯‘𝐾) ∈
ℤ ∧ 𝑁 ∈
ℤ) → ((𝑝 ∥
(♯‘𝐾) ∧
𝑝 ∥ 𝑁) ↔ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁))) |
70 | 62, 66, 68, 69 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (♯‘𝐾) ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁))) |
71 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑀 ∈ ℤ) |
72 | | dvdsgcdb 16138 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝑀 gcd 𝑁))) |
73 | 62, 71, 68, 72 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝑀 gcd 𝑁))) |
74 | 60, 70, 73 | 3imtr3d 296 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((♯‘𝐾) gcd 𝑁) → 𝑝 ∥ (𝑀 gcd 𝑁))) |
75 | 6, 74 | mtod 201 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)) |
76 | 75 | nrexdv 3198 |
. . 3
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)) |
77 | | exprmfct 16294 |
. . 3
⊢
(((♯‘𝐾)
gcd 𝑁) ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)) |
78 | 76, 77 | nsyl 142 |
. 2
⊢ (𝜑 → ¬
((♯‘𝐾) gcd
𝑁) ∈
(ℤ≥‘2)) |
79 | 24 | nnne0d 11910 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) |
80 | | simpr 488 |
. . . . . . 7
⊢
(((♯‘𝐾)
= 0 ∧ 𝑁 = 0) →
𝑁 = 0) |
81 | 80 | necon3ai 2968 |
. . . . . 6
⊢ (𝑁 ≠ 0 → ¬
((♯‘𝐾) = 0
∧ 𝑁 =
0)) |
82 | 79, 81 | syl 17 |
. . . . 5
⊢ (𝜑 → ¬
((♯‘𝐾) = 0
∧ 𝑁 =
0)) |
83 | | gcdn0cl 16094 |
. . . . 5
⊢
((((♯‘𝐾)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ ¬ ((♯‘𝐾) = 0 ∧ 𝑁 = 0)) → ((♯‘𝐾) gcd 𝑁) ∈ ℕ) |
84 | 65, 67, 82, 83 | syl21anc 838 |
. . . 4
⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) ∈ ℕ) |
85 | | elnn1uz2 12551 |
. . . 4
⊢
(((♯‘𝐾)
gcd 𝑁) ∈ ℕ
↔ (((♯‘𝐾)
gcd 𝑁) = 1 ∨
((♯‘𝐾) gcd
𝑁) ∈
(ℤ≥‘2))) |
86 | 84, 85 | sylib 221 |
. . 3
⊢ (𝜑 → (((♯‘𝐾) gcd 𝑁) = 1 ∨ ((♯‘𝐾) gcd 𝑁) ∈
(ℤ≥‘2))) |
87 | 86 | ord 864 |
. 2
⊢ (𝜑 → (¬
((♯‘𝐾) gcd
𝑁) = 1 →
((♯‘𝐾) gcd
𝑁) ∈
(ℤ≥‘2))) |
88 | 78, 87 | mt3d 150 |
1
⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1) |