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

Theorem dvmulxxbr 14563
Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 14565. (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 2189 . . . . 5 (𝐽 β†Ύt 𝑆) = (𝐽 β†Ύt 𝑆)
3 dvaddcntop.j . . . . 5 𝐽 = (MetOpenβ€˜(abs ∘ βˆ’ ))
4 eqid 2189 . . . . 5 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
5 dvaddbr.s . . . . 5 (πœ‘ β†’ 𝑆 βŠ† β„‚)
6 dvadd.f . . . . 5 (πœ‘ β†’ 𝐹:π‘‹βŸΆβ„‚)
7 dvadd.x . . . . 5 (πœ‘ β†’ 𝑋 βŠ† 𝑆)
82, 3, 4, 5, 6, 7eldvap 14548 . . . 4 (πœ‘ β†’ (𝐢(𝑆 D 𝐹)𝐾 ↔ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐾 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))))
91, 8mpbid 147 . . 3 (πœ‘ β†’ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐾 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢)))
109simpld 112 . 2 (πœ‘ β†’ 𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹))
117, 5sstrd 3180 . . . . . 6 (πœ‘ β†’ 𝑋 βŠ† β„‚)
123cntoptopon 14429 . . . . . . . . . 10 𝐽 ∈ (TopOnβ€˜β„‚)
13 resttopon 14068 . . . . . . . . . 10 ((𝐽 ∈ (TopOnβ€˜β„‚) ∧ 𝑆 βŠ† β„‚) β†’ (𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
1412, 5, 13sylancr 414 . . . . . . . . 9 (πœ‘ β†’ (𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†))
15 topontop 13911 . . . . . . . . 9 ((𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†) β†’ (𝐽 β†Ύt 𝑆) ∈ Top)
1614, 15syl 14 . . . . . . . 8 (πœ‘ β†’ (𝐽 β†Ύt 𝑆) ∈ Top)
17 toponuni 13912 . . . . . . . . . 10 ((𝐽 β†Ύt 𝑆) ∈ (TopOnβ€˜π‘†) β†’ 𝑆 = βˆͺ (𝐽 β†Ύt 𝑆))
1814, 17syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝑆 = βˆͺ (𝐽 β†Ύt 𝑆))
197, 18sseqtrd 3208 . . . . . . . 8 (πœ‘ β†’ 𝑋 βŠ† βˆͺ (𝐽 β†Ύt 𝑆))
20 eqid 2189 . . . . . . . . 9 βˆͺ (𝐽 β†Ύt 𝑆) = βˆͺ (𝐽 β†Ύt 𝑆)
2120ntrss2 14018 . . . . . . . 8 (((𝐽 β†Ύt 𝑆) ∈ Top ∧ 𝑋 βŠ† βˆͺ (𝐽 β†Ύt 𝑆)) β†’ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) βŠ† 𝑋)
2216, 19, 21syl2anc 411 . . . . . . 7 (πœ‘ β†’ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) βŠ† 𝑋)
2322, 10sseldd 3171 . . . . . 6 (πœ‘ β†’ 𝐢 ∈ 𝑋)
246, 11, 23dvlemap 14546 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) ∈ β„‚)
25 dvaddxx.g . . . . . . 7 (πœ‘ β†’ 𝐺:π‘‹βŸΆβ„‚)
2625adantr 276 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐺:π‘‹βŸΆβ„‚)
27 elrabi 2905 . . . . . . 7 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} β†’ 𝑧 ∈ 𝑋)
2827adantl 277 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 ∈ 𝑋)
2926, 28ffvelcdmd 5668 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΊβ€˜π‘§) ∈ β„‚)
3024, 29mulcld 7996 . . . 4 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) ∈ β„‚)
3125, 11, 23dvlemap 14546 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) ∈ β„‚)
326, 23ffvelcdmd 5668 . . . . . 6 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ β„‚)
3332adantr 276 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΉβ€˜πΆ) ∈ β„‚)
3431, 33mulcld 7996 . . . 4 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)) ∈ β„‚)
35 ssidd 3191 . . . 4 (πœ‘ β†’ β„‚ βŠ† β„‚)
36 txtopon 14159 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜β„‚) ∧ 𝐽 ∈ (TopOnβ€˜β„‚)) β†’ (𝐽 Γ—t 𝐽) ∈ (TopOnβ€˜(β„‚ Γ— β„‚)))
3712, 12, 36mp2an 426 . . . . 5 (𝐽 Γ—t 𝐽) ∈ (TopOnβ€˜(β„‚ Γ— β„‚))
3837toponrestid 13918 . . . 4 (𝐽 Γ—t 𝐽) = ((𝐽 Γ—t 𝐽) β†Ύt (β„‚ Γ— β„‚))
399simprd 114 . . . . 5 (πœ‘ β†’ 𝐾 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))
40 cnex 7953 . . . . . . . . . . . . 13 β„‚ ∈ V
4140a1i 9 . . . . . . . . . . . 12 (πœ‘ β†’ β„‚ ∈ V)
4241, 5ssexd 4158 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 ∈ V)
43 elpm2r 6684 . . . . . . . . . . . 12 (((β„‚ ∈ V ∧ 𝑆 ∈ V) ∧ (𝐺:π‘‹βŸΆβ„‚ ∧ 𝑋 βŠ† 𝑆)) β†’ 𝐺 ∈ (β„‚ ↑pm 𝑆))
4441, 42, 25, 7, 43syl22anc 1250 . . . . . . . . . . 11 (πœ‘ β†’ 𝐺 ∈ (β„‚ ↑pm 𝑆))
45 reldvg 14545 . . . . . . . . . . 11 ((𝑆 βŠ† β„‚ ∧ 𝐺 ∈ (β„‚ ↑pm 𝑆)) β†’ Rel (𝑆 D 𝐺))
465, 44, 45syl2anc 411 . . . . . . . . . 10 (πœ‘ β†’ Rel (𝑆 D 𝐺))
47 dvadd.bg . . . . . . . . . 10 (πœ‘ β†’ 𝐢(𝑆 D 𝐺)𝐿)
48 releldm 4877 . . . . . . . . . 10 ((Rel (𝑆 D 𝐺) ∧ 𝐢(𝑆 D 𝐺)𝐿) β†’ 𝐢 ∈ dom (𝑆 D 𝐺))
4946, 47, 48syl2anc 411 . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ dom (𝑆 D 𝐺))
50 eqid 2189 . . . . . . . . . 10 (𝐽 β†Ύt 𝑋) = (𝐽 β†Ύt 𝑋)
5150, 3dvcnp2cntop 14560 . . . . . . . . 9 (((𝑆 βŠ† β„‚ ∧ 𝐺:π‘‹βŸΆβ„‚ ∧ 𝑋 βŠ† 𝑆) ∧ 𝐢 ∈ dom (𝑆 D 𝐺)) β†’ 𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ))
525, 25, 7, 49, 51syl31anc 1252 . . . . . . . 8 (πœ‘ β†’ 𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ))
533, 50cnplimccntop 14536 . . . . . . . . 9 ((𝑋 βŠ† β„‚ ∧ 𝐢 ∈ 𝑋) β†’ (𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ) ↔ (𝐺:π‘‹βŸΆβ„‚ ∧ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢))))
5411, 23, 53syl2anc 411 . . . . . . . 8 (πœ‘ β†’ (𝐺 ∈ (((𝐽 β†Ύt 𝑋) CnP 𝐽)β€˜πΆ) ↔ (𝐺:π‘‹βŸΆβ„‚ ∧ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢))))
5552, 54mpbid 147 . . . . . . 7 (πœ‘ β†’ (𝐺:π‘‹βŸΆβ„‚ ∧ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢)))
5655simprd 114 . . . . . 6 (πœ‘ β†’ (πΊβ€˜πΆ) ∈ (𝐺 limβ„‚ 𝐢))
5725, 11limcdifap 14528 . . . . . . 7 (πœ‘ β†’ (𝐺 limβ„‚ 𝐢) = ((𝐺 β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢))
58 ssrab2 3255 . . . . . . . . . 10 {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} βŠ† 𝑋
5958a1i 9 . . . . . . . . 9 (πœ‘ β†’ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} βŠ† 𝑋)
6025, 59feqresmpt 5586 . . . . . . . 8 (πœ‘ β†’ (𝐺 β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)))
6160oveq1d 5906 . . . . . . 7 (πœ‘ β†’ ((𝐺 β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)) limβ„‚ 𝐢))
6257, 61eqtrd 2222 . . . . . 6 (πœ‘ β†’ (𝐺 limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)) limβ„‚ 𝐢))
6356, 62eleqtrd 2268 . . . . 5 (πœ‘ β†’ (πΊβ€˜πΆ) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΊβ€˜π‘§)) limβ„‚ 𝐢))
643mulcncntop 14451 . . . . . 6 Β· ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽)
655, 6, 7dvcl 14549 . . . . . . . 8 ((πœ‘ ∧ 𝐢(𝑆 D 𝐹)𝐾) β†’ 𝐾 ∈ β„‚)
661, 65mpdan 421 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ β„‚)
6725, 23ffvelcdmd 5668 . . . . . . 7 (πœ‘ β†’ (πΊβ€˜πΆ) ∈ β„‚)
6866, 67opelxpd 4674 . . . . . 6 (πœ‘ β†’ ⟨𝐾, (πΊβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚))
6937toponunii 13914 . . . . . . 7 (β„‚ Γ— β„‚) = βˆͺ (𝐽 Γ—t 𝐽)
7069cncnpi 14125 . . . . . 6 (( Β· ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (πΊβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚)) β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΎ, (πΊβ€˜πΆ)⟩))
7164, 68, 70sylancr 414 . . . . 5 (πœ‘ β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΎ, (πΊβ€˜πΆ)⟩))
7224, 29, 35, 35, 3, 38, 39, 63, 71limccnp2cntop 14543 . . . 4 (πœ‘ β†’ (𝐾 Β· (πΊβ€˜πΆ)) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§))) limβ„‚ 𝐢))
73 eqid 2189 . . . . . . . 8 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
742, 3, 73, 5, 25, 7eldvap 14548 . . . . . . 7 (πœ‘ β†’ (𝐢(𝑆 D 𝐺)𝐿 ↔ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))))
7547, 74mpbid 147 . . . . . 6 (πœ‘ β†’ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢)))
7675simprd 114 . . . . 5 (πœ‘ β†’ 𝐿 ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))
77 cncfmptc 14479 . . . . . . . 8 (((πΉβ€˜πΆ) ∈ β„‚ ∧ 𝑋 βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) ∈ (𝑋–cnβ†’β„‚))
7832, 11, 35, 77syl3anc 1249 . . . . . . 7 (πœ‘ β†’ (𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) ∈ (𝑋–cnβ†’β„‚))
79 eqidd 2190 . . . . . . 7 (𝑧 = 𝐢 β†’ (πΉβ€˜πΆ) = (πΉβ€˜πΆ))
8078, 23, 79cnmptlimc 14540 . . . . . 6 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
8132adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ (πΉβ€˜πΆ) ∈ β„‚)
8281fmpttd 5687 . . . . . . . 8 (πœ‘ β†’ (𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)):π‘‹βŸΆβ„‚)
8382, 11limcdifap 14528 . . . . . . 7 (πœ‘ β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢) = (((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢))
84 resmpt 4970 . . . . . . . . 9 ({𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} βŠ† 𝑋 β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)))
8558, 84mp1i 10 . . . . . . . 8 (πœ‘ β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)))
8685oveq1d 5906 . . . . . . 7 (πœ‘ β†’ (((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) β†Ύ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
8783, 86eqtrd 2222 . . . . . 6 (πœ‘ β†’ ((𝑧 ∈ 𝑋 ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
8880, 87eleqtrd 2268 . . . . 5 (πœ‘ β†’ (πΉβ€˜πΆ) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (πΉβ€˜πΆ)) limβ„‚ 𝐢))
895, 25, 7dvcl 14549 . . . . . . . 8 ((πœ‘ ∧ 𝐢(𝑆 D 𝐺)𝐿) β†’ 𝐿 ∈ β„‚)
9047, 89mpdan 421 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ β„‚)
9190, 32opelxpd 4674 . . . . . 6 (πœ‘ β†’ ⟨𝐿, (πΉβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚))
9269cncnpi 14125 . . . . . 6 (( Β· ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (πΉβ€˜πΆ)⟩ ∈ (β„‚ Γ— β„‚)) β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΏ, (πΉβ€˜πΆ)⟩))
9364, 91, 92sylancr 414 . . . . 5 (πœ‘ β†’ Β· ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨πΏ, (πΉβ€˜πΆ)⟩))
9431, 33, 35, 35, 3, 38, 76, 88, 93limccnp2cntop 14543 . . . 4 (πœ‘ β†’ (𝐿 Β· (πΉβ€˜πΆ)) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ))) limβ„‚ 𝐢))
953addcncntop 14449 . . . . 5 + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽)
9666, 67mulcld 7996 . . . . . 6 (πœ‘ β†’ (𝐾 Β· (πΊβ€˜πΆ)) ∈ β„‚)
9790, 32mulcld 7996 . . . . . 6 (πœ‘ β†’ (𝐿 Β· (πΉβ€˜πΆ)) ∈ β„‚)
9896, 97opelxpd 4674 . . . . 5 (πœ‘ β†’ ⟨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩ ∈ (β„‚ Γ— β„‚))
9969cncnpi 14125 . . . . 5 (( + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩ ∈ (β„‚ Γ— β„‚)) β†’ + ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩))
10095, 98, 99sylancr 414 . . . 4 (πœ‘ β†’ + ∈ (((𝐽 Γ—t 𝐽) CnP 𝐽)β€˜βŸ¨(𝐾 Β· (πΊβ€˜πΆ)), (𝐿 Β· (πΉβ€˜πΆ))⟩))
10130, 34, 35, 35, 3, 38, 72, 94, 100limccnp2cntop 14543 . . 3 (πœ‘ β†’ ((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))) limβ„‚ 𝐢))
1026adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐹:π‘‹βŸΆβ„‚)
103102, 28ffvelcdmd 5668 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΉβ€˜π‘§) ∈ β„‚)
104103, 33subcld 8286 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) ∈ β„‚)
105104, 29mulcld 7996 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) ∈ β„‚)
10667adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (πΊβ€˜πΆ) ∈ β„‚)
10729, 106subcld 8286 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) ∈ β„‚)
108107, 33mulcld 7996 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) ∈ β„‚)
10911adantr 276 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑋 βŠ† β„‚)
110109, 28sseldd 3171 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 ∈ β„‚)
11111, 23sseldd 3171 . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ β„‚)
112111adantr 276 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐢 ∈ β„‚)
113110, 112subcld 8286 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (𝑧 βˆ’ 𝐢) ∈ β„‚)
114 breq1 4021 . . . . . . . . . . 11 (𝑀 = 𝑧 β†’ (𝑀 # 𝐢 ↔ 𝑧 # 𝐢))
115114elrab 2908 . . . . . . . . . 10 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↔ (𝑧 ∈ 𝑋 ∧ 𝑧 # 𝐢))
116115simprbi 275 . . . . . . . . 9 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} β†’ 𝑧 # 𝐢)
117116adantl 277 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 # 𝐢)
118110, 112, 117subap0d 8619 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (𝑧 βˆ’ 𝐢) # 0)
119105, 108, 113, 118divdirapd 8804 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) / (𝑧 βˆ’ 𝐢)) = (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) / (𝑧 βˆ’ 𝐢)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))))
120103, 29mulcld 7996 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) ∈ β„‚)
12133, 29mulcld 7996 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) ∈ β„‚)
12233, 106mulcld 7996 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)) ∈ β„‚)
123120, 121, 122npncand 8310 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§))) + (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))) = (((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
124103, 33, 29subdird 8390 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) = (((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§))))
125107, 33mulcomd 7997 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) = ((πΉβ€˜πΆ) Β· ((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ))))
12633, 29, 106subdid 8389 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((πΉβ€˜πΆ) Β· ((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ))) = (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
127125, 126eqtrd 2222 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) = (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
128124, 127oveq12d 5909 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) = ((((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§))) + (((πΉβ€˜πΆ) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))))
12928, 28elind 3335 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑧 ∈ (𝑋 ∩ 𝑋))
1306ffnd 5381 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹 Fn 𝑋)
131130adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐹 Fn 𝑋)
13225ffnd 5381 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺 Fn 𝑋)
133132adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝐺 Fn 𝑋)
134 ssexg 4157 . . . . . . . . . . . . 13 ((𝑋 βŠ† β„‚ ∧ β„‚ ∈ V) β†’ 𝑋 ∈ V)
13511, 40, 134sylancl 413 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ V)
136135adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ 𝑋 ∈ V)
137 eqid 2189 . . . . . . . . . . 11 (𝑋 ∩ 𝑋) = (𝑋 ∩ 𝑋)
138 eqidd 2190 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ 𝑋) β†’ (πΉβ€˜π‘§) = (πΉβ€˜π‘§))
139 eqidd 2190 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ 𝑋) β†’ (πΊβ€˜π‘§) = (πΊβ€˜π‘§))
140120adantr 276 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ (𝑋 ∩ 𝑋)) β†’ ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) ∈ β„‚)
141131, 133, 136, 136, 137, 138, 139, 140ofvalg 6110 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝑧 ∈ (𝑋 ∩ 𝑋)) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) = ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)))
142129, 141mpdan 421 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) = ((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)))
14323, 23elind 3335 . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ (𝑋 ∩ 𝑋))
144 eqidd 2190 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ 𝑋) β†’ (πΉβ€˜πΆ) = (πΉβ€˜πΆ))
145 eqidd 2190 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ 𝑋) β†’ (πΊβ€˜πΆ) = (πΊβ€˜πΆ))
146122adantr 276 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ (𝑋 ∩ 𝑋)) β†’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)) ∈ β„‚)
147131, 133, 136, 136, 137, 144, 145, 146ofvalg 6110 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) ∧ 𝐢 ∈ (𝑋 ∩ 𝑋)) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ) = ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))
148143, 147mpidan 423 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ) = ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ)))
149142, 148oveq12d 5909 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) = (((πΉβ€˜π‘§) Β· (πΊβ€˜π‘§)) βˆ’ ((πΉβ€˜πΆ) Β· (πΊβ€˜πΆ))))
150123, 128, 1493eqtr4d 2232 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) = (((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)))
151150oveq1d 5906 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) + (((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ))) / (𝑧 βˆ’ 𝐢)) = ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
152104, 29, 113, 118div23apd 8803 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) / (𝑧 βˆ’ 𝐢)) = ((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)))
153107, 33, 113, 118div23apd 8803 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) = ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))
154152, 153oveq12d 5909 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) Β· (πΊβ€˜π‘§)) / (𝑧 βˆ’ 𝐢)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) Β· (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ))))
155119, 151, 1543eqtr3d 2230 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢}) β†’ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢)) = (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ))))
156155mpteq2dva 4108 . . . 4 (πœ‘ β†’ (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))))
157156oveq1d 5906 . . 3 (πœ‘ β†’ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢) = ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ (((((πΉβ€˜π‘§) βˆ’ (πΉβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΊβ€˜π‘§)) + ((((πΊβ€˜π‘§) βˆ’ (πΊβ€˜πΆ)) / (𝑧 βˆ’ 𝐢)) Β· (πΉβ€˜πΆ)))) limβ„‚ 𝐢))
158101, 157eleqtrrd 2269 . 2 (πœ‘ β†’ ((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))
159 eqid 2189 . . 3 (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) = (𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢)))
160 mulcl 7956 . . . . 5 ((π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (π‘₯ Β· 𝑦) ∈ β„‚)
161160adantl 277 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ β„‚ ∧ 𝑦 ∈ β„‚)) β†’ (π‘₯ Β· 𝑦) ∈ β„‚)
162 inidm 3359 . . . 4 (𝑋 ∩ 𝑋) = 𝑋
163161, 6, 25, 135, 135, 162off 6113 . . 3 (πœ‘ β†’ (𝐹 βˆ˜π‘“ Β· 𝐺):π‘‹βŸΆβ„‚)
1642, 3, 159, 5, 163, 7eldvap 14548 . 2 (πœ‘ β†’ (𝐢(𝑆 D (𝐹 βˆ˜π‘“ Β· 𝐺))((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ↔ (𝐢 ∈ ((intβ€˜(𝐽 β†Ύt 𝑆))β€˜π‘‹) ∧ ((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))) ∈ ((𝑧 ∈ {𝑀 ∈ 𝑋 ∣ 𝑀 # 𝐢} ↦ ((((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜π‘§) βˆ’ ((𝐹 βˆ˜π‘“ Β· 𝐺)β€˜πΆ)) / (𝑧 βˆ’ 𝐢))) limβ„‚ 𝐢))))
16510, 158, 164mpbir2and 946 1 (πœ‘ β†’ 𝐢(𝑆 D (𝐹 βˆ˜π‘“ Β· 𝐺))((𝐾 Β· (πΊβ€˜πΆ)) + (𝐿 Β· (πΉβ€˜πΆ))))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2160  {crab 2472  Vcvv 2752   ∩ cin 3143   βŠ† wss 3144  βŸ¨cop 3610  βˆͺ cuni 3824   class class class wbr 4018   ↦ cmpt 4079   Γ— cxp 4639  dom cdm 4641   β†Ύ cres 4643   ∘ ccom 4645  Rel wrel 4646   Fn wfn 5226  βŸΆwf 5227  β€˜cfv 5231  (class class class)co 5891   βˆ˜π‘“ cof 6099   ↑pm cpm 6667  β„‚cc 7827   + caddc 7832   Β· cmul 7834   βˆ’ cmin 8146   # cap 8556   / cdiv 8647  abscabs 11024   β†Ύt crest 12710  MetOpencmopn 13815  Topctop 13894  TopOnctopon 13907  intcnt 13990   Cn ccn 14082   CnP ccnp 14083   Γ—t ctx 14149  β€“cnβ†’ccncf 14454   limβ„‚ climc 14520   D cdv 14521
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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602  ax-cnex 7920  ax-resscn 7921  ax-1cn 7922  ax-1re 7923  ax-icn 7924  ax-addcl 7925  ax-addrcl 7926  ax-mulcl 7927  ax-mulrcl 7928  ax-addcom 7929  ax-mulcom 7930  ax-addass 7931  ax-mulass 7932  ax-distr 7933  ax-i2m1 7934  ax-0lt1 7935  ax-1rid 7936  ax-0id 7937  ax-rnegex 7938  ax-precex 7939  ax-cnre 7940  ax-pre-ltirr 7941  ax-pre-ltwlin 7942  ax-pre-lttrn 7943  ax-pre-apti 7944  ax-pre-ltadd 7945  ax-pre-mulgt0 7946  ax-pre-mulext 7947  ax-arch 7948  ax-caucvg 7949  ax-addf 7951  ax-mulf 7952
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-ilim 4384  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-isom 5240  df-riota 5847  df-ov 5894  df-oprab 5895  df-mpo 5896  df-of 6101  df-1st 6159  df-2nd 6160  df-recs 6324  df-frec 6410  df-map 6668  df-pm 6669  df-sup 7001  df-inf 7002  df-pnf 8012  df-mnf 8013  df-xr 8014  df-ltxr 8015  df-le 8016  df-sub 8148  df-neg 8149  df-reap 8550  df-ap 8557  df-div 8648  df-inn 8938  df-2 8996  df-3 8997  df-4 8998  df-n0 9195  df-z 9272  df-uz 9547  df-q 9638  df-rp 9672  df-xneg 9790  df-xadd 9791  df-seqfrec 10464  df-exp 10538  df-cj 10869  df-re 10870  df-im 10871  df-rsqrt 11025  df-abs 11026  df-rest 12712  df-topgen 12731  df-psmet 13817  df-xmet 13818  df-met 13819  df-bl 13820  df-mopn 13821  df-top 13895  df-topon 13908  df-bases 13940  df-ntr 13993  df-cn 14085  df-cnp 14086  df-tx 14150  df-cncf 14455  df-limced 14522  df-dvap 14523
This theorem is referenced by:  dvmulxx  14565  dvimulf  14567  dvef  14585
  Copyright terms: Public domain W3C validator