MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablfacrplem Structured version   Visualization version   GIF version

Theorem ablfacrplem 19485
Description: Lemma for ablfacrp2 19487. (Contributed by Mario Carneiro, 19-Apr-2016.)
Hypotheses
Ref Expression
ablfacrp.b 𝐵 = (Base‘𝐺)
ablfacrp.o 𝑂 = (od‘𝐺)
ablfacrp.k 𝐾 = {𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑀}
ablfacrp.l 𝐿 = {𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑁}
ablfacrp.g (𝜑𝐺 ∈ Abel)
ablfacrp.m (𝜑𝑀 ∈ ℕ)
ablfacrp.n (𝜑𝑁 ∈ ℕ)
ablfacrp.1 (𝜑 → (𝑀 gcd 𝑁) = 1)
ablfacrp.2 (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))
Assertion
Ref Expression
ablfacrplem (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1)
Distinct variable groups:   𝑥,𝐵   𝑥,𝐺   𝑥,𝑂   𝑥,𝑀   𝑥,𝑁   𝜑,𝑥
Allowed substitution hints:   𝐾(𝑥)   𝐿(𝑥)

Proof of Theorem ablfacrplem
Dummy variables 𝑔 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nprmdvds1 16296 . . . . . . 7 (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
21adantl 485 . . . . . 6 ((𝜑𝑝 ∈ ℙ) → ¬ 𝑝 ∥ 1)
3 ablfacrp.1 . . . . . . . 8 (𝜑 → (𝑀 gcd 𝑁) = 1)
43adantr 484 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → (𝑀 gcd 𝑁) = 1)
54breq2d 5082 . . . . . 6 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ (𝑀 gcd 𝑁) ↔ 𝑝 ∥ 1))
62, 5mtbird 328 . . . . 5 ((𝜑𝑝 ∈ ℙ) → ¬ 𝑝 ∥ (𝑀 gcd 𝑁))
7 ablfacrp.k . . . . . . . . . . . . . 14 𝐾 = {𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑀}
8 ablfacrp.g . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ Abel)
9 ablfacrp.m . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℕ)
109nnzd 12311 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℤ)
11 ablfacrp.o . . . . . . . . . . . . . . . 16 𝑂 = (od‘𝐺)
12 ablfacrp.b . . . . . . . . . . . . . . . 16 𝐵 = (Base‘𝐺)
1311, 12oddvdssubg 19273 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
148, 10, 13syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → {𝑥𝐵 ∣ (𝑂𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
157, 14eqeltrid 2844 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ (SubGrp‘𝐺))
1615ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 ∈ (SubGrp‘𝐺))
17 eqid 2739 . . . . . . . . . . . . 13 (𝐺s 𝐾) = (𝐺s 𝐾)
1817subggrp 18579 . . . . . . . . . . . 12 (𝐾 ∈ (SubGrp‘𝐺) → (𝐺s 𝐾) ∈ Grp)
1916, 18syl 17 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (𝐺s 𝐾) ∈ Grp)
2017subgbas 18580 . . . . . . . . . . . . 13 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 = (Base‘(𝐺s 𝐾)))
2116, 20syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 = (Base‘(𝐺s 𝐾)))
22 ablfacrp.2 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))
239nnnn0d 12180 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ0)
24 ablfacrp.n . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℕ)
2524nnnn0d 12180 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ0)
2623, 25nn0mulcld 12185 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 · 𝑁) ∈ ℕ0)
2722, 26eqeltrd 2840 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘𝐵) ∈ ℕ0)
2812fvexi 6753 . . . . . . . . . . . . . . . 16 𝐵 ∈ V
29 hashclb 13958 . . . . . . . . . . . . . . . 16 (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15 (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
3127, 30sylibr 237 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ Fin)
327ssrab3 4012 . . . . . . . . . . . . . 14 𝐾𝐵
33 ssfi 8877 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ 𝐾𝐵) → 𝐾 ∈ Fin)
3431, 32, 33sylancl 589 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ Fin)
3534ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝐾 ∈ Fin)
3621, 35eqeltrrd 2841 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (Base‘(𝐺s 𝐾)) ∈ Fin)
37 simplr 769 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∈ ℙ)
38 simpr 488 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ (♯‘𝐾))
3921fveq2d 6743 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (♯‘𝐾) = (♯‘(Base‘(𝐺s 𝐾))))
4038, 39breqtrd 5096 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝 ∥ (♯‘(Base‘(𝐺s 𝐾))))
41 eqid 2739 . . . . . . . . . . . 12 (Base‘(𝐺s 𝐾)) = (Base‘(𝐺s 𝐾))
42 eqid 2739 . . . . . . . . . . . 12 (od‘(𝐺s 𝐾)) = (od‘(𝐺s 𝐾))
4341, 42odcau 19026 . . . . . . . . . . 11 ((((𝐺s 𝐾) ∈ Grp ∧ (Base‘(𝐺s 𝐾)) ∈ Fin ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘(Base‘(𝐺s 𝐾)))) → ∃𝑔 ∈ (Base‘(𝐺s 𝐾))((od‘(𝐺s 𝐾))‘𝑔) = 𝑝)
4419, 36, 37, 40, 43syl31anc 1375 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → ∃𝑔 ∈ (Base‘(𝐺s 𝐾))((od‘(𝐺s 𝐾))‘𝑔) = 𝑝)
4521rexeqdv 3341 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (∃𝑔𝐾 ((od‘(𝐺s 𝐾))‘𝑔) = 𝑝 ↔ ∃𝑔 ∈ (Base‘(𝐺s 𝐾))((od‘(𝐺s 𝐾))‘𝑔) = 𝑝))
4644, 45mpbird 260 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → ∃𝑔𝐾 ((od‘(𝐺s 𝐾))‘𝑔) = 𝑝)
4717, 11, 42subgod 18992 . . . . . . . . . . . . 13 ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑔𝐾) → (𝑂𝑔) = ((od‘(𝐺s 𝐾))‘𝑔))
4816, 47sylan 583 . . . . . . . . . . . 12 ((((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔𝐾) → (𝑂𝑔) = ((od‘(𝐺s 𝐾))‘𝑔))
49 fveq2 6739 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑔 → (𝑂𝑥) = (𝑂𝑔))
5049breq1d 5080 . . . . . . . . . . . . . . 15 (𝑥 = 𝑔 → ((𝑂𝑥) ∥ 𝑀 ↔ (𝑂𝑔) ∥ 𝑀))
5150, 7elrab2 3620 . . . . . . . . . . . . . 14 (𝑔𝐾 ↔ (𝑔𝐵 ∧ (𝑂𝑔) ∥ 𝑀))
5251simprbi 500 . . . . . . . . . . . . 13 (𝑔𝐾 → (𝑂𝑔) ∥ 𝑀)
5352adantl 485 . . . . . . . . . . . 12 ((((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔𝐾) → (𝑂𝑔) ∥ 𝑀)
5448, 53eqbrtrrd 5094 . . . . . . . . . . 11 ((((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔𝐾) → ((od‘(𝐺s 𝐾))‘𝑔) ∥ 𝑀)
55 breq1 5073 . . . . . . . . . . 11 (((od‘(𝐺s 𝐾))‘𝑔) = 𝑝 → (((od‘(𝐺s 𝐾))‘𝑔) ∥ 𝑀𝑝𝑀))
5654, 55syl5ibcom 248 . . . . . . . . . 10 ((((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) ∧ 𝑔𝐾) → (((od‘(𝐺s 𝐾))‘𝑔) = 𝑝𝑝𝑀))
5756rexlimdva 3213 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → (∃𝑔𝐾 ((od‘(𝐺s 𝐾))‘𝑔) = 𝑝𝑝𝑀))
5846, 57mpd 15 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝 ∥ (♯‘𝐾)) → 𝑝𝑀)
5958ex 416 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ (♯‘𝐾) → 𝑝𝑀))
6059anim1d 614 . . . . . 6 ((𝜑𝑝 ∈ ℙ) → ((𝑝 ∥ (♯‘𝐾) ∧ 𝑝𝑁) → (𝑝𝑀𝑝𝑁)))
61 prmz 16265 . . . . . . . 8 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
6261adantl 485 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
63 hashcl 13956 . . . . . . . . . 10 (𝐾 ∈ Fin → (♯‘𝐾) ∈ ℕ0)
6434, 63syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐾) ∈ ℕ0)
6564nn0zd 12310 . . . . . . . 8 (𝜑 → (♯‘𝐾) ∈ ℤ)
6665adantr 484 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → (♯‘𝐾) ∈ ℤ)
6724nnzd 12311 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
6867adantr 484 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → 𝑁 ∈ ℤ)
69 dvdsgcdb 16138 . . . . . . 7 ((𝑝 ∈ ℤ ∧ (♯‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝 ∥ (♯‘𝐾) ∧ 𝑝𝑁) ↔ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)))
7062, 66, 68, 69syl3anc 1373 . . . . . 6 ((𝜑𝑝 ∈ ℙ) → ((𝑝 ∥ (♯‘𝐾) ∧ 𝑝𝑁) ↔ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁)))
7110adantr 484 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → 𝑀 ∈ ℤ)
72 dvdsgcdb 16138 . . . . . . 7 ((𝑝 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑝𝑀𝑝𝑁) ↔ 𝑝 ∥ (𝑀 gcd 𝑁)))
7362, 71, 68, 72syl3anc 1373 . . . . . 6 ((𝜑𝑝 ∈ ℙ) → ((𝑝𝑀𝑝𝑁) ↔ 𝑝 ∥ (𝑀 gcd 𝑁)))
7460, 70, 733imtr3d 296 . . . . 5 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ ((♯‘𝐾) gcd 𝑁) → 𝑝 ∥ (𝑀 gcd 𝑁)))
756, 74mtod 201 . . . 4 ((𝜑𝑝 ∈ ℙ) → ¬ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁))
7675nrexdv 3198 . . 3 (𝜑 → ¬ ∃𝑝 ∈ ℙ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁))
77 exprmfct 16294 . . 3 (((♯‘𝐾) gcd 𝑁) ∈ (ℤ‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((♯‘𝐾) gcd 𝑁))
7876, 77nsyl 142 . 2 (𝜑 → ¬ ((♯‘𝐾) gcd 𝑁) ∈ (ℤ‘2))
7924nnne0d 11910 . . . . . 6 (𝜑𝑁 ≠ 0)
80 simpr 488 . . . . . . 7 (((♯‘𝐾) = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
8180necon3ai 2968 . . . . . 6 (𝑁 ≠ 0 → ¬ ((♯‘𝐾) = 0 ∧ 𝑁 = 0))
8279, 81syl 17 . . . . 5 (𝜑 → ¬ ((♯‘𝐾) = 0 ∧ 𝑁 = 0))
83 gcdn0cl 16094 . . . . 5 ((((♯‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ ((♯‘𝐾) = 0 ∧ 𝑁 = 0)) → ((♯‘𝐾) gcd 𝑁) ∈ ℕ)
8465, 67, 82, 83syl21anc 838 . . . 4 (𝜑 → ((♯‘𝐾) gcd 𝑁) ∈ ℕ)
85 elnn1uz2 12551 . . . 4 (((♯‘𝐾) gcd 𝑁) ∈ ℕ ↔ (((♯‘𝐾) gcd 𝑁) = 1 ∨ ((♯‘𝐾) gcd 𝑁) ∈ (ℤ‘2)))
8684, 85sylib 221 . . 3 (𝜑 → (((♯‘𝐾) gcd 𝑁) = 1 ∨ ((♯‘𝐾) gcd 𝑁) ∈ (ℤ‘2)))
8786ord 864 . 2 (𝜑 → (¬ ((♯‘𝐾) gcd 𝑁) = 1 → ((♯‘𝐾) gcd 𝑁) ∈ (ℤ‘2)))
8878, 87mt3d 150 1 (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wcel 2112  wne 2943  wrex 3065  {crab 3068  Vcvv 3423  wss 3883   class class class wbr 5070  cfv 6401  (class class class)co 7235  Fincfn 8650  0cc0 10759  1c1 10760   · cmul 10764  cn 11860  2c2 11915  0cn0 12120  cz 12206  cuz 12468  chash 13929  cdvds 15848   gcd cgcd 16086  cprime 16261  Basecbs 16793  s cress 16817  Grpcgrp 18398  SubGrpcsubg 18570  odcod 18949  Abelcabl 19204
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-inf2 9286  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836  ax-pre-sup 10837
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-disj 5036  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-se 5528  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-isom 6410  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-om 7667  df-1st 7783  df-2nd 7784  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-1o 8226  df-2o 8227  df-oadd 8230  df-omul 8231  df-er 8415  df-ec 8417  df-qs 8421  df-map 8534  df-en 8651  df-dom 8652  df-sdom 8653  df-fin 8654  df-sup 9088  df-inf 9089  df-oi 9156  df-dju 9547  df-card 9585  df-acn 9588  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-div 11520  df-nn 11861  df-2 11923  df-3 11924  df-n0 12121  df-xnn0 12193  df-z 12207  df-uz 12469  df-q 12575  df-rp 12617  df-fz 13126  df-fzo 13269  df-fl 13397  df-mod 13475  df-seq 13607  df-exp 13668  df-fac 13873  df-bc 13902  df-hash 13930  df-cj 14695  df-re 14696  df-im 14697  df-sqrt 14831  df-abs 14832  df-clim 15082  df-sum 15283  df-dvds 15849  df-gcd 16087  df-prm 16262  df-pc 16423  df-sets 16750  df-slot 16768  df-ndx 16778  df-base 16794  df-ress 16818  df-plusg 16848  df-0g 16979  df-mgm 18147  df-sgrp 18196  df-mnd 18207  df-submnd 18252  df-grp 18401  df-minusg 18402  df-sbg 18403  df-mulg 18522  df-subg 18573  df-eqg 18575  df-ga 18717  df-od 18953  df-cmn 19205  df-abl 19206
This theorem is referenced by:  ablfacrp2  19487
  Copyright terms: Public domain W3C validator