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

Theorem dvcnp2cntop 14166
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 3166 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐴 βŠ† β„‚)
6 simpl2 1001 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐹:π΄βŸΆβ„‚)
71cntoptop 14036 . . . . . . . 8 𝐾 ∈ Top
8 cnex 7935 . . . . . . . . 9 β„‚ ∈ V
9 ssexg 4143 . . . . . . . . 9 ((𝑆 βŠ† β„‚ ∧ β„‚ ∈ V) β†’ 𝑆 ∈ V)
104, 8, 9sylancl 413 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑆 ∈ V)
11 resttop 13673 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑆 ∈ V) β†’ (𝐾 β†Ύt 𝑆) ∈ Top)
127, 10, 11sylancr 414 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐾 β†Ύt 𝑆) ∈ Top)
131cntoptopon 14035 . . . . . . . . . 10 𝐾 ∈ (TopOnβ€˜β„‚)
14 resttopon 13674 . . . . . . . . . 10 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ 𝑆 βŠ† β„‚) β†’ (𝐾 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
1513, 4, 14sylancr 414 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐾 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
16 toponuni 13518 . . . . . . . . 9 ((𝐾 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†) β†’ 𝑆 = βˆͺ (𝐾 β†Ύt 𝑆))
1715, 16syl 14 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑆 = βˆͺ (𝐾 β†Ύt 𝑆))
183, 17sseqtrd 3194 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐴 βŠ† βˆͺ (𝐾 β†Ύt 𝑆))
19 eqid 2177 . . . . . . . 8 βˆͺ (𝐾 β†Ύt 𝑆) = βˆͺ (𝐾 β†Ύt 𝑆)
2019ntrss2 13624 . . . . . . 7 (((𝐾 β†Ύt 𝑆) ∈ Top ∧ 𝐴 βŠ† βˆͺ (𝐾 β†Ύt 𝑆)) β†’ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄) βŠ† 𝐴)
2112, 18, 20syl2anc 411 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄) βŠ† 𝐴)
22 eqid 2177 . . . . . . . 8 (𝐾 β†Ύt 𝑆) = (𝐾 β†Ύt 𝑆)
23 eqid 2177 . . . . . . . 8 (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡))) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)))
24 simp1 997 . . . . . . . 8 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ 𝑆 βŠ† β„‚)
25 simp2 998 . . . . . . . 8 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ 𝐹:π΄βŸΆβ„‚)
26 simp3 999 . . . . . . . 8 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ 𝐴 βŠ† 𝑆)
2722, 1, 23, 24, 25, 26eldvap 14154 . . . . . . 7 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ (𝐡(𝑆 D 𝐹)𝑦 ↔ (𝐡 ∈ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄) ∧ 𝑦 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡))))
2827simprbda 383 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐡 ∈ ((intβ€˜(𝐾 β†Ύt 𝑆))β€˜π΄))
2921, 28sseldd 3157 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐡 ∈ 𝐴)
306ffvelcdmda 5652 . . . . . . . 8 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) ∈ β„‚)
316, 29ffvelcdmd 5653 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (πΉβ€˜π΅) ∈ β„‚)
3231adantr 276 . . . . . . . 8 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π΅) ∈ β„‚)
3330, 32subcld 8268 . . . . . . 7 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) ∈ β„‚)
34 ssid 3176 . . . . . . . 8 β„‚ βŠ† β„‚
3534a1i 9 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ β„‚ βŠ† β„‚)
36 txtopon 13765 . . . . . . . . 9 ((𝐾 ∈ (TopOnβ€˜β„‚) ∧ 𝐾 ∈ (TopOnβ€˜β„‚)) β†’ (𝐾 Γ—t 𝐾) ∈ (TopOnβ€˜(β„‚ Γ— β„‚)))
3713, 13, 36mp2an 426 . . . . . . . 8 (𝐾 Γ—t 𝐾) ∈ (TopOnβ€˜(β„‚ Γ— β„‚))
3837toponrestid 13524 . . . . . . 7 (𝐾 Γ—t 𝐾) = ((𝐾 Γ—t 𝐾) β†Ύt (β„‚ Γ— β„‚))
396, 5, 29dvlemap 14152 . . . . . . . . . 10 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) ∈ β„‚)
40 ssrab2 3241 . . . . . . . . . . . . 13 {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† 𝐴
4140, 5sstrid 3167 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† β„‚)
4241sselda 3156 . . . . . . . . . . 11 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 ∈ β„‚)
435, 29sseldd 3157 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐡 ∈ β„‚)
4443adantr 276 . . . . . . . . . . 11 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝐡 ∈ β„‚)
4542, 44subcld 8268 . . . . . . . . . 10 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (𝑧 βˆ’ 𝐡) ∈ β„‚)
4627simplbda 384 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑦 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡))
47 limcresi 14138 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡) βŠ† (((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡)
48 resmpt 4956 . . . . . . . . . . . . . 14 ({𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† 𝐴 β†’ ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)))
4940, 48ax-mp 5 . . . . . . . . . . . . 13 ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡))
5049oveq1i 5885 . . . . . . . . . . . 12 (((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡)
5147, 50sseqtri 3190 . . . . . . . . . . 11 ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡) βŠ† ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡)
5243subidd 8256 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐡 βˆ’ 𝐡) = 0)
531subcncntop 14056 . . . . . . . . . . . . . . 15 βˆ’ ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾)
5453a1i 9 . . . . . . . . . . . . . 14 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ βˆ’ ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾))
55 cncfmptid 14086 . . . . . . . . . . . . . . 15 ((𝐴 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cnβ†’β„‚))
565, 34, 55sylancl 413 . . . . . . . . . . . . . 14 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cnβ†’β„‚))
57 cncfmptc 14085 . . . . . . . . . . . . . . 15 ((𝐡 ∈ β„‚ ∧ 𝐴 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝐴 ↦ 𝐡) ∈ (𝐴–cnβ†’β„‚))
5843, 5, 35, 57syl3anc 1238 . . . . . . . . . . . . . 14 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ 𝐡) ∈ (𝐴–cnβ†’β„‚))
591, 54, 56, 58cncfmpt2fcntop 14088 . . . . . . . . . . . . 13 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) ∈ (𝐴–cnβ†’β„‚))
60 oveq1 5882 . . . . . . . . . . . . 13 (𝑧 = 𝐡 β†’ (𝑧 βˆ’ 𝐡) = (𝐡 βˆ’ 𝐡))
6159, 29, 60cnmptlimc 14146 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝐡 βˆ’ 𝐡) ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡))
6252, 61eqeltrrd 2255 . . . . . . . . . . 11 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡))
6351, 62sselid 3154 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ (𝑧 βˆ’ 𝐡)) limβ„‚ 𝐡))
641mulcncntop 14057 . . . . . . . . . . 11 Β· ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾)
6524, 25, 26dvcl 14155 . . . . . . . . . . . 12 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝑦 ∈ β„‚)
66 0cn 7949 . . . . . . . . . . . 12 0 ∈ β„‚
67 opelxpi 4659 . . . . . . . . . . . 12 ((𝑦 ∈ β„‚ ∧ 0 ∈ β„‚) β†’ βŸ¨π‘¦, 0⟩ ∈ (β„‚ Γ— β„‚))
6865, 66, 67sylancl 413 . . . . . . . . . . 11 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ βŸ¨π‘¦, 0⟩ ∈ (β„‚ Γ— β„‚))
6937toponunii 13520 . . . . . . . . . . . 12 (β„‚ Γ— β„‚) = βˆͺ (𝐾 Γ—t 𝐾)
7069cncnpi 13731 . . . . . . . . . . 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 14149 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑦 Β· 0) ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡))
7365mul01d 8350 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑦 Β· 0) = 0)
746adantr 276 . . . . . . . . . . . . . 14 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝐹:π΄βŸΆβ„‚)
75 simpr 110 . . . . . . . . . . . . . . 15 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡})
7640, 75sselid 3154 . . . . . . . . . . . . . 14 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 ∈ 𝐴)
7774, 76ffvelcdmd 5653 . . . . . . . . . . . . 13 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (πΉβ€˜π‘§) ∈ β„‚)
7831adantr 276 . . . . . . . . . . . . 13 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (πΉβ€˜π΅) ∈ β„‚)
7977, 78subcld 8268 . . . . . . . . . . . 12 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) ∈ β„‚)
80 breq1 4007 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑧 β†’ (𝑀 # 𝐡 ↔ 𝑧 # 𝐡))
8180elrab 2894 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 # 𝐡))
8281simprbi 275 . . . . . . . . . . . . . 14 (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} β†’ 𝑧 # 𝐡)
8382adantl 277 . . . . . . . . . . . . 13 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ 𝑧 # 𝐡)
8442, 44, 83subap0d 8601 . . . . . . . . . . . 12 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ (𝑧 βˆ’ 𝐡) # 0)
8579, 45, 84divcanap1d 8748 . . . . . . . . . . 11 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡)) = ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)))
8685mpteq2dva 4094 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡))) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))))
8786oveq1d 5890 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) / (𝑧 βˆ’ 𝐡)) Β· (𝑧 βˆ’ 𝐡))) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
8872, 73, 873eltr3d 2260 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
8933fmpttd 5672 . . . . . . . . . 10 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))):π΄βŸΆβ„‚)
9089, 5limcdifap 14134 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡) = (((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡))
91 resmpt 4956 . . . . . . . . . . 11 ({𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} βŠ† 𝐴 β†’ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))))
9240, 91ax-mp 5 . . . . . . . . . 10 ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) = (𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)))
9392oveq1i 5885 . . . . . . . . 9 (((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) β†Ύ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡}) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡)
9490, 93eqtrdi 2226 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡) = ((𝑧 ∈ {𝑀 ∈ 𝐴 ∣ 𝑀 # 𝐡} ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
9588, 94eleqtrrd 2257 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 0 ∈ ((𝑧 ∈ 𝐴 ↦ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅))) limβ„‚ 𝐡))
96 cncfmptc 14085 . . . . . . . . 9 (((πΉβ€˜π΅) ∈ β„‚ ∧ 𝐴 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π΅)) ∈ (𝐴–cnβ†’β„‚))
9731, 5, 35, 96syl3anc 1238 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π΅)) ∈ (𝐴–cnβ†’β„‚))
98 eqidd 2178 . . . . . . . 8 (𝑧 = 𝐡 β†’ (πΉβ€˜π΅) = (πΉβ€˜π΅))
9997, 29, 98cnmptlimc 14146 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (πΉβ€˜π΅) ∈ ((𝑧 ∈ 𝐴 ↦ (πΉβ€˜π΅)) limβ„‚ 𝐡))
1001addcncntop 14055 . . . . . . . 8 + ∈ ((𝐾 Γ—t 𝐾) Cn 𝐾)
101 opelxpi 4659 . . . . . . . . 9 ((0 ∈ β„‚ ∧ (πΉβ€˜π΅) ∈ β„‚) β†’ ⟨0, (πΉβ€˜π΅)⟩ ∈ (β„‚ Γ— β„‚))
10266, 31, 101sylancr 414 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ⟨0, (πΉβ€˜π΅)⟩ ∈ (β„‚ Γ— β„‚))
10369cncnpi 13731 . . . . . . . 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 14149 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (0 + (πΉβ€˜π΅)) ∈ ((𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) limβ„‚ 𝐡))
10631addid2d 8107 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (0 + (πΉβ€˜π΅)) = (πΉβ€˜π΅))
10730, 32npcand 8272 . . . . . . . . 9 ((((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅)) = (πΉβ€˜π‘§))
108107mpteq2dva 4094 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) = (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π‘§)))
1096feqmptd 5570 . . . . . . . 8 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐹 = (𝑧 ∈ 𝐴 ↦ (πΉβ€˜π‘§)))
110108, 109eqtr4d 2213 . . . . . . 7 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) = 𝐹)
111110oveq1d 5890 . . . . . 6 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ ((𝑧 ∈ 𝐴 ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜π΅)) + (πΉβ€˜π΅))) limβ„‚ 𝐡) = (𝐹 limβ„‚ 𝐡))
112105, 106, 1113eltr3d 2260 . . . . 5 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ (πΉβ€˜π΅) ∈ (𝐹 limβ„‚ 𝐡))
1131, 2, 5, 6, 29, 112cnplimclemr 14141 . . . 4 (((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) ∧ 𝐡(𝑆 D 𝐹)𝑦) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅))
114113ex 115 . . 3 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ (𝐡(𝑆 D 𝐹)𝑦 β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅)))
115114exlimdv 1819 . 2 ((𝑆 βŠ† β„‚ ∧ 𝐹:π΄βŸΆβ„‚ ∧ 𝐴 βŠ† 𝑆) β†’ (βˆƒπ‘¦ 𝐡(𝑆 D 𝐹)𝑦 β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΅)))
116 eldmg 4823 . . 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 1492   ∈ wcel 2148  {crab 2459  Vcvv 2738   βŠ† wss 3130  βŸ¨cop 3596  βˆͺ cuni 3810   class class class wbr 4004   ↦ cmpt 4065   Γ— cxp 4625  dom cdm 4627   β†Ύ cres 4629   ∘ ccom 4631  βŸΆwf 5213  β€˜cfv 5217  (class class class)co 5875  β„‚cc 7809  0cc0 7811   + caddc 7814   Β· cmul 7816   βˆ’ cmin 8128   # cap 8538   / cdiv 8629  abscabs 11006   β†Ύt crest 12688  MetOpencmopn 13448  Topctop 13500  TopOnctopon 13513  intcnt 13596   Cn ccn 13688   CnP ccnp 13689   Γ—t ctx 13755  β€“cnβ†’ccncf 14060   limβ„‚ climc 14126   D cdv 14127
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-mulrcl 7910  ax-addcom 7911  ax-mulcom 7912  ax-addass 7913  ax-mulass 7914  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-1rid 7918  ax-0id 7919  ax-rnegex 7920  ax-precex 7921  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-apti 7926  ax-pre-ltadd 7927  ax-pre-mulgt0 7928  ax-pre-mulext 7929  ax-arch 7930  ax-caucvg 7931  ax-addf 7933  ax-mulf 7934
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 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-po 4297  df-iso 4298  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-isom 5226  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-frec 6392  df-map 6650  df-pm 6651  df-sup 6983  df-inf 6984  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-reap 8532  df-ap 8539  df-div 8630  df-inn 8920  df-2 8978  df-3 8979  df-4 8980  df-n0 9177  df-z 9254  df-uz 9529  df-q 9620  df-rp 9654  df-xneg 9772  df-xadd 9773  df-seqfrec 10446  df-exp 10520  df-cj 10851  df-re 10852  df-im 10853  df-rsqrt 11007  df-abs 11008  df-rest 12690  df-topgen 12709  df-psmet 13450  df-xmet 13451  df-met 13452  df-bl 13453  df-mopn 13454  df-top 13501  df-topon 13514  df-bases 13546  df-ntr 13599  df-cn 13691  df-cnp 13692  df-tx 13756  df-cncf 14061  df-limced 14128  df-dvap 14129
This theorem is referenced by:  dvcn  14167  dvmulxxbr  14169  dvcoapbr  14174
  Copyright terms: Public domain W3C validator