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

Theorem dvmulxxbr 14393
Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 14395. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
Hypotheses
Ref Expression
dvadd.f (πœ‘ β†’ 𝐹:π‘‹βŸΆβ„‚)
dvadd.x (πœ‘ β†’ 𝑋 βŠ† 𝑆)
dvaddxx.g (πœ‘ β†’ 𝐺:π‘‹βŸΆβ„‚)
dvaddbr.s (πœ‘ β†’ 𝑆 βŠ† β„‚)
dvadd.bf (πœ‘ β†’ 𝐢(𝑆 D 𝐹)𝐾)
dvadd.bg (πœ‘ β†’ 𝐢(𝑆 D 𝐺)𝐿)
dvaddcntop.j 𝐽 = (MetOpenβ€˜(abs ∘ βˆ’ ))
Assertion
Ref Expression
dvmulxxbr (πœ‘ β†’ 𝐢(𝑆 D (𝐹 βˆ˜π‘“ Β· 𝐺))((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))))

Proof of Theorem dvmulxxbr
Dummy variables 𝑦 𝑧 π‘₯ 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvadd.bf . . . 4 (πœ‘ β†’ 𝐢(𝑆 D 𝐹)𝐾)
2 eqid 2187 . . . . 5 (𝐽 β†Ύt 𝑆) = (𝐽 β†Ύt 𝑆)
3 dvaddcntop.j . . . . 5 𝐽 = (MetOpenβ€˜(abs ∘ βˆ’ ))
4 eqid 2187 . . . . 5 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
5 dvaddbr.s . . . . 5 (πœ‘ β†’ 𝑆 βŠ† β„‚)
6 dvadd.f . . . . 5 (πœ‘ β†’ 𝐹:π‘‹βŸΆβ„‚)
7 dvadd.x . . . . 5 (πœ‘ β†’ 𝑋 βŠ† 𝑆)
82, 3, 4, 5, 6, 7eldvap 14378 . . . 4 (πœ‘ β†’ (𝐢(𝑆 D 𝐹)𝐾 ↔ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐾 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))))
91, 8mpbid 147 . . 3 (πœ‘ β†’ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐾 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢)))
109simpld 112 . 2 (πœ‘ β†’ 𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹))
117, 5sstrd 3177 . . . . . 6 (πœ‘ β†’ 𝑋 βŠ† β„‚)
123cntoptopon 14259 . . . . . . . . . 10 𝐽 ∈ (TopOnβ€˜β„‚)
13 resttopon 13898 . . . . . . . . . 10 ((𝐽 ∈ (TopOnβ€˜β„‚) ∧ 𝑆 βŠ† β„‚) β†’ (𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
1412, 5, 13sylancr 414 . . . . . . . . 9 (πœ‘ β†’ (𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
15 topontop 13741 . . . . . . . . 9 ((𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†) β†’ (𝐽 β†Ύt 𝑆) ∈ Top)
1614, 15syl 14 . . . . . . . 8 (πœ‘ β†’ (𝐽 β†Ύt 𝑆) ∈ Top)
17 toponuni 13742 . . . . . . . . . 10 ((𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†) β†’ 𝑆 = βˆͺ (𝐽 β†Ύt 𝑆))
1814, 17syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝑆 = βˆͺ (𝐽 β†Ύt 𝑆))
197, 18sseqtrd 3205 . . . . . . . 8 (πœ‘ β†’ 𝑋 βŠ† βˆͺ (𝐽 β†Ύt 𝑆))
20 eqid 2187 . . . . . . . . 9 βˆͺ (𝐽 β†Ύt 𝑆) = βˆͺ (𝐽 β†Ύt 𝑆)
2120ntrss2 13848 . . . . . . . 8 (((𝐽 β†Ύt 𝑆) ∈ Top ∧ 𝑋 βŠ† βˆͺ (𝐽 β†Ύt 𝑆)) β†’ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) βŠ† 𝑋)
2216, 19, 21syl2anc 411 . . . . . . 7 (πœ‘ β†’ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) βŠ† 𝑋)
2322, 10sseldd 3168 . . . . . 6 (πœ‘ β†’ 𝐢 ∈ 𝑋)
246, 11, 23dvlemap 14376 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) ∈ β„‚)
25 dvaddxx.g . . . . . . 7 (πœ‘ β†’ 𝐺:π‘‹βŸΆβ„‚)
2625adantr 276 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐺:π‘‹βŸΆβ„‚)
27 elrabi 2902 . . . . . . 7 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} β†’ 𝑧 ∈ 𝑋)
2827adantl 277 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 ∈ 𝑋)
2926, 28ffvelcdmd 5665 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΊβ€˜π‘§) ∈ β„‚)
3024, 29mulcld 7991 . . . 4 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) ∈ β„‚)
3125, 11, 23dvlemap 14376 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) ∈ β„‚)
326, 23ffvelcdmd 5665 . . . . . 6 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ β„‚)
3332adantr 276 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΉβ€˜πΆ) ∈ β„‚)
3431, 33mulcld 7991 . . . 4 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)) ∈ β„‚)
35 ssidd 3188 . . . 4 (πœ‘ β†’ β„‚ βŠ† β„‚)
36 txtopon 13989 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜β„‚) ∧ 𝐽 ∈ (TopOnβ€˜β„‚)) β†’ (𝐽 Γ—t 𝐽) ∈ (TopOnβ€˜(β„‚ Γ— β„‚)))
3712, 12, 36mp2an 426 . . . . 5 (𝐽 Γ—t 𝐽) ∈ (TopOnβ€˜(β„‚ Γ— β„‚))
3837toponrestid 13748 . . . 4 (𝐽 Γ—t 𝐽) = ((𝐽 Γ—t 𝐽) β†Ύt (β„‚ Γ— β„‚))
399simprd 114 . . . . 5 (πœ‘ β†’ 𝐾 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))
40 cnex 7948 . . . . . . . . . . . . 13 β„‚ ∈ V
4140a1i 9 . . . . . . . . . . . 12 (πœ‘ β†’ β„‚ ∈ V)
4241, 5ssexd 4155 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 ∈ V)
43 elpm2r 6679 . . . . . . . . . . . 12 (((β„‚ ∈ V ∧ 𝑆 ∈ V) ∧ (𝐺:π‘‹βŸΆβ„‚ ∧ 𝑋 βŠ† 𝑆)) β†’ 𝐺 ∈ (β„‚ ↑pm 𝑆))
4441, 42, 25, 7, 43syl22anc 1249 . . . . . . . . . . 11 (πœ‘ β†’ 𝐺 ∈ (β„‚ ↑pm 𝑆))
45 reldvg 14375 . . . . . . . . . . 11 ((𝑆 βŠ† β„‚ ∧ 𝐺 ∈ (β„‚ ↑pm 𝑆)) β†’ Rel (𝑆 D 𝐺))
465, 44, 45syl2anc 411 . . . . . . . . . 10 (πœ‘ β†’ Rel (𝑆 D 𝐺))
47 dvadd.bg . . . . . . . . . 10 (πœ‘ β†’ 𝐢(𝑆 D 𝐺)𝐿)
48 releldm 4874 . . . . . . . . . 10 ((Rel (𝑆 D 𝐺) ∧ 𝐢(𝑆 D 𝐺)𝐿) β†’ 𝐢 ∈ dom (𝑆 D 𝐺))
4946, 47, 48syl2anc 411 . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ dom (𝑆 D 𝐺))
50 eqid 2187 . . . . . . . . . 10 (𝐽 β†Ύt 𝑋) = (𝐽 β†Ύt 𝑋)
5150, 3dvcnp2cntop 14390 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐺:π‘‹βŸΆβ„‚ ∧ 𝑋 βŠ† 𝑆) ∧ 𝐢 ∈ dom (𝑆 D 𝐺)) β†’ 𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ))
525, 25, 7, 49, 51syl31anc 1251 . . . . . . . 8 (πœ‘ β†’ 𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ))
533, 50cnplimccntop 14366 . . . . . . . . 9 ((𝑋 βŠ† β„‚ ∧ 𝐢 ∈ 𝑋) β†’ (𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ) ↔ (𝐺:π‘‹βŸΆβ„‚ ∧ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢))))
5411, 23, 53syl2anc 411 . . . . . . . 8 (πœ‘ β†’ (𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ) ↔ (𝐺:π‘‹βŸΆβ„‚ ∧ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢))))
5552, 54mpbid 147 . . . . . . 7 (πœ‘ β†’ (𝐺:π‘‹βŸΆβ„‚ ∧ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢)))
5655simprd 114 . . . . . 6 (πœ‘ β†’ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢))
5725, 11limcdifap 14358 . . . . . . 7 (πœ‘ β†’ (𝐺 limβ„‚ 𝐢) = ((𝐺 β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢))
58 ssrab2 3252 . . . . . . . . . 10 {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} βŠ† 𝑋
5958a1i 9 . . . . . . . . 9 (πœ‘ β†’ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} βŠ† 𝑋)
6025, 59feqresmpt 5583 . . . . . . . 8 (πœ‘ β†’ (𝐺 β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)))
6160oveq1d 5903 . . . . . . 7 (πœ‘ β†’ ((𝐺 β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)) limβ„‚ 𝐢))
6257, 61eqtrd 2220 . . . . . 6 (πœ‘ β†’ (𝐺 limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)) limβ„‚ 𝐢))
6356, 62eleqtrd 2266 . . . . 5 (πœ‘ β†’ (πΊβ€˜πΆ) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)) limβ„‚ 𝐢))
643mulcncntop 14281 . . . . . 6 Β· ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽)
655, 6, 7dvcl 14379 . . . . . . . 8 ((πœ‘ ∧ 𝐢(𝑆 D 𝐹)𝐾) β†’ 𝐾 ∈ β„‚)
661, 65mpdan 421 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ β„‚)
6725, 23ffvelcdmd 5665 . . . . . . 7 (πœ‘ β†’ (πΊβ€˜πΆ) ∈ β„‚)
6866, 67opelxpd 4671 . . . . . 6 (πœ‘ β†’ ⟨𝐾, (πΊβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚))
6937toponunii 13744 . . . . . . 7 (β„‚ Γ— β„‚) = βˆͺ (𝐽 Γ—t 𝐽)
7069cncnpi 13955 . . . . . 6 (( Β· ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (πΊβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚)) β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΎ, (πΊβ€˜πΆ)⟩))
7164, 68, 70sylancr 414 . . . . 5 (πœ‘ β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΎ, (πΊβ€˜πΆ)⟩))
7224, 29, 35, 35, 3, 38, 39, 63, 71limccnp2cntop 14373 . . . 4 (πœ‘ β†’ (𝐾 Β· (πΊβ€˜πΆ)) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§))) limβ„‚ 𝐢))
73 eqid 2187 . . . . . . . 8 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
742, 3, 73, 5, 25, 7eldvap 14378 . . . . . . 7 (πœ‘ β†’ (𝐢(𝑆 D 𝐺)𝐿 ↔ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))))
7547, 74mpbid 147 . . . . . 6 (πœ‘ β†’ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢)))
7675simprd 114 . . . . 5 (πœ‘ β†’ 𝐿 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))
77 cncfmptc 14309 . . . . . . . 8 (((πΉβ€˜πΆ) ∈ β„‚ ∧ 𝑋 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) ∈ (𝑋–cnβ†’β„‚))
7832, 11, 35, 77syl3anc 1248 . . . . . . 7 (πœ‘ β†’ (𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) ∈ (𝑋–cnβ†’β„‚))
79 eqidd 2188 . . . . . . 7 (𝑧 = 𝐢 β†’ (πΉβ€˜πΆ) = (πΉβ€˜πΆ))
8078, 23, 79cnmptlimc 14370 . . . . . 6 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
8132adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ (πΉβ€˜πΆ) ∈ β„‚)
8281fmpttd 5684 . . . . . . . 8 (πœ‘ β†’ (𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)):π‘‹βŸΆβ„‚)
8382, 11limcdifap 14358 . . . . . . 7 (πœ‘ β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢) = (((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢))
84 resmpt 4967 . . . . . . . . 9 ({𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} βŠ† 𝑋 β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)))
8558, 84mp1i 10 . . . . . . . 8 (πœ‘ β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)))
8685oveq1d 5903 . . . . . . 7 (πœ‘ β†’ (((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
8783, 86eqtrd 2220 . . . . . 6 (πœ‘ β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
8880, 87eleqtrd 2266 . . . . 5 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
895, 25, 7dvcl 14379 . . . . . . . 8 ((πœ‘ ∧ 𝐢(𝑆 D 𝐺)𝐿) β†’ 𝐿 ∈ β„‚)
9047, 89mpdan 421 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ β„‚)
9190, 32opelxpd 4671 . . . . . 6 (πœ‘ β†’ ⟨𝐿, (πΉβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚))
9269cncnpi 13955 . . . . . 6 (( Β· ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (πΉβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚)) β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΏ, (πΉβ€˜πΆ)⟩))
9364, 91, 92sylancr 414 . . . . 5 (πœ‘ β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΏ, (πΉβ€˜πΆ)⟩))
9431, 33, 35, 35, 3, 38, 76, 88, 93limccnp2cntop 14373 . . . 4 (πœ‘ β†’ (𝐿 Β· (πΉβ€˜πΆ)) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ))) limβ„‚ 𝐢))
953addcncntop 14279 . . . . 5 + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽)
9666, 67mulcld 7991 . . . . . 6 (πœ‘ β†’ (𝐾 Β· (πΊβ€˜πΆ)) ∈ β„‚)
9790, 32mulcld 7991 . . . . . 6 (πœ‘ β†’ (𝐿 Β· (πΉβ€˜πΆ)) ∈ β„‚)
9896, 97opelxpd 4671 . . . . 5 (πœ‘ β†’ ⟨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩ ∈ (β„‚ Γ— β„‚))
9969cncnpi 13955 . . . . 5 (( + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩ ∈ (β„‚ Γ— β„‚)) β†’ + ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩))
10095, 98, 99sylancr 414 . . . 4 (πœ‘ β†’ + ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩))
10130, 34, 35, 35, 3, 38, 72, 94, 100limccnp2cntop 14373 . . 3 (πœ‘ β†’ ((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))) limβ„‚ 𝐢))
1026adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐹:π‘‹βŸΆβ„‚)
103102, 28ffvelcdmd 5665 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΉβ€˜π‘§) ∈ β„‚)
104103, 33subcld 8281 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) ∈ β„‚)
105104, 29mulcld 7991 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) ∈ β„‚)
10667adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΊβ€˜πΆ) ∈ β„‚)
10729, 106subcld 8281 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) ∈ β„‚)
108107, 33mulcld 7991 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) ∈ β„‚)
10911adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑋 βŠ† β„‚)
110109, 28sseldd 3168 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 ∈ β„‚)
11111, 23sseldd 3168 . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ β„‚)
112111adantr 276 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐢 ∈ β„‚)
113110, 112subcld 8281 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (𝑧 βˆ’ 𝐢) ∈ β„‚)
114 breq1 4018 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ (𝑀 # 𝐢 ↔ 𝑧 # 𝐢))
115114elrab 2905 . . . . . . . . . 10 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↔ (𝑧 ∈ 𝑋 ∧ 𝑧 # 𝐢))
116115simprbi 275 . . . . . . . . 9 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} β†’ 𝑧 # 𝐢)
117116adantl 277 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 # 𝐢)
118110, 112, 117subap0d 8614 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (𝑧 βˆ’ 𝐢) # 0)
119105, 108, 113, 118divdirapd 8799 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) / (𝑧 βˆ’ 𝐢)) = (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) / (𝑧 βˆ’ 𝐢)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))))
120103, 29mulcld 7991 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) ∈ β„‚)
12133, 29mulcld 7991 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) ∈ β„‚)
12233, 106mulcld 7991 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)) ∈ β„‚)
123120, 121, 122npncand 8305 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§))) + (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))) = (((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
124103, 33, 29subdird 8385 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) = (((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§))))
125107, 33mulcomd 7992 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) = ((πΉβ€˜πΆ) Β· ((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ))))
12633, 29, 106subdid 8384 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜πΆ) Β· ((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ))) = (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
127125, 126eqtrd 2220 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) = (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
128124, 127oveq12d 5906 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) = ((((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§))) + (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))))
12928, 28elind 3332 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 ∈ (𝑋 ∩ 𝑋))
1306ffnd 5378 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹 Fn 𝑋)
131130adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐹 Fn 𝑋)
13225ffnd 5378 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺 Fn 𝑋)
133132adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐺 Fn 𝑋)
134 ssexg 4154 . . . . . . . . . . . . 13 ((𝑋 βŠ† β„‚ ∧ β„‚ ∈ V) β†’ 𝑋 ∈ V)
13511, 40, 134sylancl 413 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ V)
136135adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑋 ∈ V)
137 eqid 2187 . . . . . . . . . . 11 (𝑋 ∩ 𝑋) = (𝑋 ∩ 𝑋)
138 eqidd 2188 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ 𝑋) β†’ (πΉβ€˜π‘§) = (πΉβ€˜π‘§))
139 eqidd 2188 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ 𝑋) β†’ (πΊβ€˜π‘§) = (πΊβ€˜π‘§))
140120adantr 276 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ (𝑋 ∩ 𝑋)) β†’ ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) ∈ β„‚)
141131, 133, 136, 136, 137, 138, 139, 140ofvalg 6105 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ (𝑋 ∩ 𝑋)) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) = ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)))
142129, 141mpdan 421 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) = ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)))
14323, 23elind 3332 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ (𝑋 ∩ 𝑋))
144 eqidd 2188 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ 𝑋) β†’ (πΉβ€˜πΆ) = (πΉβ€˜πΆ))
145 eqidd 2188 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ 𝑋) β†’ (πΊβ€˜πΆ) = (πΊβ€˜πΆ))
146122adantr 276 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ (𝑋 ∩ 𝑋)) β†’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)) ∈ β„‚)
147131, 133, 136, 136, 137, 144, 145, 146ofvalg 6105 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ (𝑋 ∩ 𝑋)) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ) = ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))
148143, 147mpidan 423 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ) = ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))
149142, 148oveq12d 5906 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) = (((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
150123, 128, 1493eqtr4d 2230 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) = (((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)))
151150oveq1d 5903 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) / (𝑧 βˆ’ 𝐢)) = ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
152104, 29, 113, 118div23apd 8798 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) / (𝑧 βˆ’ 𝐢)) = ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)))
153107, 33, 113, 118div23apd 8798 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) = ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))
154152, 153oveq12d 5906 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) / (𝑧 βˆ’ 𝐢)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ))))
155119, 151, 1543eqtr3d 2228 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢)) = (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ))))
156155mpteq2dva 4105 . . . 4 (πœ‘ β†’ (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))))
157156oveq1d 5903 . . 3 (πœ‘ β†’ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))) limβ„‚ 𝐢))
158101, 157eleqtrrd 2267 . 2 (πœ‘ β†’ ((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))
159 eqid 2187 . . 3 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
160 mulcl 7951 . . . . 5 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (π‘₯ Β· 𝑦) ∈ β„‚)
161160adantl 277 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚)) β†’ (π‘₯ Β· 𝑦) ∈ β„‚)
162 inidm 3356 . . . 4 (𝑋 ∩ 𝑋) = 𝑋
163161, 6, 25, 135, 135, 162off 6108 . . 3 (πœ‘ β†’ (𝐹 βˆ˜π‘“ Β· 𝐺):π‘‹βŸΆβ„‚)
1642, 3, 159, 5, 163, 7eldvap 14378 . 2 (πœ‘ β†’ (𝐢(𝑆 D (𝐹 βˆ˜π‘“ Β· 𝐺))((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ↔ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ ((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))))
16510, 158, 164mpbir2and 945 1 (πœ‘ β†’ 𝐢(𝑆 D (𝐹 βˆ˜π‘“ Β· 𝐺))((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1363   ∈ wcel 2158  {crab 2469  Vcvv 2749   ∩ cin 3140   βŠ† wss 3141  βŸ¨cop 3607  βˆͺ cuni 3821   class class class wbr 4015   ↦ cmpt 4076   Γ— cxp 4636  dom cdm 4638   β†Ύ cres 4640   ∘ ccom 4642  Rel wrel 4643   Fn wfn 5223  βŸΆwf 5224  β€˜cfv 5228  (class class class)co 5888   βˆ˜π‘“ cof 6094   ↑pm cpm 6662  β„‚cc 7822   + caddc 7827   Β· cmul 7829   βˆ’ cmin 8141   # cap 8551   / cdiv 8642  abscabs 11019   β†Ύt crest 12705  MetOpencmopn 13658  Topctop 13724  TopOnctopon 13737  intcnt 13820   Cn ccn 13912   CnP ccnp 13913   Γ—t ctx 13979  β€“cnβ†’ccncf 14284   limβ„‚ climc 14350   D cdv 14351
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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944  ax-addf 7946  ax-mulf 7947
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-of 6096  df-1st 6154  df-2nd 6155  df-recs 6319  df-frec 6405  df-map 6663  df-pm 6664  df-sup 6996  df-inf 6997  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-xneg 9785  df-xadd 9786  df-seqfrec 10459  df-exp 10533  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-rest 12707  df-topgen 12726  df-psmet 13660  df-xmet 13661  df-met 13662  df-bl 13663  df-mopn 13664  df-top 13725  df-topon 13738  df-bases 13770  df-ntr 13823  df-cn 13915  df-cnp 13916  df-tx 13980  df-cncf 14285  df-limced 14352  df-dvap 14353
This theorem is referenced by:  dvmulxx  14395  dvimulf  14397  dvef  14415
  Copyright terms: Public domain W3C validator