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

Theorem dvmulbr 25791
Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25794. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11186 and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025.)
Hypotheses
Ref Expression
dvadd.f (𝜑𝐹:𝑋⟶ℂ)
dvadd.x (𝜑𝑋𝑆)
dvadd.g (𝜑𝐺:𝑌⟶ℂ)
dvadd.y (𝜑𝑌𝑆)
dvaddbr.s (𝜑𝑆 ⊆ ℂ)
dvadd.bf (𝜑𝐶(𝑆 D 𝐹)𝐾)
dvadd.bg (𝜑𝐶(𝑆 D 𝐺)𝐿)
dvadd.j 𝐽 = (TopOpen‘ℂfld)
Assertion
Ref Expression
dvmulbr (𝜑𝐶(𝑆 D (𝐹f · 𝐺))((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))))

Proof of Theorem dvmulbr
Dummy variables 𝑦 𝑧 𝑥 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvadd.bf . . . . . 6 (𝜑𝐶(𝑆 D 𝐹)𝐾)
2 eqid 2724 . . . . . . 7 (𝐽t 𝑆) = (𝐽t 𝑆)
3 dvadd.j . . . . . . 7 𝐽 = (TopOpen‘ℂfld)
4 eqid 2724 . . . . . . 7 (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)))
5 dvaddbr.s . . . . . . 7 (𝜑𝑆 ⊆ ℂ)
6 dvadd.f . . . . . . 7 (𝜑𝐹:𝑋⟶ℂ)
7 dvadd.x . . . . . . 7 (𝜑𝑋𝑆)
82, 3, 4, 5, 6, 7eldv 25749 . . . . . 6 (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))))
91, 8mpbid 231 . . . . 5 (𝜑 → (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶)))
109simpld 494 . . . 4 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋))
11 dvadd.bg . . . . . 6 (𝜑𝐶(𝑆 D 𝐺)𝐿)
12 eqid 2724 . . . . . . 7 (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)))
13 dvadd.g . . . . . . 7 (𝜑𝐺:𝑌⟶ℂ)
14 dvadd.y . . . . . . 7 (𝜑𝑌𝑆)
152, 3, 12, 5, 13, 14eldv 25749 . . . . . 6 (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))))
1611, 15mpbid 231 . . . . 5 (𝜑 → (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶)))
1716simpld 494 . . . 4 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌))
1810, 17elind 4186 . . 3 (𝜑𝐶 ∈ (((int‘(𝐽t 𝑆))‘𝑋) ∩ ((int‘(𝐽t 𝑆))‘𝑌)))
193cnfldtopon 24621 . . . . . 6 𝐽 ∈ (TopOn‘ℂ)
20 resttopon 22987 . . . . . 6 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽t 𝑆) ∈ (TopOn‘𝑆))
2119, 5, 20sylancr 586 . . . . 5 (𝜑 → (𝐽t 𝑆) ∈ (TopOn‘𝑆))
22 topontop 22737 . . . . 5 ((𝐽t 𝑆) ∈ (TopOn‘𝑆) → (𝐽t 𝑆) ∈ Top)
2321, 22syl 17 . . . 4 (𝜑 → (𝐽t 𝑆) ∈ Top)
24 toponuni 22738 . . . . . 6 ((𝐽t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = (𝐽t 𝑆))
2521, 24syl 17 . . . . 5 (𝜑𝑆 = (𝐽t 𝑆))
267, 25sseqtrd 4014 . . . 4 (𝜑𝑋 (𝐽t 𝑆))
2714, 25sseqtrd 4014 . . . 4 (𝜑𝑌 (𝐽t 𝑆))
28 eqid 2724 . . . . 5 (𝐽t 𝑆) = (𝐽t 𝑆)
2928ntrin 22887 . . . 4 (((𝐽t 𝑆) ∈ Top ∧ 𝑋 (𝐽t 𝑆) ∧ 𝑌 (𝐽t 𝑆)) → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘𝑋) ∩ ((int‘(𝐽t 𝑆))‘𝑌)))
3023, 26, 27, 29syl3anc 1368 . . 3 (𝜑 → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘𝑋) ∩ ((int‘(𝐽t 𝑆))‘𝑌)))
3118, 30eleqtrrd 2828 . 2 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘(𝑋𝑌)))
326adantr 480 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33 inss1 4220 . . . . . . . . 9 (𝑋𝑌) ⊆ 𝑋
34 eldifi 4118 . . . . . . . . . 10 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋𝑌))
3534adantl 481 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋𝑌))
3633, 35sselid 3972 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧𝑋)
3732, 36ffvelcdmd 7077 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐹𝑧) ∈ ℂ)
385, 6, 7dvbss 25752 . . . . . . . . . 10 (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39 reldv 25721 . . . . . . . . . . 11 Rel (𝑆 D 𝐹)
40 releldm 5933 . . . . . . . . . . 11 ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
4139, 1, 40sylancr 586 . . . . . . . . . 10 (𝜑𝐶 ∈ dom (𝑆 D 𝐹))
4238, 41sseldd 3975 . . . . . . . . 9 (𝜑𝐶𝑋)
436, 42ffvelcdmd 7077 . . . . . . . 8 (𝜑 → (𝐹𝐶) ∈ ℂ)
4443adantr 480 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐹𝐶) ∈ ℂ)
4537, 44subcld 11568 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝑧) − (𝐹𝐶)) ∈ ℂ)
467, 5sstrd 3984 . . . . . . . . 9 (𝜑𝑋 ⊆ ℂ)
4746adantr 480 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
4847, 36sseldd 3975 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
4946, 42sseldd 3975 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
5049adantr 480 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
5148, 50subcld 11568 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑧𝐶) ∈ ℂ)
52 eldifsni 4785 . . . . . . . 8 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) → 𝑧𝐶)
5352adantl 481 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧𝐶)
5448, 50, 53subne0d 11577 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑧𝐶) ≠ 0)
5545, 51, 54divcld 11987 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) ∈ ℂ)
5613adantr 480 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57 inss2 4221 . . . . . . 7 (𝑋𝑌) ⊆ 𝑌
5857, 35sselid 3972 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧𝑌)
5956, 58ffvelcdmd 7077 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐺𝑧) ∈ ℂ)
6055, 59mulcld 11231 . . . 4 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) ∈ ℂ)
61 ssdif 4131 . . . . . . . 8 ((𝑋𝑌) ⊆ 𝑌 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
6257, 61mp1i 13 . . . . . . 7 (𝜑 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
6362sselda 3974 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
6414, 5sstrd 3984 . . . . . . 7 (𝜑𝑌 ⊆ ℂ)
655, 13, 14dvbss 25752 . . . . . . . 8 (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66 reldv 25721 . . . . . . . . 9 Rel (𝑆 D 𝐺)
67 releldm 5933 . . . . . . . . 9 ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
6866, 11, 67sylancr 586 . . . . . . . 8 (𝜑𝐶 ∈ dom (𝑆 D 𝐺))
6965, 68sseldd 3975 . . . . . . 7 (𝜑𝐶𝑌)
7013, 64, 69dvlem 25747 . . . . . 6 ((𝜑𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) ∈ ℂ)
7163, 70syldan 590 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) ∈ ℂ)
7271, 44mulcld 11231 . . . 4 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)) ∈ ℂ)
73 ssidd 3997 . . . 4 (𝜑 → ℂ ⊆ ℂ)
74 txtopon 23417 . . . . . 6 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
7519, 19, 74mp2an 689 . . . . 5 (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
7675toponrestid 22745 . . . 4 (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ × ℂ))
779simprd 495 . . . . . . . 8 (𝜑𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
786, 46, 42dvlem 25747 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) ∈ ℂ)
7978fmpttd 7106 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80 ssdif 4131 . . . . . . . . . . 11 ((𝑋𝑌) ⊆ 𝑋 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
8133, 80mp1i 13 . . . . . . . . . 10 (𝜑 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
8246ssdifssd 4134 . . . . . . . . . 10 (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83 eqid 2724 . . . . . . . . . 10 (𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
8433, 7sstrid 3985 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋𝑌) ⊆ 𝑆)
8584, 25sseqtrd 4014 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋𝑌) ⊆ (𝐽t 𝑆))
86 difssd 4124 . . . . . . . . . . . . . . . 16 (𝜑 → ( (𝐽t 𝑆) ∖ 𝑋) ⊆ (𝐽t 𝑆))
8785, 86unssd 4178 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋)) ⊆ (𝐽t 𝑆))
88 ssun1 4164 . . . . . . . . . . . . . . . 16 (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))
8988a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋)))
9028ntrss 22881 . . . . . . . . . . . . . . 15 (((𝐽t 𝑆) ∈ Top ∧ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋)) ⊆ (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))))
9123, 87, 89, 90syl3anc 1368 . . . . . . . . . . . . . 14 (𝜑 → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))))
92 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))
932, 3, 92, 5, 6, 7eldv 25749 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) lim 𝐶))))
941, 93mpbid 231 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) lim 𝐶)))
9594simpld 494 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋))
96 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑥) − (𝐺𝐶)) / (𝑥𝐶))) = (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑥) − (𝐺𝐶)) / (𝑥𝐶)))
972, 3, 96, 5, 13, 14eldv 25749 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑥) − (𝐺𝐶)) / (𝑥𝐶))) lim 𝐶))))
9811, 97mpbid 231 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑥) − (𝐺𝐶)) / (𝑥𝐶))) lim 𝐶)))
9998simpld 494 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌))
10095, 99elind 4186 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ (((int‘(𝐽t 𝑆))‘𝑋) ∩ ((int‘(𝐽t 𝑆))‘𝑌)))
101100, 30eleqtrrd 2828 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘(𝑋𝑌)))
10291, 101sseldd 3975 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))))
103102, 42elind 4186 . . . . . . . . . . . 12 (𝜑𝐶 ∈ (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋))
10433a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝑋𝑌) ⊆ 𝑋)
105 eqid 2724 . . . . . . . . . . . . . . 15 ((𝐽t 𝑆) ↾t 𝑋) = ((𝐽t 𝑆) ↾t 𝑋)
10628, 105restntr 23008 . . . . . . . . . . . . . 14 (((𝐽t 𝑆) ∈ Top ∧ 𝑋 (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ 𝑋) → ((int‘((𝐽t 𝑆) ↾t 𝑋))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋))
10723, 26, 104, 106syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑋))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋))
1083cnfldtop 24622 . . . . . . . . . . . . . . . . 17 𝐽 ∈ Top
109108a1i 11 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ Top)
110 cnex 11187 . . . . . . . . . . . . . . . . 17 ℂ ∈ V
111 ssexg 5313 . . . . . . . . . . . . . . . . 17 ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
1125, 110, 111sylancl 585 . . . . . . . . . . . . . . . 16 (𝜑𝑆 ∈ V)
113 restabs 22991 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑋𝑆𝑆 ∈ V) → ((𝐽t 𝑆) ↾t 𝑋) = (𝐽t 𝑋))
114109, 7, 112, 113syl3anc 1368 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐽t 𝑆) ↾t 𝑋) = (𝐽t 𝑋))
115114fveq2d 6885 . . . . . . . . . . . . . 14 (𝜑 → (int‘((𝐽t 𝑆) ↾t 𝑋)) = (int‘(𝐽t 𝑋)))
116115fveq1d 6883 . . . . . . . . . . . . 13 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑋))‘(𝑋𝑌)) = ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
117107, 116eqtr3d 2766 . . . . . . . . . . . 12 (𝜑 → (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
118103, 117eleqtrd 2827 . . . . . . . . . . 11 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
119 undif1 4467 . . . . . . . . . . . . . . 15 ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
12042snssd 4804 . . . . . . . . . . . . . . . 16 (𝜑 → {𝐶} ⊆ 𝑋)
121 ssequn2 4175 . . . . . . . . . . . . . . . 16 ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
122120, 121sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
123119, 122eqtrid 2776 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
124123oveq2d 7417 . . . . . . . . . . . . 13 (𝜑 → (𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t 𝑋))
125124fveq2d 6885 . . . . . . . . . . . 12 (𝜑 → (int‘(𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽t 𝑋)))
126 undif1 4467 . . . . . . . . . . . . 13 (((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋𝑌) ∪ {𝐶})
12742, 69elind 4186 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ (𝑋𝑌))
128127snssd 4804 . . . . . . . . . . . . . 14 (𝜑 → {𝐶} ⊆ (𝑋𝑌))
129 ssequn2 4175 . . . . . . . . . . . . . 14 ({𝐶} ⊆ (𝑋𝑌) ↔ ((𝑋𝑌) ∪ {𝐶}) = (𝑋𝑌))
130128, 129sylib 217 . . . . . . . . . . . . 13 (𝜑 → ((𝑋𝑌) ∪ {𝐶}) = (𝑋𝑌))
131126, 130eqtrid 2776 . . . . . . . . . . . 12 (𝜑 → (((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋𝑌))
132125, 131fveq12d 6888 . . . . . . . . . . 11 (𝜑 → ((int‘(𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
133118, 132eleqtrrd 2828 . . . . . . . . . 10 (𝜑𝐶 ∈ ((int‘(𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})))
13479, 81, 82, 3, 83, 133limcres 25737 . . . . . . . . 9 (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
13581resmptd 6030 . . . . . . . . . 10 (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))))
136135oveq1d 7416 . . . . . . . . 9 (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
137134, 136eqtr3d 2766 . . . . . . . 8 (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
13877, 137eleqtrd 2827 . . . . . . 7 (𝜑𝐾 ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
139 eqid 2724 . . . . . . . . . . . 12 (𝐽t 𝑌) = (𝐽t 𝑌)
140139, 3dvcnp2 25771 . . . . . . . . . . 11 (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶))
1415, 13, 14, 68, 140syl31anc 1370 . . . . . . . . . 10 (𝜑𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶))
1423, 139cnplimc 25738 . . . . . . . . . . 11 ((𝑌 ⊆ ℂ ∧ 𝐶𝑌) → (𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶))))
14364, 69, 142syl2anc 583 . . . . . . . . . 10 (𝜑 → (𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶))))
144141, 143mpbid 231 . . . . . . . . 9 (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶)))
145144simprd 495 . . . . . . . 8 (𝜑 → (𝐺𝐶) ∈ (𝐺 lim 𝐶))
146 difss 4123 . . . . . . . . . . . 12 ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋𝑌)
147146, 57sstri 3983 . . . . . . . . . . 11 ((𝑋𝑌) ∖ {𝐶}) ⊆ 𝑌
148147a1i 11 . . . . . . . . . 10 (𝜑 → ((𝑋𝑌) ∖ {𝐶}) ⊆ 𝑌)
149 eqid 2724 . . . . . . . . . 10 (𝐽t (𝑌 ∪ {𝐶})) = (𝐽t (𝑌 ∪ {𝐶}))
150 difssd 4124 . . . . . . . . . . . . . . . 16 (𝜑 → ( (𝐽t 𝑆) ∖ 𝑌) ⊆ (𝐽t 𝑆))
15185, 150unssd 4178 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌)) ⊆ (𝐽t 𝑆))
152 ssun1 4164 . . . . . . . . . . . . . . . 16 (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))
153152a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌)))
15428ntrss 22881 . . . . . . . . . . . . . . 15 (((𝐽t 𝑆) ∈ Top ∧ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌)) ⊆ (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))))
15523, 151, 153, 154syl3anc 1368 . . . . . . . . . . . . . 14 (𝜑 → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))))
156155, 101sseldd 3975 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))))
157156, 69elind 4186 . . . . . . . . . . . 12 (𝜑𝐶 ∈ (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌))
15857a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝑋𝑌) ⊆ 𝑌)
159 eqid 2724 . . . . . . . . . . . . . . 15 ((𝐽t 𝑆) ↾t 𝑌) = ((𝐽t 𝑆) ↾t 𝑌)
16028, 159restntr 23008 . . . . . . . . . . . . . 14 (((𝐽t 𝑆) ∈ Top ∧ 𝑌 (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ 𝑌) → ((int‘((𝐽t 𝑆) ↾t 𝑌))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌))
16123, 27, 158, 160syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑌))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌))
162 restabs 22991 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑌𝑆𝑆 ∈ V) → ((𝐽t 𝑆) ↾t 𝑌) = (𝐽t 𝑌))
163109, 14, 112, 162syl3anc 1368 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐽t 𝑆) ↾t 𝑌) = (𝐽t 𝑌))
164163fveq2d 6885 . . . . . . . . . . . . . 14 (𝜑 → (int‘((𝐽t 𝑆) ↾t 𝑌)) = (int‘(𝐽t 𝑌)))
165164fveq1d 6883 . . . . . . . . . . . . 13 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑌))‘(𝑋𝑌)) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
166161, 165eqtr3d 2766 . . . . . . . . . . . 12 (𝜑 → (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
167157, 166eleqtrd 2827 . . . . . . . . . . 11 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
16869snssd 4804 . . . . . . . . . . . . . . 15 (𝜑 → {𝐶} ⊆ 𝑌)
169 ssequn2 4175 . . . . . . . . . . . . . . 15 ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
170168, 169sylib 217 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
171170oveq2d 7417 . . . . . . . . . . . . 13 (𝜑 → (𝐽t (𝑌 ∪ {𝐶})) = (𝐽t 𝑌))
172171fveq2d 6885 . . . . . . . . . . . 12 (𝜑 → (int‘(𝐽t (𝑌 ∪ {𝐶}))) = (int‘(𝐽t 𝑌)))
173172, 131fveq12d 6888 . . . . . . . . . . 11 (𝜑 → ((int‘(𝐽t (𝑌 ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
174167, 173eleqtrrd 2828 . . . . . . . . . 10 (𝜑𝐶 ∈ ((int‘(𝐽t (𝑌 ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})))
17513, 148, 64, 3, 149, 174limcres 25737 . . . . . . . . 9 (𝜑 → ((𝐺 ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = (𝐺 lim 𝐶))
17613, 148feqresmpt 6951 . . . . . . . . . 10 (𝜑 → (𝐺 ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)))
177176oveq1d 7416 . . . . . . . . 9 (𝜑 → ((𝐺 ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)) lim 𝐶))
178175, 177eqtr3d 2766 . . . . . . . 8 (𝜑 → (𝐺 lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)) lim 𝐶))
179145, 178eleqtrd 2827 . . . . . . 7 (𝜑 → (𝐺𝐶) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)) lim 𝐶))
1803mpomulcn 24707 . . . . . . . 8 (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
1815, 6, 7dvcl 25750 . . . . . . . . . 10 ((𝜑𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
1821, 181mpdan 684 . . . . . . . . 9 (𝜑𝐾 ∈ ℂ)
18313, 69ffvelcdmd 7077 . . . . . . . . 9 (𝜑 → (𝐺𝐶) ∈ ℂ)
184182, 183opelxpd 5705 . . . . . . . 8 (𝜑 → ⟨𝐾, (𝐺𝐶)⟩ ∈ (ℂ × ℂ))
18575toponunii 22740 . . . . . . . . 9 (ℂ × ℂ) = (𝐽 ×t 𝐽)
186185cncnpi 23104 . . . . . . . 8 (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (𝐺𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺𝐶)⟩))
187180, 184, 186sylancr 586 . . . . . . 7 (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺𝐶)⟩))
18855, 59, 73, 73, 3, 76, 138, 179, 187limccnp2 25743 . . . . . 6 (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝐶)) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧))) lim 𝐶))
189 df-mpt 5222 . . . . . . 7 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)))}
190189oveq1i 7411 . . . . . 6 ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧))) lim 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)))} lim 𝐶)
191188, 190eleqtrdi 2835 . . . . 5 (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)))} lim 𝐶))
192 ovmpot 7561 . . . . . 6 ((𝐾 ∈ ℂ ∧ (𝐺𝐶) ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝐶)) = (𝐾 · (𝐺𝐶)))
193182, 183, 192syl2anc 583 . . . . 5 (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝐶)) = (𝐾 · (𝐺𝐶)))
194 ovmpot 7561 . . . . . . . . . . 11 (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) ∈ ℂ ∧ (𝐺𝑧) ∈ ℂ) → ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)) = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)))
19555, 59, 194syl2anc 583 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)) = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)))
196195eqeq2d 2735 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)) ↔ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧))))
197196pm5.32da 578 . . . . . . . 8 (𝜑 → ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧))) ↔ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)))))
198197opabbidv 5204 . . . . . . 7 (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)))})
199 df-mpt 5222 . . . . . . 7 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)))}
200198, 199eqtr4di 2782 . . . . . 6 (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)))} = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧))))
201200oveq1d 7416 . . . . 5 (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺𝑧)))} lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧))) lim 𝐶))
202191, 193, 2013eltr3d 2839 . . . 4 (𝜑 → (𝐾 · (𝐺𝐶)) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧))) lim 𝐶))
20316simprd 495 . . . . . . . 8 (𝜑𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
20470fmpttd 7106 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
20564ssdifssd 4134 . . . . . . . . . 10 (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
206 eqid 2724 . . . . . . . . . 10 (𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
207 undif1 4467 . . . . . . . . . . . . . . 15 ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
208207, 170eqtrid 2776 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
209208oveq2d 7417 . . . . . . . . . . . . 13 (𝜑 → (𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t 𝑌))
210209fveq2d 6885 . . . . . . . . . . . 12 (𝜑 → (int‘(𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽t 𝑌)))
211210, 131fveq12d 6888 . . . . . . . . . . 11 (𝜑 → ((int‘(𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
212167, 211eleqtrrd 2828 . . . . . . . . . 10 (𝜑𝐶 ∈ ((int‘(𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})))
213204, 62, 205, 3, 206, 212limcres 25737 . . . . . . . . 9 (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
21462resmptd 6030 . . . . . . . . . 10 (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))))
215214oveq1d 7416 . . . . . . . . 9 (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
216213, 215eqtr3d 2766 . . . . . . . 8 (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
217203, 216eleqtrd 2827 . . . . . . 7 (𝜑𝐿 ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
21884, 5sstrd 3984 . . . . . . . . . 10 (𝜑 → (𝑋𝑌) ⊆ ℂ)
219 cncfmptc 24754 . . . . . . . . . 10 (((𝐹𝐶) ∈ ℂ ∧ (𝑋𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ∈ ((𝑋𝑌)–cn→ℂ))
22043, 218, 73, 219syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ∈ ((𝑋𝑌)–cn→ℂ))
221 eqidd 2725 . . . . . . . . 9 (𝑧 = 𝐶 → (𝐹𝐶) = (𝐹𝐶))
222220, 127, 221cnmptlimc 25741 . . . . . . . 8 (𝜑 → (𝐹𝐶) ∈ ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) lim 𝐶))
22343adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑋𝑌)) → (𝐹𝐶) ∈ ℂ)
224223fmpttd 7106 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)):(𝑋𝑌)⟶ℂ)
225224limcdif 25727 . . . . . . . . 9 (𝜑 → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) lim 𝐶) = (((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶))
226 resmpt 6027 . . . . . . . . . . 11 (((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋𝑌) → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)))
227146, 226mp1i 13 . . . . . . . . . 10 (𝜑 → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)))
228227oveq1d 7416 . . . . . . . . 9 (𝜑 → (((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)) lim 𝐶))
229225, 228eqtrd 2764 . . . . . . . 8 (𝜑 → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)) lim 𝐶))
230222, 229eleqtrd 2827 . . . . . . 7 (𝜑 → (𝐹𝐶) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)) lim 𝐶))
2315, 13, 14dvcl 25750 . . . . . . . . . 10 ((𝜑𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
23211, 231mpdan 684 . . . . . . . . 9 (𝜑𝐿 ∈ ℂ)
233232, 43opelxpd 5705 . . . . . . . 8 (𝜑 → ⟨𝐿, (𝐹𝐶)⟩ ∈ (ℂ × ℂ))
234185cncnpi 23104 . . . . . . . 8 (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (𝐹𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹𝐶)⟩))
235180, 233, 234sylancr 586 . . . . . . 7 (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹𝐶)⟩))
23671, 44, 73, 73, 3, 76, 217, 230, 235limccnp2 25743 . . . . . 6 (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶))) lim 𝐶))
237 df-mpt 5222 . . . . . . 7 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)))}
238237oveq1i 7411 . . . . . 6 ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶))) lim 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)))} lim 𝐶)
239236, 238eleqtrdi 2835 . . . . 5 (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)))} lim 𝐶))
240 ovmpot 7561 . . . . . 6 ((𝐿 ∈ ℂ ∧ (𝐹𝐶) ∈ ℂ) → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)) = (𝐿 · (𝐹𝐶)))
241232, 43, 240syl2anc 583 . . . . 5 (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)) = (𝐿 · (𝐹𝐶)))
24242adantr 480 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶𝑋)
24332, 242ffvelcdmd 7077 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐹𝐶) ∈ ℂ)
244 ovmpot 7561 . . . . . . . . . . 11 (((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) ∈ ℂ ∧ (𝐹𝐶) ∈ ℂ) → ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)) = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))
24571, 243, 244syl2anc 583 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)) = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))
246245eqeq2d 2735 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)) ↔ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))))
247246pm5.32da 578 . . . . . . . 8 (𝜑 → ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶))) ↔ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))))
248247opabbidv 5204 . . . . . . 7 (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))})
249 df-mpt 5222 . . . . . . 7 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))}
250248, 249eqtr4di 2782 . . . . . 6 (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)))} = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))))
251250oveq1d 7416 . . . . 5 (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹𝐶)))} lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))) lim 𝐶))
252239, 241, 2513eltr3d 2839 . . . 4 (𝜑 → (𝐿 · (𝐹𝐶)) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))) lim 𝐶))
2533addcn 24703 . . . . 5 + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
254182, 183mulcld 11231 . . . . . 6 (𝜑 → (𝐾 · (𝐺𝐶)) ∈ ℂ)
255232, 43mulcld 11231 . . . . . 6 (𝜑 → (𝐿 · (𝐹𝐶)) ∈ ℂ)
256254, 255opelxpd 5705 . . . . 5 (𝜑 → ⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩ ∈ (ℂ × ℂ))
257185cncnpi 23104 . . . . 5 (( + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩))
258253, 256, 257sylancr 586 . . . 4 (𝜑 → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩))
25960, 72, 73, 73, 3, 76, 202, 252, 258limccnp2 25743 . . 3 (𝜑 → ((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))) lim 𝐶))
26037, 243subcld 11568 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝑧) − (𝐹𝐶)) ∈ ℂ)
261260, 59mulcld 11231 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) ∈ ℂ)
26269adantr 480 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶𝑌)
26356, 262ffvelcdmd 7077 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐺𝐶) ∈ ℂ)
26459, 263subcld 11568 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐺𝑧) − (𝐺𝐶)) ∈ ℂ)
265264, 243mulcld 11231 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) ∈ ℂ)
26647, 242sseldd 3975 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
26748, 266subcld 11568 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑧𝐶) ∈ ℂ)
268261, 265, 267, 54divdird 12025 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) / (𝑧𝐶)) = (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) / (𝑧𝐶)) + ((((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) / (𝑧𝐶))))
26937, 59mulcld 11231 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝑧) · (𝐺𝑧)) ∈ ℂ)
270243, 59mulcld 11231 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝐶) · (𝐺𝑧)) ∈ ℂ)
271243, 263mulcld 11231 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝐶) · (𝐺𝐶)) ∈ ℂ)
272269, 270, 271npncand 11592 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝑧))) + (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶)))) = (((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
27337, 243, 59subdird 11668 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) = (((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝑧))))
274264, 243mulcomd 11232 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) = ((𝐹𝐶) · ((𝐺𝑧) − (𝐺𝐶))))
275243, 59, 263subdid 11667 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝐶) · ((𝐺𝑧) − (𝐺𝐶))) = (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
276274, 275eqtrd 2764 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) = (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
277273, 276oveq12d 7419 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) = ((((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝑧))) + (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶)))))
2786ffnd 6708 . . . . . . . . . . . 12 (𝜑𝐹 Fn 𝑋)
279278adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
28013ffnd 6708 . . . . . . . . . . . 12 (𝜑𝐺 Fn 𝑌)
281280adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
282 ssexg 5313 . . . . . . . . . . . . 13 ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
28346, 110, 282sylancl 585 . . . . . . . . . . . 12 (𝜑𝑋 ∈ V)
284283adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
285 ssexg 5313 . . . . . . . . . . . . 13 ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
28664, 110, 285sylancl 585 . . . . . . . . . . . 12 (𝜑𝑌 ∈ V)
287286adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
288 eqid 2724 . . . . . . . . . . 11 (𝑋𝑌) = (𝑋𝑌)
289 eqidd 2725 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝑧𝑋) → (𝐹𝑧) = (𝐹𝑧))
290 eqidd 2725 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝑧𝑌) → (𝐺𝑧) = (𝐺𝑧))
291279, 281, 284, 287, 288, 289, 290ofval 7674 . . . . . . . . . 10 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋𝑌)) → ((𝐹f · 𝐺)‘𝑧) = ((𝐹𝑧) · (𝐺𝑧)))
29235, 291mpdan 684 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹f · 𝐺)‘𝑧) = ((𝐹𝑧) · (𝐺𝑧)))
293 eqidd 2725 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝐶𝑋) → (𝐹𝐶) = (𝐹𝐶))
294 eqidd 2725 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝐶𝑌) → (𝐺𝐶) = (𝐺𝐶))
295279, 281, 284, 287, 288, 293, 294ofval 7674 . . . . . . . . . 10 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋𝑌)) → ((𝐹f · 𝐺)‘𝐶) = ((𝐹𝐶) · (𝐺𝐶)))
296127, 295mpidan 686 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹f · 𝐺)‘𝐶) = ((𝐹𝐶) · (𝐺𝐶)))
297292, 296oveq12d 7419 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) = (((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
298272, 277, 2973eqtr4d 2774 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) = (((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)))
299298oveq1d 7416 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) / (𝑧𝐶)) = ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶)))
300260, 59, 267, 54div23d 12024 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) / (𝑧𝐶)) = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)))
301264, 243, 267, 54div23d 12024 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) / (𝑧𝐶)) = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))
302300, 301oveq12d 7419 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) / (𝑧𝐶)) + ((((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) / (𝑧𝐶))) = (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))))
303268, 299, 3023eqtr3d 2772 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶)) = (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))))
304303mpteq2dva 5238 . . . 4 (𝜑 → (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))))
305304oveq1d 7416 . . 3 (𝜑 → ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))) lim 𝐶))
306259, 305eleqtrrd 2828 . 2 (𝜑 → ((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶))
307 eqid 2724 . . 3 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶)))
308 mulcl 11190 . . . . 5 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
309308adantl 481 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
310309, 6, 13, 283, 286, 288off 7681 . . 3 (𝜑 → (𝐹f · 𝐺):(𝑋𝑌)⟶ℂ)
3112, 3, 307, 5, 310, 84eldv 25749 . 2 (𝜑 → (𝐶(𝑆 D (𝐹f · 𝐺))((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ∧ ((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶))))
31231, 306, 311mpbir2and 710 1 (𝜑𝐶(𝑆 D (𝐹f · 𝐺))((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1533  wcel 2098  wne 2932  Vcvv 3466  cdif 3937  cun 3938  cin 3939  wss 3940  {csn 4620  cop 4626   cuni 4899   class class class wbr 5138  {copab 5200  cmpt 5221   × cxp 5664  dom cdm 5666  cres 5668  Rel wrel 5671   Fn wfn 6528  wf 6529  cfv 6533  (class class class)co 7401  cmpo 7403  f cof 7661  cc 11104   + caddc 11109   · cmul 11111  cmin 11441   / cdiv 11868  t crest 17365  TopOpenctopn 17366  fldccnfld 21228  Topctop 22717  TopOnctopon 22734  intcnt 22843   Cn ccn 23050   CnP ccnp 23051   ×t ctx 23386  cnccncf 24718   lim climc 25713   D cdv 25714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-icc 13328  df-fz 13482  df-fzo 13625  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-cn 23053  df-cnp 23054  df-tx 23388  df-hmeo 23581  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718
This theorem is referenced by:  dvmul  25794  dvmulf  25796  dvef  25834
  Copyright terms: Public domain W3C validator