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

Theorem dvmulbr 24551
Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 24553. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
dvadd.f (𝜑𝐹:𝑋⟶ℂ)
dvadd.x (𝜑𝑋𝑆)
dvadd.g (𝜑𝐺:𝑌⟶ℂ)
dvadd.y (𝜑𝑌𝑆)
dvaddbr.s (𝜑𝑆 ⊆ ℂ)
dvadd.k (𝜑𝐾𝑉)
dvadd.l (𝜑𝐿𝑉)
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 2824 . . . . . . 7 (𝐽t 𝑆) = (𝐽t 𝑆)
3 dvadd.j . . . . . . 7 𝐽 = (TopOpen‘ℂfld)
4 eqid 2824 . . . . . . 7 (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)))
5 dvaddbr.s . . . . . . 7 (𝜑𝑆 ⊆ ℂ)
6 dvadd.f . . . . . . 7 (𝜑𝐹:𝑋⟶ℂ)
7 dvadd.x . . . . . . 7 (𝜑𝑋𝑆)
82, 3, 4, 5, 6, 7eldv 24510 . . . . . 6 (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))))
91, 8mpbid 235 . . . . 5 (𝜑 → (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶)))
109simpld 498 . . . 4 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑋))
11 dvadd.bg . . . . . 6 (𝜑𝐶(𝑆 D 𝐺)𝐿)
12 eqid 2824 . . . . . . 7 (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)))
13 dvadd.g . . . . . . 7 (𝜑𝐺:𝑌⟶ℂ)
14 dvadd.y . . . . . . 7 (𝜑𝑌𝑆)
152, 3, 12, 5, 13, 14eldv 24510 . . . . . 6 (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))))
1611, 15mpbid 235 . . . . 5 (𝜑 → (𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶)))
1716simpld 498 . . . 4 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘𝑌))
1810, 17elind 4156 . . 3 (𝜑𝐶 ∈ (((int‘(𝐽t 𝑆))‘𝑋) ∩ ((int‘(𝐽t 𝑆))‘𝑌)))
193cnfldtopon 23397 . . . . . 6 𝐽 ∈ (TopOn‘ℂ)
20 resttopon 21775 . . . . . 6 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽t 𝑆) ∈ (TopOn‘𝑆))
2119, 5, 20sylancr 590 . . . . 5 (𝜑 → (𝐽t 𝑆) ∈ (TopOn‘𝑆))
22 topontop 21527 . . . . 5 ((𝐽t 𝑆) ∈ (TopOn‘𝑆) → (𝐽t 𝑆) ∈ Top)
2321, 22syl 17 . . . 4 (𝜑 → (𝐽t 𝑆) ∈ Top)
24 toponuni 21528 . . . . . 6 ((𝐽t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = (𝐽t 𝑆))
2521, 24syl 17 . . . . 5 (𝜑𝑆 = (𝐽t 𝑆))
267, 25sseqtrd 3993 . . . 4 (𝜑𝑋 (𝐽t 𝑆))
2714, 25sseqtrd 3993 . . . 4 (𝜑𝑌 (𝐽t 𝑆))
28 eqid 2824 . . . . 5 (𝐽t 𝑆) = (𝐽t 𝑆)
2928ntrin 21675 . . . 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 2919 . 2 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘(𝑋𝑌)))
326adantr 484 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33 inss1 4190 . . . . . . . . 9 (𝑋𝑌) ⊆ 𝑋
34 eldifi 4089 . . . . . . . . . 10 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋𝑌))
3534adantl 485 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋𝑌))
3633, 35sseldi 3951 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧𝑋)
3732, 36ffvelrnd 6845 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐹𝑧) ∈ ℂ)
385, 6, 7dvbss 24513 . . . . . . . . . 10 (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39 reldv 24482 . . . . . . . . . . 11 Rel (𝑆 D 𝐹)
40 releldm 5802 . . . . . . . . . . 11 ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
4139, 1, 40sylancr 590 . . . . . . . . . 10 (𝜑𝐶 ∈ dom (𝑆 D 𝐹))
4238, 41sseldd 3954 . . . . . . . . 9 (𝜑𝐶𝑋)
436, 42ffvelrnd 6845 . . . . . . . 8 (𝜑 → (𝐹𝐶) ∈ ℂ)
4443adantr 484 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐹𝐶) ∈ ℂ)
4537, 44subcld 10997 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝑧) − (𝐹𝐶)) ∈ ℂ)
467, 5sstrd 3963 . . . . . . . . 9 (𝜑𝑋 ⊆ ℂ)
4746adantr 484 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
4847, 36sseldd 3954 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
4946, 42sseldd 3954 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
5049adantr 484 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
5148, 50subcld 10997 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑧𝐶) ∈ ℂ)
52 eldifsni 4707 . . . . . . . 8 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) → 𝑧𝐶)
5352adantl 485 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧𝐶)
5448, 50, 53subne0d 11006 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑧𝐶) ≠ 0)
5545, 51, 54divcld 11416 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) ∈ ℂ)
5613adantr 484 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57 inss2 4191 . . . . . . 7 (𝑋𝑌) ⊆ 𝑌
5857, 35sseldi 3951 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧𝑌)
5956, 58ffvelrnd 6845 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐺𝑧) ∈ ℂ)
6055, 59mulcld 10661 . . . 4 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) ∈ ℂ)
61 ssdif 4102 . . . . . . . 8 ((𝑋𝑌) ⊆ 𝑌 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
6257, 61mp1i 13 . . . . . . 7 (𝜑 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
6362sselda 3953 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
6414, 5sstrd 3963 . . . . . . 7 (𝜑𝑌 ⊆ ℂ)
655, 13, 14dvbss 24513 . . . . . . . 8 (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66 reldv 24482 . . . . . . . . 9 Rel (𝑆 D 𝐺)
67 releldm 5802 . . . . . . . . 9 ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
6866, 11, 67sylancr 590 . . . . . . . 8 (𝜑𝐶 ∈ dom (𝑆 D 𝐺))
6965, 68sseldd 3954 . . . . . . 7 (𝜑𝐶𝑌)
7013, 64, 69dvlem 24508 . . . . . 6 ((𝜑𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) ∈ ℂ)
7163, 70syldan 594 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) ∈ ℂ)
7271, 44mulcld 10661 . . . 4 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)) ∈ ℂ)
73 ssidd 3976 . . . 4 (𝜑 → ℂ ⊆ ℂ)
74 txtopon 22205 . . . . . 6 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
7519, 19, 74mp2an 691 . . . . 5 (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
7675toponrestid 21535 . . . 4 (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ × ℂ))
779simprd 499 . . . . . 6 (𝜑𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
786, 46, 42dvlem 24508 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) ∈ ℂ)
7978fmpttd 6872 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80 ssdif 4102 . . . . . . . . 9 ((𝑋𝑌) ⊆ 𝑋 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
8133, 80mp1i 13 . . . . . . . 8 (𝜑 → ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
8246ssdifssd 4105 . . . . . . . 8 (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83 eqid 2824 . . . . . . . 8 (𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
8433, 7sstrid 3964 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋𝑌) ⊆ 𝑆)
8584, 25sseqtrd 3993 . . . . . . . . . . . . . 14 (𝜑 → (𝑋𝑌) ⊆ (𝐽t 𝑆))
86 difssd 4095 . . . . . . . . . . . . . 14 (𝜑 → ( (𝐽t 𝑆) ∖ 𝑋) ⊆ (𝐽t 𝑆))
8785, 86unssd 4148 . . . . . . . . . . . . 13 (𝜑 → ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋)) ⊆ (𝐽t 𝑆))
88 ssun1 4134 . . . . . . . . . . . . . 14 (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))
8988a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋)))
9028ntrss 21669 . . . . . . . . . . . . 13 (((𝐽t 𝑆) ∈ Top ∧ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋)) ⊆ (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))))
9123, 87, 89, 90syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))))
9291, 31sseldd 3954 . . . . . . . . . . 11 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))))
9392, 42elind 4156 . . . . . . . . . 10 (𝜑𝐶 ∈ (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋))
9433a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑋𝑌) ⊆ 𝑋)
95 eqid 2824 . . . . . . . . . . . . 13 ((𝐽t 𝑆) ↾t 𝑋) = ((𝐽t 𝑆) ↾t 𝑋)
9628, 95restntr 21796 . . . . . . . . . . . 12 (((𝐽t 𝑆) ∈ Top ∧ 𝑋 (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ 𝑋) → ((int‘((𝐽t 𝑆) ↾t 𝑋))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋))
9723, 26, 94, 96syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑋))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋))
983cnfldtop 23398 . . . . . . . . . . . . . . 15 𝐽 ∈ Top
9998a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ Top)
100 cnex 10618 . . . . . . . . . . . . . . 15 ℂ ∈ V
101 ssexg 5214 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
1025, 100, 101sylancl 589 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ V)
103 restabs 21779 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑋𝑆𝑆 ∈ V) → ((𝐽t 𝑆) ↾t 𝑋) = (𝐽t 𝑋))
10499, 7, 102, 103syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → ((𝐽t 𝑆) ↾t 𝑋) = (𝐽t 𝑋))
105104fveq2d 6667 . . . . . . . . . . . 12 (𝜑 → (int‘((𝐽t 𝑆) ↾t 𝑋)) = (int‘(𝐽t 𝑋)))
106105fveq1d 6665 . . . . . . . . . . 11 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑋))‘(𝑋𝑌)) = ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
10797, 106eqtr3d 2861 . . . . . . . . . 10 (𝜑 → (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
10893, 107eleqtrd 2918 . . . . . . . . 9 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
109 undif1 4407 . . . . . . . . . . . . 13 ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
11042snssd 4726 . . . . . . . . . . . . . 14 (𝜑 → {𝐶} ⊆ 𝑋)
111 ssequn2 4145 . . . . . . . . . . . . . 14 ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
112110, 111sylib 221 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
113109, 112syl5eq 2871 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
114113oveq2d 7167 . . . . . . . . . . 11 (𝜑 → (𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t 𝑋))
115114fveq2d 6667 . . . . . . . . . 10 (𝜑 → (int‘(𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽t 𝑋)))
116 undif1 4407 . . . . . . . . . . 11 (((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋𝑌) ∪ {𝐶})
11742, 69elind 4156 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ (𝑋𝑌))
118117snssd 4726 . . . . . . . . . . . 12 (𝜑 → {𝐶} ⊆ (𝑋𝑌))
119 ssequn2 4145 . . . . . . . . . . . 12 ({𝐶} ⊆ (𝑋𝑌) ↔ ((𝑋𝑌) ∪ {𝐶}) = (𝑋𝑌))
120118, 119sylib 221 . . . . . . . . . . 11 (𝜑 → ((𝑋𝑌) ∪ {𝐶}) = (𝑋𝑌))
121116, 120syl5eq 2871 . . . . . . . . . 10 (𝜑 → (((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋𝑌))
122115, 121fveq12d 6670 . . . . . . . . 9 (𝜑 → ((int‘(𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽t 𝑋))‘(𝑋𝑌)))
123108, 122eleqtrrd 2919 . . . . . . . 8 (𝜑𝐶 ∈ ((int‘(𝐽t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})))
12479, 81, 82, 3, 83, 123limcres 24498 . . . . . . 7 (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
12581resmptd 5897 . . . . . . . 8 (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))))
126125oveq1d 7166 . . . . . . 7 (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
127124, 126eqtr3d 2861 . . . . . 6 (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
12877, 127eleqtrd 2918 . . . . 5 (𝜑𝐾 ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶))) lim 𝐶))
129 eqid 2824 . . . . . . . . . 10 (𝐽t 𝑌) = (𝐽t 𝑌)
130129, 3dvcnp2 24532 . . . . . . . . 9 (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶))
1315, 13, 14, 68, 130syl31anc 1370 . . . . . . . 8 (𝜑𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶))
1323, 129cnplimc 24499 . . . . . . . . 9 ((𝑌 ⊆ ℂ ∧ 𝐶𝑌) → (𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶))))
13364, 69, 132syl2anc 587 . . . . . . . 8 (𝜑 → (𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶))))
134131, 133mpbid 235 . . . . . . 7 (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶)))
135134simprd 499 . . . . . 6 (𝜑 → (𝐺𝐶) ∈ (𝐺 lim 𝐶))
136 difss 4094 . . . . . . . . . 10 ((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋𝑌)
137136, 57sstri 3962 . . . . . . . . 9 ((𝑋𝑌) ∖ {𝐶}) ⊆ 𝑌
138137a1i 11 . . . . . . . 8 (𝜑 → ((𝑋𝑌) ∖ {𝐶}) ⊆ 𝑌)
139 eqid 2824 . . . . . . . 8 (𝐽t (𝑌 ∪ {𝐶})) = (𝐽t (𝑌 ∪ {𝐶}))
140 difssd 4095 . . . . . . . . . . . . . 14 (𝜑 → ( (𝐽t 𝑆) ∖ 𝑌) ⊆ (𝐽t 𝑆))
14185, 140unssd 4148 . . . . . . . . . . . . 13 (𝜑 → ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌)) ⊆ (𝐽t 𝑆))
142 ssun1 4134 . . . . . . . . . . . . . 14 (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))
143142a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌)))
14428ntrss 21669 . . . . . . . . . . . . 13 (((𝐽t 𝑆) ∈ Top ∧ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌)) ⊆ (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ ((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))))
14523, 141, 143, 144syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ⊆ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))))
146145, 31sseldd 3954 . . . . . . . . . . 11 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))))
147146, 69elind 4156 . . . . . . . . . 10 (𝜑𝐶 ∈ (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌))
14857a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑋𝑌) ⊆ 𝑌)
149 eqid 2824 . . . . . . . . . . . . 13 ((𝐽t 𝑆) ↾t 𝑌) = ((𝐽t 𝑆) ↾t 𝑌)
15028, 149restntr 21796 . . . . . . . . . . . 12 (((𝐽t 𝑆) ∈ Top ∧ 𝑌 (𝐽t 𝑆) ∧ (𝑋𝑌) ⊆ 𝑌) → ((int‘((𝐽t 𝑆) ↾t 𝑌))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌))
15123, 27, 148, 150syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑌))‘(𝑋𝑌)) = (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌))
152 restabs 21779 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑌𝑆𝑆 ∈ V) → ((𝐽t 𝑆) ↾t 𝑌) = (𝐽t 𝑌))
15399, 14, 102, 152syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → ((𝐽t 𝑆) ↾t 𝑌) = (𝐽t 𝑌))
154153fveq2d 6667 . . . . . . . . . . . 12 (𝜑 → (int‘((𝐽t 𝑆) ↾t 𝑌)) = (int‘(𝐽t 𝑌)))
155154fveq1d 6665 . . . . . . . . . . 11 (𝜑 → ((int‘((𝐽t 𝑆) ↾t 𝑌))‘(𝑋𝑌)) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
156151, 155eqtr3d 2861 . . . . . . . . . 10 (𝜑 → (((int‘(𝐽t 𝑆))‘((𝑋𝑌) ∪ ( (𝐽t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
157147, 156eleqtrd 2918 . . . . . . . . 9 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
15869snssd 4726 . . . . . . . . . . . . 13 (𝜑 → {𝐶} ⊆ 𝑌)
159 ssequn2 4145 . . . . . . . . . . . . 13 ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
160158, 159sylib 221 . . . . . . . . . . . 12 (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
161160oveq2d 7167 . . . . . . . . . . 11 (𝜑 → (𝐽t (𝑌 ∪ {𝐶})) = (𝐽t 𝑌))
162161fveq2d 6667 . . . . . . . . . 10 (𝜑 → (int‘(𝐽t (𝑌 ∪ {𝐶}))) = (int‘(𝐽t 𝑌)))
163162, 121fveq12d 6670 . . . . . . . . 9 (𝜑 → ((int‘(𝐽t (𝑌 ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
164157, 163eleqtrrd 2919 . . . . . . . 8 (𝜑𝐶 ∈ ((int‘(𝐽t (𝑌 ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})))
16513, 138, 64, 3, 139, 164limcres 24498 . . . . . . 7 (𝜑 → ((𝐺 ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = (𝐺 lim 𝐶))
16613, 138feqresmpt 6727 . . . . . . . 8 (𝜑 → (𝐺 ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)))
167166oveq1d 7166 . . . . . . 7 (𝜑 → ((𝐺 ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)) lim 𝐶))
168165, 167eqtr3d 2861 . . . . . 6 (𝜑 → (𝐺 lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)) lim 𝐶))
169135, 168eleqtrd 2918 . . . . 5 (𝜑 → (𝐺𝐶) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐺𝑧)) lim 𝐶))
1703mulcn 23481 . . . . . 6 · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
1715, 6, 7dvcl 24511 . . . . . . . 8 ((𝜑𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
1721, 171mpdan 686 . . . . . . 7 (𝜑𝐾 ∈ ℂ)
17313, 69ffvelrnd 6845 . . . . . . 7 (𝜑 → (𝐺𝐶) ∈ ℂ)
174172, 173opelxpd 5581 . . . . . 6 (𝜑 → ⟨𝐾, (𝐺𝐶)⟩ ∈ (ℂ × ℂ))
17575toponunii 21530 . . . . . . 7 (ℂ × ℂ) = (𝐽 ×t 𝐽)
176175cncnpi 21892 . . . . . 6 (( · ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (𝐺𝐶)⟩ ∈ (ℂ × ℂ)) → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺𝐶)⟩))
177170, 174, 176sylancr 590 . . . . 5 (𝜑 → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺𝐶)⟩))
17855, 59, 73, 73, 3, 76, 128, 169, 177limccnp2 24504 . . . 4 (𝜑 → (𝐾 · (𝐺𝐶)) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧))) lim 𝐶))
17916simprd 499 . . . . . 6 (𝜑𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
18070fmpttd 6872 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
18164ssdifssd 4105 . . . . . . . 8 (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
182 eqid 2824 . . . . . . . 8 (𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
183 undif1 4407 . . . . . . . . . . . . 13 ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
184183, 160syl5eq 2871 . . . . . . . . . . . 12 (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
185184oveq2d 7167 . . . . . . . . . . 11 (𝜑 → (𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽t 𝑌))
186185fveq2d 6667 . . . . . . . . . 10 (𝜑 → (int‘(𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽t 𝑌)))
187186, 121fveq12d 6670 . . . . . . . . 9 (𝜑 → ((int‘(𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽t 𝑌))‘(𝑋𝑌)))
188157, 187eleqtrrd 2919 . . . . . . . 8 (𝜑𝐶 ∈ ((int‘(𝐽t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋𝑌) ∖ {𝐶}) ∪ {𝐶})))
189180, 62, 181, 3, 182, 188limcres 24498 . . . . . . 7 (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
19062resmptd 5897 . . . . . . . 8 (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))))
191190oveq1d 7166 . . . . . . 7 (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
192189, 191eqtr3d 2861 . . . . . 6 (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
193179, 192eleqtrd 2918 . . . . 5 (𝜑𝐿 ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
19484, 5sstrd 3963 . . . . . . . 8 (𝜑 → (𝑋𝑌) ⊆ ℂ)
195 cncfmptc 23526 . . . . . . . 8 (((𝐹𝐶) ∈ ℂ ∧ (𝑋𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ∈ ((𝑋𝑌)–cn→ℂ))
19643, 194, 73, 195syl3anc 1368 . . . . . . 7 (𝜑 → (𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ∈ ((𝑋𝑌)–cn→ℂ))
197 eqidd 2825 . . . . . . 7 (𝑧 = 𝐶 → (𝐹𝐶) = (𝐹𝐶))
198196, 117, 197cnmptlimc 24502 . . . . . 6 (𝜑 → (𝐹𝐶) ∈ ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) lim 𝐶))
19943adantr 484 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑋𝑌)) → (𝐹𝐶) ∈ ℂ)
200199fmpttd 6872 . . . . . . . 8 (𝜑 → (𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)):(𝑋𝑌)⟶ℂ)
201200limcdif 24488 . . . . . . 7 (𝜑 → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) lim 𝐶) = (((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶))
202 resmpt 5894 . . . . . . . . 9 (((𝑋𝑌) ∖ {𝐶}) ⊆ (𝑋𝑌) → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)))
203136, 202mp1i 13 . . . . . . . 8 (𝜑 → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)))
204203oveq1d 7166 . . . . . . 7 (𝜑 → (((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) ↾ ((𝑋𝑌) ∖ {𝐶})) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)) lim 𝐶))
205201, 204eqtrd 2859 . . . . . 6 (𝜑 → ((𝑧 ∈ (𝑋𝑌) ↦ (𝐹𝐶)) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)) lim 𝐶))
206198, 205eleqtrd 2918 . . . . 5 (𝜑 → (𝐹𝐶) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (𝐹𝐶)) lim 𝐶))
2075, 13, 14dvcl 24511 . . . . . . . 8 ((𝜑𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
20811, 207mpdan 686 . . . . . . 7 (𝜑𝐿 ∈ ℂ)
209208, 43opelxpd 5581 . . . . . 6 (𝜑 → ⟨𝐿, (𝐹𝐶)⟩ ∈ (ℂ × ℂ))
210175cncnpi 21892 . . . . . 6 (( · ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (𝐹𝐶)⟩ ∈ (ℂ × ℂ)) → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹𝐶)⟩))
211170, 209, 210sylancr 590 . . . . 5 (𝜑 → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹𝐶)⟩))
21271, 44, 73, 73, 3, 76, 193, 206, 211limccnp2 24504 . . . 4 (𝜑 → (𝐿 · (𝐹𝐶)) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))) lim 𝐶))
2133addcn 23479 . . . . 5 + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
214172, 173mulcld 10661 . . . . . 6 (𝜑 → (𝐾 · (𝐺𝐶)) ∈ ℂ)
215208, 43mulcld 10661 . . . . . 6 (𝜑 → (𝐿 · (𝐹𝐶)) ∈ ℂ)
216214, 215opelxpd 5581 . . . . 5 (𝜑 → ⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩ ∈ (ℂ × ℂ))
217175cncnpi 21892 . . . . 5 (( + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩))
218213, 216, 217sylancr 590 . . . 4 (𝜑 → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺𝐶)), (𝐿 · (𝐹𝐶))⟩))
21960, 72, 73, 73, 3, 76, 178, 212, 218limccnp2 24504 . . 3 (𝜑 → ((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))) lim 𝐶))
22042adantr 484 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶𝑋)
22132, 220ffvelrnd 6845 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐹𝐶) ∈ ℂ)
22237, 221subcld 10997 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝑧) − (𝐹𝐶)) ∈ ℂ)
223222, 59mulcld 10661 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) ∈ ℂ)
22469adantr 484 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶𝑌)
22556, 224ffvelrnd 6845 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝐺𝐶) ∈ ℂ)
22659, 225subcld 10997 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐺𝑧) − (𝐺𝐶)) ∈ ℂ)
227226, 221mulcld 10661 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) ∈ ℂ)
22847, 220sseldd 3954 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
22948, 228subcld 10997 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (𝑧𝐶) ∈ ℂ)
230223, 227, 229, 54divdird 11454 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) / (𝑧𝐶)) = (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) / (𝑧𝐶)) + ((((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) / (𝑧𝐶))))
23137, 59mulcld 10661 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝑧) · (𝐺𝑧)) ∈ ℂ)
232221, 59mulcld 10661 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝐶) · (𝐺𝑧)) ∈ ℂ)
233221, 225mulcld 10661 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝐶) · (𝐺𝐶)) ∈ ℂ)
234231, 232, 233npncand 11021 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝑧))) + (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶)))) = (((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
23537, 221, 59subdird 11097 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) = (((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝑧))))
236226, 221mulcomd 10662 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) = ((𝐹𝐶) · ((𝐺𝑧) − (𝐺𝐶))))
237221, 59, 225subdid 11096 . . . . . . . . . 10 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹𝐶) · ((𝐺𝑧) − (𝐺𝐶))) = (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
238236, 237eqtrd 2859 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) = (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
239235, 238oveq12d 7169 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) = ((((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝑧))) + (((𝐹𝐶) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶)))))
2406ffnd 6506 . . . . . . . . . . . 12 (𝜑𝐹 Fn 𝑋)
241240adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
24213ffnd 6506 . . . . . . . . . . . 12 (𝜑𝐺 Fn 𝑌)
243242adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
244 ssexg 5214 . . . . . . . . . . . . 13 ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
24546, 100, 244sylancl 589 . . . . . . . . . . . 12 (𝜑𝑋 ∈ V)
246245adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
247 ssexg 5214 . . . . . . . . . . . . 13 ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
24864, 100, 247sylancl 589 . . . . . . . . . . . 12 (𝜑𝑌 ∈ V)
249248adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
250 eqid 2824 . . . . . . . . . . 11 (𝑋𝑌) = (𝑋𝑌)
251 eqidd 2825 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝑧𝑋) → (𝐹𝑧) = (𝐹𝑧))
252 eqidd 2825 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝑧𝑌) → (𝐺𝑧) = (𝐺𝑧))
253241, 243, 246, 249, 250, 251, 252ofval 7414 . . . . . . . . . 10 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋𝑌)) → ((𝐹f · 𝐺)‘𝑧) = ((𝐹𝑧) · (𝐺𝑧)))
25435, 253mpdan 686 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹f · 𝐺)‘𝑧) = ((𝐹𝑧) · (𝐺𝑧)))
255 eqidd 2825 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝐶𝑋) → (𝐹𝐶) = (𝐹𝐶))
256 eqidd 2825 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝐶𝑌) → (𝐺𝐶) = (𝐺𝐶))
257241, 243, 246, 249, 250, 255, 256ofval 7414 . . . . . . . . . 10 (((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋𝑌)) → ((𝐹f · 𝐺)‘𝐶) = ((𝐹𝐶) · (𝐺𝐶)))
258117, 257mpidan 688 . . . . . . . . 9 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((𝐹f · 𝐺)‘𝐶) = ((𝐹𝐶) · (𝐺𝐶)))
259254, 258oveq12d 7169 . . . . . . . 8 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) = (((𝐹𝑧) · (𝐺𝑧)) − ((𝐹𝐶) · (𝐺𝐶))))
260234, 239, 2593eqtr4d 2869 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) = (((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)))
261260oveq1d 7166 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) + (((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶))) / (𝑧𝐶)) = ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶)))
262222, 59, 229, 54div23d 11453 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) / (𝑧𝐶)) = ((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)))
263226, 221, 229, 54div23d 11453 . . . . . . 7 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) / (𝑧𝐶)) = ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))
264262, 263oveq12d 7169 . . . . . 6 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → (((((𝐹𝑧) − (𝐹𝐶)) · (𝐺𝑧)) / (𝑧𝐶)) + ((((𝐺𝑧) − (𝐺𝐶)) · (𝐹𝐶)) / (𝑧𝐶))) = (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))))
265230, 261, 2643eqtr3d 2867 . . . . 5 ((𝜑𝑧 ∈ ((𝑋𝑌) ∖ {𝐶})) → ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶)) = (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶))))
266265mpteq2dva 5148 . . . 4 (𝜑 → (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))))
267266oveq1d 7166 . . 3 (𝜑 → ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶) = ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ (((((𝐹𝑧) − (𝐹𝐶)) / (𝑧𝐶)) · (𝐺𝑧)) + ((((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) · (𝐹𝐶)))) lim 𝐶))
268219, 267eleqtrrd 2919 . 2 (𝜑 → ((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶))
269 eqid 2824 . . 3 (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) = (𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶)))
270 mulcl 10621 . . . . 5 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
271270adantl 485 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
272271, 6, 13, 245, 248, 250off 7420 . . 3 (𝜑 → (𝐹f · 𝐺):(𝑋𝑌)⟶ℂ)
2732, 3, 269, 5, 272, 84eldv 24510 . 2 (𝜑 → (𝐶(𝑆 D (𝐹f · 𝐺))((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽t 𝑆))‘(𝑋𝑌)) ∧ ((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))) ∈ ((𝑧 ∈ ((𝑋𝑌) ∖ {𝐶}) ↦ ((((𝐹f · 𝐺)‘𝑧) − ((𝐹f · 𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶))))
27431, 268, 273mpbir2and 712 1 (𝜑𝐶(𝑆 D (𝐹f · 𝐺))((𝐾 · (𝐺𝐶)) + (𝐿 · (𝐹𝐶))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wne 3014  Vcvv 3480  cdif 3916  cun 3917  cin 3918  wss 3919  {csn 4550  cop 4556   cuni 4824   class class class wbr 5053  cmpt 5133   × cxp 5541  dom cdm 5543  cres 5545  Rel wrel 5548   Fn wfn 6340  wf 6341  cfv 6345  (class class class)co 7151  f cof 7403  cc 10535   + caddc 10540   · cmul 10542  cmin 10870   / cdiv 11297  t crest 16696  TopOpenctopn 16697  fldccnfld 20100  Topctop 21507  TopOnctopon 21524  intcnt 21631   Cn ccn 21838   CnP ccnp 21839   ×t ctx 22174  cnccncf 23490   lim climc 24474   D cdv 24475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615  ax-addf 10616  ax-mulf 10617
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-isom 6354  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7405  df-om 7577  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-er 8287  df-map 8406  df-pm 8407  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-fi 8874  df-sup 8905  df-inf 8906  df-oi 8973  df-card 9367  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11637  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-q 12348  df-rp 12389  df-xneg 12506  df-xadd 12507  df-xmul 12508  df-icc 12744  df-fz 12897  df-fzo 13040  df-seq 13376  df-exp 13437  df-hash 13698  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-starv 16582  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-unif 16590  df-hom 16591  df-cco 16592  df-rest 16698  df-topn 16699  df-0g 16717  df-gsum 16718  df-topgen 16719  df-pt 16720  df-prds 16723  df-xrs 16777  df-qtop 16782  df-imas 16783  df-xps 16785  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-submnd 17959  df-mulg 18227  df-cntz 18449  df-cmn 18910  df-psmet 20092  df-xmet 20093  df-met 20094  df-bl 20095  df-mopn 20096  df-cnfld 20101  df-top 21508  df-topon 21525  df-topsp 21547  df-bases 21560  df-cld 21633  df-ntr 21634  df-cls 21635  df-cn 21841  df-cnp 21842  df-tx 22176  df-hmeo 22369  df-xms 22936  df-ms 22937  df-tms 22938  df-cncf 23492  df-limc 24478  df-dv 24479
This theorem is referenced by:  dvmul  24553  dvmulf  24555  dvef  24592
  Copyright terms: Public domain W3C validator