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

Theorem dchrpt 26177
Description: For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016.)
Hypotheses
Ref Expression
dchrpt.g 𝐺 = (DChr‘𝑁)
dchrpt.z 𝑍 = (ℤ/nℤ‘𝑁)
dchrpt.d 𝐷 = (Base‘𝐺)
dchrpt.b 𝐵 = (Base‘𝑍)
dchrpt.1 1 = (1r𝑍)
dchrpt.n (𝜑𝑁 ∈ ℕ)
dchrpt.n1 (𝜑𝐴1 )
dchrpt.a (𝜑𝐴𝐵)
Assertion
Ref Expression
dchrpt (𝜑 → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
Distinct variable groups:   𝑥, 1   𝑥,𝐴   𝑥,𝐵   𝑥,𝐺   𝑥,𝑁   𝑥,𝑍   𝑥,𝐷   𝜑,𝑥

Proof of Theorem dchrpt
Dummy variables 𝑎 𝑏 𝑘 𝑛 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dchrpt.g . . . . 5 𝐺 = (DChr‘𝑁)
2 dchrpt.z . . . . 5 𝑍 = (ℤ/nℤ‘𝑁)
3 dchrpt.d . . . . 5 𝐷 = (Base‘𝐺)
4 dchrpt.b . . . . 5 𝐵 = (Base‘𝑍)
5 dchrpt.1 . . . . 5 1 = (1r𝑍)
6 dchrpt.n . . . . . 6 (𝜑𝑁 ∈ ℕ)
76ad3antrrr 730 . . . . 5 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → 𝑁 ∈ ℕ)
8 dchrpt.n1 . . . . . 6 (𝜑𝐴1 )
98ad3antrrr 730 . . . . 5 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → 𝐴1 )
10 eqid 2739 . . . . 5 (Unit‘𝑍) = (Unit‘𝑍)
11 eqid 2739 . . . . 5 ((mulGrp‘𝑍) ↾s (Unit‘𝑍)) = ((mulGrp‘𝑍) ↾s (Unit‘𝑍))
12 eqid 2739 . . . . 5 (.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) = (.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))
13 oveq1 7241 . . . . . . . . 9 (𝑛 = 𝑏 → (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)) = (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))
1413cbvmptv 5174 . . . . . . . 8 (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))) = (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))
15 fveq2 6738 . . . . . . . . . 10 (𝑘 = 𝑎 → (𝑤𝑘) = (𝑤𝑎))
1615oveq2d 7250 . . . . . . . . 9 (𝑘 = 𝑎 → (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)) = (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑎)))
1716mpteq2dv 5167 . . . . . . . 8 (𝑘 = 𝑎 → (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))) = (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑎))))
1814, 17syl5eq 2792 . . . . . . 7 (𝑘 = 𝑎 → (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))) = (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑎))))
1918rneqd 5824 . . . . . 6 (𝑘 = 𝑎 → ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))) = ran (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑎))))
2019cbvmptv 5174 . . . . 5 (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) = (𝑎 ∈ dom 𝑤 ↦ ran (𝑏 ∈ ℤ ↦ (𝑏(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑎))))
21 simpllr 776 . . . . 5 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → 𝐴 ∈ (Unit‘𝑍))
22 simplr 769 . . . . 5 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → 𝑤 ∈ Word (Unit‘𝑍))
23 simprl 771 . . . . 5 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → ((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))))
24 simprr 773 . . . . 5 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))
251, 2, 3, 4, 5, 7, 9, 10, 11, 12, 20, 21, 22, 23, 24dchrptlem3 26176 . . . 4 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
26253adantr1 1171 . . 3 ((((𝜑𝐴 ∈ (Unit‘𝑍)) ∧ 𝑤 ∈ Word (Unit‘𝑍)) ∧ ((𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))):dom 𝑤⟶{𝑢 ∈ (SubGrp‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) ∣ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp )} ∧ ((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍))) → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
2710, 11unitgrpbas 19714 . . . 4 (Unit‘𝑍) = (Base‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))
28 eqid 2739 . . . 4 {𝑢 ∈ (SubGrp‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) ∣ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp )} = {𝑢 ∈ (SubGrp‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) ∣ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp )}
296nnnn0d 12177 . . . . . 6 (𝜑𝑁 ∈ ℕ0)
302zncrng 20539 . . . . . 6 (𝑁 ∈ ℕ0𝑍 ∈ CRing)
3110, 11unitabl 19716 . . . . . 6 (𝑍 ∈ CRing → ((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ∈ Abel)
3229, 30, 313syl 18 . . . . 5 (𝜑 → ((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ∈ Abel)
3332adantr 484 . . . 4 ((𝜑𝐴 ∈ (Unit‘𝑍)) → ((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ∈ Abel)
342, 4znfi 20554 . . . . . . 7 (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
356, 34syl 17 . . . . . 6 (𝜑𝐵 ∈ Fin)
364, 10unitss 19708 . . . . . 6 (Unit‘𝑍) ⊆ 𝐵
37 ssfi 8876 . . . . . 6 ((𝐵 ∈ Fin ∧ (Unit‘𝑍) ⊆ 𝐵) → (Unit‘𝑍) ∈ Fin)
3835, 36, 37sylancl 589 . . . . 5 (𝜑 → (Unit‘𝑍) ∈ Fin)
3938adantr 484 . . . 4 ((𝜑𝐴 ∈ (Unit‘𝑍)) → (Unit‘𝑍) ∈ Fin)
40 eqid 2739 . . . 4 (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))
4127, 28, 33, 39, 12, 40ablfac2 19506 . . 3 ((𝜑𝐴 ∈ (Unit‘𝑍)) → ∃𝑤 ∈ Word (Unit‘𝑍)((𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))):dom 𝑤⟶{𝑢 ∈ (SubGrp‘((mulGrp‘𝑍) ↾s (Unit‘𝑍))) ∣ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) ↾s 𝑢) ∈ (CycGrp ∩ ran pGrp )} ∧ ((mulGrp‘𝑍) ↾s (Unit‘𝑍))dom DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘)))) ∧ (((mulGrp‘𝑍) ↾s (Unit‘𝑍)) DProd (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘((mulGrp‘𝑍) ↾s (Unit‘𝑍)))(𝑤𝑘))))) = (Unit‘𝑍)))
4226, 41r19.29a 3217 . 2 ((𝜑𝐴 ∈ (Unit‘𝑍)) → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
431dchrabl 26164 . . . 4 (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
44 ablgrp 19205 . . . 4 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
45 eqid 2739 . . . . 5 (0g𝐺) = (0g𝐺)
463, 45grpidcl 18425 . . . 4 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝐷)
476, 43, 44, 464syl 19 . . 3 (𝜑 → (0g𝐺) ∈ 𝐷)
48 0ne1 11928 . . . 4 0 ≠ 1
49 dchrpt.a . . . . . . . 8 (𝜑𝐴𝐵)
501, 2, 3, 4, 10, 47, 49dchrn0 26160 . . . . . . 7 (𝜑 → (((0g𝐺)‘𝐴) ≠ 0 ↔ 𝐴 ∈ (Unit‘𝑍)))
5150necon1bbid 2982 . . . . . 6 (𝜑 → (¬ 𝐴 ∈ (Unit‘𝑍) ↔ ((0g𝐺)‘𝐴) = 0))
5251biimpa 480 . . . . 5 ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → ((0g𝐺)‘𝐴) = 0)
5352neeq1d 3002 . . . 4 ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → (((0g𝐺)‘𝐴) ≠ 1 ↔ 0 ≠ 1))
5448, 53mpbiri 261 . . 3 ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → ((0g𝐺)‘𝐴) ≠ 1)
55 fveq1 6737 . . . . 5 (𝑥 = (0g𝐺) → (𝑥𝐴) = ((0g𝐺)‘𝐴))
5655neeq1d 3002 . . . 4 (𝑥 = (0g𝐺) → ((𝑥𝐴) ≠ 1 ↔ ((0g𝐺)‘𝐴) ≠ 1))
5756rspcev 3551 . . 3 (((0g𝐺) ∈ 𝐷 ∧ ((0g𝐺)‘𝐴) ≠ 1) → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
5847, 54, 57syl2an2r 685 . 2 ((𝜑 ∧ ¬ 𝐴 ∈ (Unit‘𝑍)) → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
5942, 58pm2.61dan 813 1 (𝜑 → ∃𝑥𝐷 (𝑥𝐴) ≠ 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2112  wne 2942  wrex 3064  {crab 3067  cin 3881  wss 3882   class class class wbr 5069  cmpt 5151  dom cdm 5568  ran crn 5569  wf 6396  cfv 6400  (class class class)co 7234  Fincfn 8649  0cc0 10756  1c1 10757  cn 11857  0cn0 12117  cz 12203  Word cword 14099  Basecbs 16790  s cress 16814  0gc0g 16974  Grpcgrp 18395  .gcmg 18518  SubGrpcsubg 18567   pGrp cpgp 18948  Abelcabl 19201  CycGrpccyg 19291   DProd cdprd 19410  mulGrpcmgp 19534  1rcur 19546  CRingccrg 19593  Unitcui 19687  ℤ/nczn 20499  DChrcdchr 26142
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 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-inf2 9283  ax-cnex 10812  ax-resscn 10813  ax-1cn 10814  ax-icn 10815  ax-addcl 10816  ax-addrcl 10817  ax-mulcl 10818  ax-mulrcl 10819  ax-mulcom 10820  ax-addass 10821  ax-mulass 10822  ax-distr 10823  ax-i2m1 10824  ax-1ne0 10825  ax-1rid 10826  ax-rnegex 10827  ax-rrecex 10828  ax-cnre 10829  ax-pre-lttri 10830  ax-pre-lttrn 10831  ax-pre-ltadd 10832  ax-pre-mulgt0 10833  ax-pre-sup 10834  ax-addf 10835  ax-mulf 10836
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 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-int 4876  df-iun 4922  df-iin 4923  df-disj 5035  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-se 5527  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-isom 6409  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-of 7490  df-rpss 7532  df-om 7666  df-1st 7782  df-2nd 7783  df-supp 7927  df-tpos 7991  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-1o 8225  df-2o 8226  df-oadd 8229  df-omul 8230  df-er 8414  df-ec 8416  df-qs 8420  df-map 8533  df-pm 8534  df-ixp 8602  df-en 8650  df-dom 8651  df-sdom 8652  df-fin 8653  df-fsupp 9013  df-fi 9054  df-sup 9085  df-inf 9086  df-oi 9153  df-dju 9544  df-card 9582  df-acn 9585  df-pnf 10896  df-mnf 10897  df-xr 10898  df-ltxr 10899  df-le 10900  df-sub 11091  df-neg 11092  df-div 11517  df-nn 11858  df-2 11920  df-3 11921  df-4 11922  df-5 11923  df-6 11924  df-7 11925  df-8 11926  df-9 11927  df-n0 12118  df-xnn0 12190  df-z 12204  df-dec 12321  df-uz 12466  df-q 12572  df-rp 12614  df-xneg 12731  df-xadd 12732  df-xmul 12733  df-ioo 12966  df-ioc 12967  df-ico 12968  df-icc 12969  df-fz 13123  df-fzo 13266  df-fl 13394  df-mod 13472  df-seq 13604  df-exp 13665  df-fac 13870  df-bc 13899  df-hash 13927  df-word 14100  df-concat 14156  df-s1 14183  df-shft 14660  df-cj 14692  df-re 14693  df-im 14694  df-sqrt 14828  df-abs 14829  df-limsup 15062  df-clim 15079  df-rlim 15080  df-sum 15280  df-ef 15659  df-sin 15661  df-cos 15662  df-pi 15664  df-dvds 15846  df-gcd 16084  df-prm 16259  df-pc 16420  df-struct 16730  df-sets 16747  df-slot 16765  df-ndx 16775  df-base 16791  df-ress 16815  df-plusg 16845  df-mulr 16846  df-starv 16847  df-sca 16848  df-vsca 16849  df-ip 16850  df-tset 16851  df-ple 16852  df-ds 16854  df-unif 16855  df-hom 16856  df-cco 16857  df-rest 16957  df-topn 16958  df-0g 16976  df-gsum 16977  df-topgen 16978  df-pt 16979  df-prds 16982  df-xrs 17037  df-qtop 17042  df-imas 17043  df-qus 17044  df-xps 17045  df-mre 17119  df-mrc 17120  df-acs 17122  df-mgm 18144  df-sgrp 18193  df-mnd 18204  df-mhm 18248  df-submnd 18249  df-grp 18398  df-minusg 18399  df-sbg 18400  df-mulg 18519  df-subg 18570  df-nsg 18571  df-eqg 18572  df-ghm 18650  df-gim 18693  df-ga 18714  df-cntz 18741  df-oppg 18768  df-od 18950  df-gex 18951  df-pgp 18952  df-lsm 19055  df-pj1 19056  df-cmn 19202  df-abl 19203  df-cyg 19292  df-dprd 19412  df-dpj 19413  df-mgp 19535  df-ur 19547  df-ring 19594  df-cring 19595  df-oppr 19671  df-dvdsr 19689  df-unit 19690  df-invr 19720  df-rnghom 19765  df-subrg 19828  df-lmod 19931  df-lss 19999  df-lsp 20039  df-sra 20239  df-rgmod 20240  df-lidl 20241  df-rsp 20242  df-2idl 20300  df-psmet 20385  df-xmet 20386  df-met 20387  df-bl 20388  df-mopn 20389  df-fbas 20390  df-fg 20391  df-cnfld 20394  df-zring 20466  df-zrh 20500  df-zn 20503  df-top 21820  df-topon 21837  df-topsp 21859  df-bases 21872  df-cld 21945  df-ntr 21946  df-cls 21947  df-nei 22024  df-lp 22062  df-perf 22063  df-cn 22153  df-cnp 22154  df-haus 22241  df-tx 22488  df-hmeo 22681  df-fil 22772  df-fm 22864  df-flim 22865  df-flf 22866  df-xms 23247  df-ms 23248  df-tms 23249  df-cncf 23804  df-limc 24792  df-dv 24793  df-log 25474  df-cxp 25475  df-dchr 26143
This theorem is referenced by:  sumdchr2  26180
  Copyright terms: Public domain W3C validator