ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvcnp2cntop GIF version

Theorem dvcnp2cntop 13656
Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
dvcnp.j 𝐽 = (𝐾 β†Ύt 𝐴)
dvcnpcntop.k 𝐾 = (MetOpenβ€˜(abs ∘ βˆ’ ))
Assertion
Ref Expression
dvcnp2cntop (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡 ∈ dom (𝑆 D 𝐹)) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅))

Proof of Theorem dvcnp2cntop
Dummy variables 𝑦 𝑧 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvcnpcntop.k . . . . 5 𝐾 = (MetOpenβ€˜(abs ∘ βˆ’ ))
2 dvcnp.j . . . . 5 𝐽 = (𝐾 β†Ύt 𝐴)
3 simpl3 1002 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐴 βŠ† 𝑆)
4 simpl1 1000 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑆 βŠ† β„‚)
53, 4sstrd 3163 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐴 βŠ† β„‚)
6 simpl2 1001 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐹:π΄βŸΆβ„‚)
71cntoptop 13526 . . . . . . . 8 𝐾 ∈ Top
8 cnex 7910 . . . . . . . . 9 β„‚ ∈ V
9 ssexg 4137 . . . . . . . . 9 ((𝑆 βŠ† β„‚ ∧ β„‚ ∈ V) β†’ 𝑆 ∈ V)
104, 8, 9sylancl 413 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑆 ∈ V)
11 resttop 13163 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑆 ∈ V) β†’ (𝐾 β†Ύt 𝑆) ∈ Top)
127, 10, 11sylancr 414 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐾 β†Ύt 𝑆) ∈ Top)
131cntoptopon 13525 . . . . . . . . . 10 𝐾 ∈ (TopOnβ€˜β„‚)
14 resttopon 13164 . . . . . . . . . 10 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ 𝑆 βŠ† β„‚) β†’ (𝐾 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
1513, 4, 14sylancr 414 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐾 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
16 toponuni 13006 . . . . . . . . 9 ((𝐾 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†) β†’ 𝑆 = βˆͺ (𝐾 β†Ύt 𝑆))
1715, 16syl 14 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑆 = βˆͺ (𝐾 β†Ύt 𝑆))
183, 17sseqtrd 3191 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐴 βŠ† βˆͺ (𝐾 β†Ύt 𝑆))
19 eqid 2175 . . . . . . . 8 βˆͺ (𝐾 β†Ύt 𝑆) = βˆͺ (𝐾 β†Ύt 𝑆)
2019ntrss2 13114 . . . . . . 7 (((𝐾 β†Ύt 𝑆) ∈ Top ∧ 𝐴 βŠ† βˆͺ (𝐾 β†Ύt 𝑆)) β†’ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄) βŠ† 𝐴)
2112, 18, 20syl2anc 411 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄) βŠ† 𝐴)
22 eqid 2175 . . . . . . . 8 (𝐾 β†Ύt 𝑆) = (𝐾 β†Ύt 𝑆)
23 eqid 2175 . . . . . . . 8 (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡))) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)))
24 simp1 997 . . . . . . . 8 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ 𝑆 βŠ† β„‚)
25 simp2 998 . . . . . . . 8 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ 𝐹:π΄βŸΆβ„‚)
26 simp3 999 . . . . . . . 8 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ 𝐴 βŠ† 𝑆)
2722, 1, 23, 24, 25, 26eldvap 13644 . . . . . . 7 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ (𝐡(𝑆 D 𝐹)𝑦 ↔ (𝐡 ∈ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄) ∧ 𝑦 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡))))
2827simprbda 383 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐡 ∈ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄))
2921, 28sseldd 3154 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐡 ∈ 𝐴)
306ffvelcdmda 5643 . . . . . . . 8 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) ∈ β„‚)
316, 29ffvelrnd 5644 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (πΉβ€˜π΅) ∈ β„‚)
3231adantr 276 . . . . . . . 8 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π΅) ∈ β„‚)
3330, 32subcld 8242 . . . . . . 7 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) ∈ β„‚)
34 ssid 3173 . . . . . . . 8 β„‚ βŠ† β„‚
3534a1i 9 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ β„‚ βŠ† β„‚)
36 txtopon 13255 . . . . . . . . 9 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ 𝐾 ∈ (TopOnβ€˜β„‚)) β†’ (𝐾 Γ—t 𝐾) ∈ (TopOnβ€˜(β„‚ Γ— β„‚)))
3713, 13, 36mp2an 426 . . . . . . . 8 (𝐾 Γ—t 𝐾) ∈ (TopOnβ€˜(β„‚ Γ— β„‚))
3837toponrestid 13012 . . . . . . 7 (𝐾 Γ—t 𝐾) = ((𝐾 Γ—t 𝐾) β†Ύt (β„‚ Γ— β„‚))
396, 5, 29dvlemap 13642 . . . . . . . . . 10 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) ∈ β„‚)
40 ssrab2 3238 . . . . . . . . . . . . 13 {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† 𝐴
4140, 5sstrid 3164 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† β„‚)
4241sselda 3153 . . . . . . . . . . 11 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 ∈ β„‚)
435, 29sseldd 3154 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐡 ∈ β„‚)
4443adantr 276 . . . . . . . . . . 11 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝐡 ∈ β„‚)
4542, 44subcld 8242 . . . . . . . . . 10 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (𝑧 βˆ’ 𝐡) ∈ β„‚)
4627simplbda 384 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑦 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡))
47 limcresi 13628 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡) βŠ† (((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡)
48 resmpt 4948 . . . . . . . . . . . . . 14 ({𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† 𝐴 β†’ ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)))
4940, 48ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡))
5049oveq1i 5875 . . . . . . . . . . . 12 (((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡)
5147, 50sseqtri 3187 . . . . . . . . . . 11 ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡) βŠ† ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡)
5243subidd 8230 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐡 βˆ’ 𝐡) = 0)
531subcncntop 13546 . . . . . . . . . . . . . . 15 βˆ’ ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾)
5453a1i 9 . . . . . . . . . . . . . 14 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ βˆ’ ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾))
55 cncfmptid 13576 . . . . . . . . . . . . . . 15 ((𝐴 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cnβ†’β„‚))
565, 34, 55sylancl 413 . . . . . . . . . . . . . 14 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cnβ†’β„‚))
57 cncfmptc 13575 . . . . . . . . . . . . . . 15 ((𝐡 ∈ β„‚ ∧ 𝐴 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝐴 ↦ 𝐡) ∈ (𝐴–cnβ†’β„‚))
5843, 5, 35, 57syl3anc 1238 . . . . . . . . . . . . . 14 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ 𝐡) ∈ (𝐴–cnβ†’β„‚))
591, 54, 56, 58cncfmpt2fcntop 13578 . . . . . . . . . . . . 13 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) ∈ (𝐴–cnβ†’β„‚))
60 oveq1 5872 . . . . . . . . . . . . 13 (𝑧 = 𝐡 β†’ (𝑧 βˆ’ 𝐡) = (𝐡 βˆ’ 𝐡))
6159, 29, 60cnmptlimc 13636 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐡 βˆ’ 𝐡) ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡))
6252, 61eqeltrrd 2253 . . . . . . . . . . 11 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡))
6351, 62sselid 3151 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡))
641mulcncntop 13547 . . . . . . . . . . 11 Β· ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾)
6524, 25, 26dvcl 13645 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑦 ∈ β„‚)
66 0cn 7924 . . . . . . . . . . . 12 0 ∈ β„‚
67 opelxpi 4652 . . . . . . . . . . . 12 ((𝑦 ∈ β„‚ ∧ 0 ∈ β„‚) β†’ βŸ¨π‘¦, 0⟩ ∈ (β„‚ Γ— β„‚))
6865, 66, 67sylancl 413 . . . . . . . . . . 11 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ βŸ¨π‘¦, 0⟩ ∈ (β„‚ Γ— β„‚))
6937toponunii 13008 . . . . . . . . . . . 12 (β„‚ Γ— β„‚) = βˆͺ (𝐾 Γ—t 𝐾)
7069cncnpi 13221 . . . . . . . . . . 11 (( Β· ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾) ∧ βŸ¨π‘¦, 0⟩ ∈ (β„‚ Γ— β„‚)) β†’ Β· ∈ (((𝐾 Γ—t 𝐾) CnP 𝐾)β€˜βŸ¨π‘¦, 0⟩))
7164, 68, 70sylancr 414 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ Β· ∈ (((𝐾 Γ—t 𝐾) CnP 𝐾)β€˜βŸ¨π‘¦, 0⟩))
7239, 45, 35, 35, 1, 38, 46, 63, 71limccnp2cntop 13639 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑦 Β· 0) ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡))
7365mul01d 8324 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑦 Β· 0) = 0)
746adantr 276 . . . . . . . . . . . . . 14 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝐹:π΄βŸΆβ„‚)
75 simpr 110 . . . . . . . . . . . . . . 15 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡})
7640, 75sselid 3151 . . . . . . . . . . . . . 14 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 ∈ 𝐴)
7774, 76ffvelrnd 5644 . . . . . . . . . . . . 13 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (πΉβ€˜π‘§) ∈ β„‚)
7831adantr 276 . . . . . . . . . . . . 13 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (πΉβ€˜π΅) ∈ β„‚)
7977, 78subcld 8242 . . . . . . . . . . . 12 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) ∈ β„‚)
80 breq1 4001 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑧 β†’ (𝑀 # 𝐡 ↔ 𝑧 # 𝐡))
8180elrab 2891 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 # 𝐡))
8281simprbi 275 . . . . . . . . . . . . . 14 (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} β†’ 𝑧 # 𝐡)
8382adantl 277 . . . . . . . . . . . . 13 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 # 𝐡)
8442, 44, 83subap0d 8575 . . . . . . . . . . . 12 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (𝑧 βˆ’ 𝐡) # 0)
8579, 45, 84divcanap1d 8720 . . . . . . . . . . 11 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡)) = ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)))
8685mpteq2dva 4088 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡))) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))))
8786oveq1d 5880 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
8872, 73, 873eltr3d 2258 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
8933fmpttd 5663 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))):π΄βŸΆβ„‚)
9089, 5limcdifap 13624 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡) = (((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡))
91 resmpt 4948 . . . . . . . . . . 11 ({𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† 𝐴 β†’ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))))
9240, 91ax-mp 5 . . . . . . . . . 10 ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)))
9392oveq1i 5875 . . . . . . . . 9 (((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡)
9490, 93eqtrdi 2224 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
9588, 94eleqtrrd 2255 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
96 cncfmptc 13575 . . . . . . . . 9 (((πΉβ€˜π΅) ∈ β„‚ ∧ 𝐴 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π΅)) ∈ (𝐴–cnβ†’β„‚))
9731, 5, 35, 96syl3anc 1238 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π΅)) ∈ (𝐴–cnβ†’β„‚))
98 eqidd 2176 . . . . . . . 8 (𝑧 = 𝐡 β†’ (πΉβ€˜π΅) = (πΉβ€˜π΅))
9997, 29, 98cnmptlimc 13636 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (πΉβ€˜π΅) ∈ ((𝑧 ∈ 𝐴 ↦ (πΉβ€˜π΅)) limβ„‚ 𝐡))
1001addcncntop 13545 . . . . . . . 8 + ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾)
101 opelxpi 4652 . . . . . . . . 9 ((0 ∈ β„‚ ∧ (πΉβ€˜π΅) ∈ β„‚) β†’ ⟨0, (πΉβ€˜π΅)⟩ ∈ (β„‚ Γ— β„‚))
10266, 31, 101sylancr 414 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ⟨0, (πΉβ€˜π΅)⟩ ∈ (β„‚ Γ— β„‚))
10369cncnpi 13221 . . . . . . . 8 (( + ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾) ∧ ⟨0, (πΉβ€˜π΅)⟩ ∈ (β„‚ Γ— β„‚)) β†’ + ∈ (((𝐾 Γ—t 𝐾) CnP 𝐾)β€˜βŸ¨0, (πΉβ€˜π΅)⟩))
104100, 102, 103sylancr 414 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ + ∈ (((𝐾 Γ—t 𝐾) CnP 𝐾)β€˜βŸ¨0, (πΉβ€˜π΅)⟩))
10533, 32, 35, 35, 1, 38, 95, 99, 104limccnp2cntop 13639 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (0 + (πΉβ€˜π΅)) ∈ ((𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) limβ„‚ 𝐡))
10631addid2d 8081 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (0 + (πΉβ€˜π΅)) = (πΉβ€˜π΅))
10730, 32npcand 8246 . . . . . . . . 9 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅)) = (πΉβ€˜π‘§))
108107mpteq2dva 4088 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) = (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π‘§)))
1096feqmptd 5561 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐹 = (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π‘§)))
110108, 109eqtr4d 2211 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) = 𝐹)
111110oveq1d 5880 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) limβ„‚ 𝐡) = (𝐹 limβ„‚ 𝐡))
112105, 106, 1113eltr3d 2258 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (πΉβ€˜π΅) ∈ (𝐹 limβ„‚ 𝐡))
1131, 2, 5, 6, 29, 112cnplimclemr 13631 . . . 4 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅))
114113ex 115 . . 3 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ (𝐡(𝑆 D 𝐹)𝑦 β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅)))
115114exlimdv 1817 . 2 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ (βˆƒπ‘¦ 𝐡(𝑆 D 𝐹)𝑦 β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅)))
116 eldmg 4815 . . 3 (𝐡 ∈ dom (𝑆 D 𝐹) β†’ (𝐡 ∈ dom (𝑆 D 𝐹) ↔ βˆƒπ‘¦ 𝐡(𝑆 D 𝐹)𝑦))
117116ibi 176 . 2 (𝐡 ∈ dom (𝑆 D 𝐹) β†’ βˆƒπ‘¦ 𝐡(𝑆 D 𝐹)𝑦)
118115, 117impel 280 1 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡 ∈ dom (𝑆 D 𝐹)) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ∧ w3a 978   = wceq 1353  βˆƒwex 1490   ∈ wcel 2146  {crab 2457  Vcvv 2735   βŠ† wss 3127  βŸ¨cop 3592  βˆͺ cuni 3805   class class class wbr 3998   ↦ cmpt 4059   Γ— cxp 4618  dom cdm 4620   β†Ύ cres 4622   ∘ ccom 4624  βŸΆwf 5204  β€˜cfv 5208  (class class class)co 5865  β„‚cc 7784  0cc0 7786   + caddc 7789   Β· cmul 7791   βˆ’ cmin 8102   # cap 8512   / cdiv 8601  abscabs 10973   β†Ύt crest 12609  MetOpencmopn 12978  Topctop 12988  TopOnctopon 13001  intcnt 13086   Cn ccn 13178   CnP ccnp 13179   Γ—t ctx 13245  β€“cnβ†’ccncf 13550   limβ„‚ climc 13616   D cdv 13617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-mulrcl 7885  ax-addcom 7886  ax-mulcom 7887  ax-addass 7888  ax-mulass 7889  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-1rid 7893  ax-0id 7894  ax-rnegex 7895  ax-precex 7896  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-apti 7901  ax-pre-ltadd 7902  ax-pre-mulgt0 7903  ax-pre-mulext 7904  ax-arch 7905  ax-caucvg 7906  ax-addf 7908  ax-mulf 7909
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rmo 2461  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-if 3533  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-po 4290  df-iso 4291  df-iord 4360  df-on 4362  df-ilim 4363  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-isom 5217  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-recs 6296  df-frec 6382  df-map 6640  df-pm 6641  df-sup 6973  df-inf 6974  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-reap 8506  df-ap 8513  df-div 8602  df-inn 8891  df-2 8949  df-3 8950  df-4 8951  df-n0 9148  df-z 9225  df-uz 9500  df-q 9591  df-rp 9623  df-xneg 9741  df-xadd 9742  df-seqfrec 10414  df-exp 10488  df-cj 10818  df-re 10819  df-im 10820  df-rsqrt 10974  df-abs 10975  df-rest 12611  df-topgen 12630  df-psmet 12980  df-xmet 12981  df-met 12982  df-bl 12983  df-mopn 12984  df-top 12989  df-topon 13002  df-bases 13034  df-ntr 13089  df-cn 13181  df-cnp 13182  df-tx 13246  df-cncf 13551  df-limced 13618  df-dvap 13619
This theorem is referenced by:  dvcn  13657  dvmulxxbr  13659  dvcoapbr  13664
  Copyright terms: Public domain W3C validator