Step | Hyp | Ref
| Expression |
1 | | nprmdvds1 15822 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → ¬
𝑝 ∥
1) |
2 | 1 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ 1) |
3 | | ablfacrp.1 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
4 | 3 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀 gcd 𝑁) = 1) |
5 | 4 | breq2d 4898 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝑀 gcd 𝑁) ↔ 𝑝 ∥ 1)) |
6 | 2, 5 | mtbird 317 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ (𝑀 gcd 𝑁)) |
7 | | ablfacrp.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} |
8 | | ablfacrp.g |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Abel) |
9 | | ablfacrp.m |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℕ) |
10 | 9 | nnzd 11833 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) |
11 | | ablfacrp.o |
. . . . . . . . . . . . . . . 16
⊢ 𝑂 = (od‘𝐺) |
12 | | ablfacrp.b |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = (Base‘𝐺) |
13 | 11, 12 | oddvdssubg 18644 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
14 | 8, 10, 13 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
15 | 7, 14 | syl5eqel 2863 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
16 | 15 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 ∈ (SubGrp‘𝐺)) |
17 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢ (𝐺 ↾s 𝐾) = (𝐺 ↾s 𝐾) |
18 | 17 | subggrp 17981 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝐾) ∈ Grp) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (𝐺 ↾s 𝐾) ∈ Grp) |
20 | 17 | subgbas 17982 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 = (Base‘(𝐺 ↾s 𝐾))) |
22 | | ablfacrp.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) |
23 | 9 | nnnn0d 11702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
24 | | ablfacrp.n |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℕ) |
25 | 24 | nnnn0d 11702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
26 | 23, 25 | nn0mulcld 11707 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 · 𝑁) ∈
ℕ0) |
27 | 22, 26 | eqeltrd 2859 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) |
28 | 12 | fvexi 6460 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 ∈ V |
29 | | hashclb 13464 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0) |
31 | 27, 30 | sylibr 226 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ Fin) |
32 | | ssrab2 3908 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ⊆ 𝐵 |
33 | 7, 32 | eqsstri 3854 |
. . . . . . . . . . . . . 14
⊢ 𝐾 ⊆ 𝐵 |
34 | | ssfi 8468 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ 𝐾 ⊆ 𝐵) → 𝐾 ∈ Fin) |
35 | 31, 33, 34 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Fin) |
36 | 35 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 ∈ Fin) |
37 | 21, 36 | eqeltrrd 2860 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (Base‘(𝐺 ↾s 𝐾)) ∈ Fin) |
38 | | simplr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∈ ℙ) |
39 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ (♯‘𝐾)) |
40 | 21 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (♯‘𝐾) = (♯‘(Base‘(𝐺 ↾s 𝐾)))) |
41 | 39, 40 | breqtrd 4912 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ (♯‘(Base‘(𝐺 ↾s 𝐾)))) |
42 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(Base‘(𝐺
↾s 𝐾)) =
(Base‘(𝐺
↾s 𝐾)) |
43 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(od‘(𝐺
↾s 𝐾)) =
(od‘(𝐺
↾s 𝐾)) |
44 | 42, 43 | odcau 18403 |
. . . . . . . . . . 11
⊢ ((((𝐺 ↾s 𝐾) ∈ Grp ∧
(Base‘(𝐺
↾s 𝐾))
∈ Fin ∧ 𝑝 ∈
ℙ) ∧ 𝑝 ∥
(♯‘(Base‘(𝐺 ↾s 𝐾)))) → ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝) |
45 | 19, 37, 38, 41, 44 | syl31anc 1441 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝) |
46 | 21 | rexeqdv 3341 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (∃𝑔 ∈ 𝐾 ((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝 ↔ ∃𝑔 ∈ (Base‘(𝐺 ↾s 𝐾))((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝)) |
47 | 45, 46 | mpbird 249 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → ∃𝑔 ∈ 𝐾 ((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝) |
48 | 17, 11, 43 | subgod 18369 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑔 ∈ 𝐾) → (𝑂‘𝑔) = ((od‘(𝐺 ↾s 𝐾))‘𝑔)) |
49 | 16, 48 | sylan 575 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → (𝑂‘𝑔) = ((od‘(𝐺 ↾s 𝐾))‘𝑔)) |
50 | | fveq2 6446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑔 → (𝑂‘𝑥) = (𝑂‘𝑔)) |
51 | 50 | breq1d 4896 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑔 → ((𝑂‘𝑥) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ 𝑀)) |
52 | 51, 7 | elrab2 3576 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ 𝐾 ↔ (𝑔 ∈ 𝐵 ∧ (𝑂‘𝑔) ∥ 𝑀)) |
53 | 52 | simprbi 492 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ 𝐾 → (𝑂‘𝑔) ∥ 𝑀) |
54 | 53 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → (𝑂‘𝑔) ∥ 𝑀) |
55 | 49, 54 | eqbrtrrd 4910 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → ((od‘(𝐺 ↾s 𝐾))‘𝑔) ∥ 𝑀) |
56 | | breq1 4889 |
. . . . . . . . . . 11
⊢
(((od‘(𝐺
↾s 𝐾))‘𝑔) = 𝑝 → (((od‘(𝐺 ↾s 𝐾))‘𝑔) ∥ 𝑀 ↔ 𝑝 ∥ 𝑀)) |
57 | 55, 56 | syl5ibcom 237 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔 ∈ 𝐾) → (((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝 → 𝑝 ∥ 𝑀)) |
58 | 57 | rexlimdva 3213 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (∃𝑔 ∈ 𝐾 ((od‘(𝐺 ↾s 𝐾))‘𝑔) = 𝑝 → 𝑝 ∥ 𝑀)) |
59 | 47, 58 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ 𝑀) |
60 | 59 | ex 403 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (♯‘𝐾) → 𝑝 ∥ 𝑀)) |
61 | 60 | anim1d 604 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (♯‘𝐾) ∧ 𝑝 ∥ 𝑁) → (𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁))) |
62 | | prmz 15794 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
63 | 62 | adantl 475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ) |
64 | | hashcl 13462 |
. . . . . . . . . 10
⊢ (𝐾 ∈ Fin →
(♯‘𝐾) ∈
ℕ0) |
65 | 35, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐾) ∈
ℕ0) |
66 | 65 | nn0zd 11832 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐾) ∈
ℤ) |
67 | 66 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (♯‘𝐾) ∈
ℤ) |
68 | 24 | nnzd 11833 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
69 | 68 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ) |
70 | | dvdsgcdb 15668 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧
(♯‘𝐾) ∈
ℤ ∧ 𝑁 ∈
ℤ) → ((𝑝 ∥
(♯‘𝐾) ∧
𝑝 ∥ 𝑁) ↔ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁))) |
71 | 63, 67, 69, 70 | syl3anc 1439 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (♯‘𝐾) ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁))) |
72 | 10 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑀 ∈ ℤ) |
73 | | dvdsgcdb 15668 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝑀 gcd 𝑁))) |
74 | 63, 72, 69, 73 | syl3anc 1439 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝑀 ∧ 𝑝 ∥ 𝑁) ↔ 𝑝 ∥ (𝑀 gcd 𝑁))) |
75 | 61, 71, 74 | 3imtr3d 285 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((♯‘𝐾) gcd 𝑁) → 𝑝 ∥ (𝑀 gcd 𝑁))) |
76 | 6, 75 | mtod 190 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)) |
77 | 76 | nrexdv 3182 |
. . 3
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)) |
78 | | exprmfct 15820 |
. . 3
⊢
(((♯‘𝐾)
gcd 𝑁) ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)) |
79 | 77, 78 | nsyl 138 |
. 2
⊢ (𝜑 → ¬
((♯‘𝐾) gcd
𝑁) ∈
(ℤ≥‘2)) |
80 | 24 | nnne0d 11425 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) |
81 | | simpr 479 |
. . . . . . 7
⊢
(((♯‘𝐾)
= 0 ∧ 𝑁 = 0) →
𝑁 = 0) |
82 | 81 | necon3ai 2994 |
. . . . . 6
⊢ (𝑁 ≠ 0 → ¬
((♯‘𝐾) = 0
∧ 𝑁 =
0)) |
83 | 80, 82 | syl 17 |
. . . . 5
⊢ (𝜑 → ¬
((♯‘𝐾) = 0
∧ 𝑁 =
0)) |
84 | | gcdn0cl 15630 |
. . . . 5
⊢
((((♯‘𝐾)
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ ¬ ((♯‘𝐾) = 0 ∧ 𝑁 = 0)) → ((♯‘𝐾) gcd 𝑁) ∈ ℕ) |
85 | 66, 68, 83, 84 | syl21anc 828 |
. . . 4
⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) ∈ ℕ) |
86 | | elnn1uz2 12072 |
. . . 4
⊢
(((♯‘𝐾)
gcd 𝑁) ∈ ℕ
↔ (((♯‘𝐾)
gcd 𝑁) = 1 ∨
((♯‘𝐾) gcd
𝑁) ∈
(ℤ≥‘2))) |
87 | 85, 86 | sylib 210 |
. . 3
⊢ (𝜑 → (((♯‘𝐾) gcd 𝑁) = 1 ∨ ((♯‘𝐾) gcd 𝑁) ∈
(ℤ≥‘2))) |
88 | 87 | ord 853 |
. 2
⊢ (𝜑 → (¬
((♯‘𝐾) gcd
𝑁) = 1 →
((♯‘𝐾) gcd
𝑁) ∈
(ℤ≥‘2))) |
89 | 79, 88 | mt3d 143 |
1
⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1) |