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

Theorem dv11cn 24201
Description: Two functions defined on a ball whose derivatives are the same and which are equal at any given point 𝐶 in the ball must be equal everywhere. (Contributed by Mario Carneiro, 31-Mar-2015.)
Hypotheses
Ref Expression
dv11cn.x 𝑋 = (𝐴(ball‘(abs ∘ − ))𝑅)
dv11cn.a (𝜑𝐴 ∈ ℂ)
dv11cn.r (𝜑𝑅 ∈ ℝ*)
dv11cn.f (𝜑𝐹:𝑋⟶ℂ)
dv11cn.g (𝜑𝐺:𝑋⟶ℂ)
dv11cn.d (𝜑 → dom (ℂ D 𝐹) = 𝑋)
dv11cn.e (𝜑 → (ℂ D 𝐹) = (ℂ D 𝐺))
dv11cn.c (𝜑𝐶𝑋)
dv11cn.p (𝜑 → (𝐹𝐶) = (𝐺𝐶))
Assertion
Ref Expression
dv11cn (𝜑𝐹 = 𝐺)

Proof of Theorem dv11cn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dv11cn.f . . . . 5 (𝜑𝐹:𝑋⟶ℂ)
21ffnd 6292 . . . 4 (𝜑𝐹 Fn 𝑋)
3 dv11cn.g . . . . 5 (𝜑𝐺:𝑋⟶ℂ)
43ffnd 6292 . . . 4 (𝜑𝐺 Fn 𝑋)
5 dv11cn.x . . . . . 6 𝑋 = (𝐴(ball‘(abs ∘ − ))𝑅)
6 ovex 6954 . . . . . 6 (𝐴(ball‘(abs ∘ − ))𝑅) ∈ V
75, 6eqeltri 2855 . . . . 5 𝑋 ∈ V
87a1i 11 . . . 4 (𝜑𝑋 ∈ V)
9 inidm 4043 . . . 4 (𝑋𝑋) = 𝑋
102, 4, 8, 8, 9offn 7185 . . 3 (𝜑 → (𝐹𝑓𝐺) Fn 𝑋)
11 0cn 10368 . . . 4 0 ∈ ℂ
12 fnconstg 6343 . . . 4 (0 ∈ ℂ → (𝑋 × {0}) Fn 𝑋)
1311, 12mp1i 13 . . 3 (𝜑 → (𝑋 × {0}) Fn 𝑋)
14 subcl 10621 . . . . . . . 8 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝑦) ∈ ℂ)
1514adantl 475 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥𝑦) ∈ ℂ)
1615, 1, 3, 8, 8, 9off 7189 . . . . . 6 (𝜑 → (𝐹𝑓𝐺):𝑋⟶ℂ)
1716ffvelrnda 6623 . . . . 5 ((𝜑𝑥𝑋) → ((𝐹𝑓𝐺)‘𝑥) ∈ ℂ)
18 simpr 479 . . . . . . . . 9 ((𝜑𝑥𝑋) → 𝑥𝑋)
19 dv11cn.c . . . . . . . . . 10 (𝜑𝐶𝑋)
2019adantr 474 . . . . . . . . 9 ((𝜑𝑥𝑋) → 𝐶𝑋)
2118, 20jca 507 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝑥𝑋𝐶𝑋))
22 cnxmet 22984 . . . . . . . . . . . 12 (abs ∘ − ) ∈ (∞Met‘ℂ)
2322a1i 11 . . . . . . . . . . 11 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
24 dv11cn.a . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
25 dv11cn.r . . . . . . . . . . 11 (𝜑𝑅 ∈ ℝ*)
26 blssm 22631 . . . . . . . . . . 11 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (𝐴(ball‘(abs ∘ − ))𝑅) ⊆ ℂ)
2723, 24, 25, 26syl3anc 1439 . . . . . . . . . 10 (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ⊆ ℂ)
285, 27syl5eqss 3868 . . . . . . . . 9 (𝜑𝑋 ⊆ ℂ)
291ffvelrnda 6623 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ ℂ)
303ffvelrnda 6623 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (𝐺𝑥) ∈ ℂ)
311feqmptd 6509 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝑥𝑋 ↦ (𝐹𝑥)))
323feqmptd 6509 . . . . . . . . . . . . . . 15 (𝜑𝐺 = (𝑥𝑋 ↦ (𝐺𝑥)))
338, 29, 30, 31, 32offval2 7191 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑓𝐺) = (𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥))))
3433oveq2d 6938 . . . . . . . . . . . . 13 (𝜑 → (ℂ D (𝐹𝑓𝐺)) = (ℂ D (𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥)))))
35 cnelprrecn 10365 . . . . . . . . . . . . . . 15 ℂ ∈ {ℝ, ℂ}
3635a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℂ ∈ {ℝ, ℂ})
37 fvexd 6461 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ V)
3831oveq2d 6938 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑥𝑋 ↦ (𝐹𝑥))))
39 dvfcn 24109 . . . . . . . . . . . . . . . . 17 (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
40 dv11cn.d . . . . . . . . . . . . . . . . . 18 (𝜑 → dom (ℂ D 𝐹) = 𝑋)
4140feq2d 6277 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ D 𝐹):𝑋⟶ℂ))
4239, 41mpbii 225 . . . . . . . . . . . . . . . 16 (𝜑 → (ℂ D 𝐹):𝑋⟶ℂ)
4342feqmptd 6509 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ D 𝐹) = (𝑥𝑋 ↦ ((ℂ D 𝐹)‘𝑥)))
4438, 43eqtr3d 2816 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D (𝑥𝑋 ↦ (𝐹𝑥))) = (𝑥𝑋 ↦ ((ℂ D 𝐹)‘𝑥)))
45 dv11cn.e . . . . . . . . . . . . . . 15 (𝜑 → (ℂ D 𝐹) = (ℂ D 𝐺))
4632oveq2d 6938 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ D 𝐺) = (ℂ D (𝑥𝑋 ↦ (𝐺𝑥))))
4745, 43, 463eqtr3rd 2823 . . . . . . . . . . . . . 14 (𝜑 → (ℂ D (𝑥𝑋 ↦ (𝐺𝑥))) = (𝑥𝑋 ↦ ((ℂ D 𝐹)‘𝑥)))
4836, 29, 37, 44, 30, 37, 47dvmptsub 24167 . . . . . . . . . . . . 13 (𝜑 → (ℂ D (𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥)))) = (𝑥𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))))
4942ffvelrnda 6623 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → ((ℂ D 𝐹)‘𝑥) ∈ ℂ)
5049subidd 10722 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥)) = 0)
5150mpteq2dva 4979 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑥𝑋 ↦ 0))
52 fconstmpt 5411 . . . . . . . . . . . . . 14 (𝑋 × {0}) = (𝑥𝑋 ↦ 0)
5351, 52syl6eqr 2832 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ (((ℂ D 𝐹)‘𝑥) − ((ℂ D 𝐹)‘𝑥))) = (𝑋 × {0}))
5434, 48, 533eqtrd 2818 . . . . . . . . . . . 12 (𝜑 → (ℂ D (𝐹𝑓𝐺)) = (𝑋 × {0}))
5554dmeqd 5571 . . . . . . . . . . 11 (𝜑 → dom (ℂ D (𝐹𝑓𝐺)) = dom (𝑋 × {0}))
56 snnzg 4541 . . . . . . . . . . . 12 (0 ∈ ℂ → {0} ≠ ∅)
57 dmxp 5589 . . . . . . . . . . . 12 ({0} ≠ ∅ → dom (𝑋 × {0}) = 𝑋)
5811, 56, 57mp2b 10 . . . . . . . . . . 11 dom (𝑋 × {0}) = 𝑋
5955, 58syl6eq 2830 . . . . . . . . . 10 (𝜑 → dom (ℂ D (𝐹𝑓𝐺)) = 𝑋)
60 eqimss2 3877 . . . . . . . . . 10 (dom (ℂ D (𝐹𝑓𝐺)) = 𝑋𝑋 ⊆ dom (ℂ D (𝐹𝑓𝐺)))
6159, 60syl 17 . . . . . . . . 9 (𝜑𝑋 ⊆ dom (ℂ D (𝐹𝑓𝐺)))
62 0red 10380 . . . . . . . . 9 (𝜑 → 0 ∈ ℝ)
6354fveq1d 6448 . . . . . . . . . . . 12 (𝜑 → ((ℂ D (𝐹𝑓𝐺))‘𝑥) = ((𝑋 × {0})‘𝑥))
64 c0ex 10370 . . . . . . . . . . . . 13 0 ∈ V
6564fvconst2 6741 . . . . . . . . . . . 12 (𝑥𝑋 → ((𝑋 × {0})‘𝑥) = 0)
6663, 65sylan9eq 2834 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ((ℂ D (𝐹𝑓𝐺))‘𝑥) = 0)
6766abs00bd 14438 . . . . . . . . . 10 ((𝜑𝑥𝑋) → (abs‘((ℂ D (𝐹𝑓𝐺))‘𝑥)) = 0)
68 0le0 11483 . . . . . . . . . 10 0 ≤ 0
6967, 68syl6eqbr 4925 . . . . . . . . 9 ((𝜑𝑥𝑋) → (abs‘((ℂ D (𝐹𝑓𝐺))‘𝑥)) ≤ 0)
7028, 16, 24, 25, 5, 61, 62, 69dvlipcn 24194 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝐶𝑋)) → (abs‘(((𝐹𝑓𝐺)‘𝑥) − ((𝐹𝑓𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥𝐶))))
7121, 70syldan 585 . . . . . . 7 ((𝜑𝑥𝑋) → (abs‘(((𝐹𝑓𝐺)‘𝑥) − ((𝐹𝑓𝐺)‘𝐶))) ≤ (0 · (abs‘(𝑥𝐶))))
7233fveq1d 6448 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝑓𝐺)‘𝐶) = ((𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥)))‘𝐶))
73 fveq2 6446 . . . . . . . . . . . . . . 15 (𝑥 = 𝐶 → (𝐹𝑥) = (𝐹𝐶))
74 fveq2 6446 . . . . . . . . . . . . . . 15 (𝑥 = 𝐶 → (𝐺𝑥) = (𝐺𝐶))
7573, 74oveq12d 6940 . . . . . . . . . . . . . 14 (𝑥 = 𝐶 → ((𝐹𝑥) − (𝐺𝑥)) = ((𝐹𝐶) − (𝐺𝐶)))
76 eqid 2778 . . . . . . . . . . . . . 14 (𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥))) = (𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥)))
77 ovex 6954 . . . . . . . . . . . . . 14 ((𝐹𝐶) − (𝐺𝐶)) ∈ V
7875, 76, 77fvmpt 6542 . . . . . . . . . . . . 13 (𝐶𝑋 → ((𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥)))‘𝐶) = ((𝐹𝐶) − (𝐺𝐶)))
7919, 78syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑥𝑋 ↦ ((𝐹𝑥) − (𝐺𝑥)))‘𝐶) = ((𝐹𝐶) − (𝐺𝐶)))
801, 19ffvelrnd 6624 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐶) ∈ ℂ)
81 dv11cn.p . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐶) = (𝐺𝐶))
8280, 81subeq0bd 10801 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝐶) − (𝐺𝐶)) = 0)
8372, 79, 823eqtrd 2818 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑓𝐺)‘𝐶) = 0)
8483adantr 474 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ((𝐹𝑓𝐺)‘𝐶) = 0)
8584oveq2d 6938 . . . . . . . . 9 ((𝜑𝑥𝑋) → (((𝐹𝑓𝐺)‘𝑥) − ((𝐹𝑓𝐺)‘𝐶)) = (((𝐹𝑓𝐺)‘𝑥) − 0))
8617subid1d 10723 . . . . . . . . 9 ((𝜑𝑥𝑋) → (((𝐹𝑓𝐺)‘𝑥) − 0) = ((𝐹𝑓𝐺)‘𝑥))
8785, 86eqtrd 2814 . . . . . . . 8 ((𝜑𝑥𝑋) → (((𝐹𝑓𝐺)‘𝑥) − ((𝐹𝑓𝐺)‘𝐶)) = ((𝐹𝑓𝐺)‘𝑥))
8887fveq2d 6450 . . . . . . 7 ((𝜑𝑥𝑋) → (abs‘(((𝐹𝑓𝐺)‘𝑥) − ((𝐹𝑓𝐺)‘𝐶))) = (abs‘((𝐹𝑓𝐺)‘𝑥)))
8928sselda 3821 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → 𝑥 ∈ ℂ)
9028, 19sseldd 3822 . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℂ)
9190adantr 474 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → 𝐶 ∈ ℂ)
9289, 91subcld 10734 . . . . . . . . . 10 ((𝜑𝑥𝑋) → (𝑥𝐶) ∈ ℂ)
9392abscld 14583 . . . . . . . . 9 ((𝜑𝑥𝑋) → (abs‘(𝑥𝐶)) ∈ ℝ)
9493recnd 10405 . . . . . . . 8 ((𝜑𝑥𝑋) → (abs‘(𝑥𝐶)) ∈ ℂ)
9594mul02d 10574 . . . . . . 7 ((𝜑𝑥𝑋) → (0 · (abs‘(𝑥𝐶))) = 0)
9671, 88, 953brtr3d 4917 . . . . . 6 ((𝜑𝑥𝑋) → (abs‘((𝐹𝑓𝐺)‘𝑥)) ≤ 0)
9717absge0d 14591 . . . . . 6 ((𝜑𝑥𝑋) → 0 ≤ (abs‘((𝐹𝑓𝐺)‘𝑥)))
9817abscld 14583 . . . . . . 7 ((𝜑𝑥𝑋) → (abs‘((𝐹𝑓𝐺)‘𝑥)) ∈ ℝ)
99 0re 10378 . . . . . . 7 0 ∈ ℝ
100 letri3 10462 . . . . . . 7 (((abs‘((𝐹𝑓𝐺)‘𝑥)) ∈ ℝ ∧ 0 ∈ ℝ) → ((abs‘((𝐹𝑓𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹𝑓𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹𝑓𝐺)‘𝑥)))))
10198, 99, 100sylancl 580 . . . . . 6 ((𝜑𝑥𝑋) → ((abs‘((𝐹𝑓𝐺)‘𝑥)) = 0 ↔ ((abs‘((𝐹𝑓𝐺)‘𝑥)) ≤ 0 ∧ 0 ≤ (abs‘((𝐹𝑓𝐺)‘𝑥)))))
10296, 97, 101mpbir2and 703 . . . . 5 ((𝜑𝑥𝑋) → (abs‘((𝐹𝑓𝐺)‘𝑥)) = 0)
10317, 102abs00d 14593 . . . 4 ((𝜑𝑥𝑋) → ((𝐹𝑓𝐺)‘𝑥) = 0)
10465adantl 475 . . . 4 ((𝜑𝑥𝑋) → ((𝑋 × {0})‘𝑥) = 0)
105103, 104eqtr4d 2817 . . 3 ((𝜑𝑥𝑋) → ((𝐹𝑓𝐺)‘𝑥) = ((𝑋 × {0})‘𝑥))
10610, 13, 105eqfnfvd 6577 . 2 (𝜑 → (𝐹𝑓𝐺) = (𝑋 × {0}))
107 ofsubeq0 11371 . . 3 ((𝑋 ∈ V ∧ 𝐹:𝑋⟶ℂ ∧ 𝐺:𝑋⟶ℂ) → ((𝐹𝑓𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺))
1088, 1, 3, 107syl3anc 1439 . 2 (𝜑 → ((𝐹𝑓𝐺) = (𝑋 × {0}) ↔ 𝐹 = 𝐺))
109106, 108mpbid 224 1 (𝜑𝐹 = 𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  wne 2969  Vcvv 3398  wss 3792  c0 4141  {csn 4398  {cpr 4400   class class class wbr 4886  cmpt 4965   × cxp 5353  dom cdm 5355  ccom 5359   Fn wfn 6130  wf 6131  cfv 6135  (class class class)co 6922  𝑓 cof 7172  cc 10270  cr 10271  0cc0 10272   · cmul 10277  *cxr 10410  cle 10412  cmin 10606  abscabs 14381  ∞Metcxmet 20127  ballcbl 20129   D cdv 24064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-hom 16362  df-cco 16363  df-rest 16469  df-topn 16470  df-0g 16488  df-gsum 16489  df-topgen 16490  df-pt 16491  df-prds 16494  df-xrs 16548  df-qtop 16553  df-imas 16554  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-fbas 20139  df-fg 20140  df-cnfld 20143  df-top 21106  df-topon 21123  df-topsp 21145  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-lp 21348  df-perf 21349  df-cn 21439  df-cnp 21440  df-haus 21527  df-cmp 21599  df-tx 21774  df-hmeo 21967  df-fil 22058  df-fm 22150  df-flim 22151  df-flf 22152  df-xms 22533  df-ms 22534  df-tms 22535  df-cncf 23089  df-limc 24067  df-dv 24068
This theorem is referenced by:  logtayl  24843  binomcxplemnotnn0  39511
  Copyright terms: Public domain W3C validator