Step | Hyp | Ref
| Expression |
1 | | dvco.bg |
. . . 4
⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿) |
2 | | eqid 2726 |
. . . . 5
⊢ (𝐽 ↾t 𝑇) = (𝐽 ↾t 𝑇) |
3 | | dvco.j |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
4 | | eqid 2726 |
. . . . 5
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
5 | | dvcobr.t |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ ℂ) |
6 | | dvco.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑌⟶𝑋) |
7 | | dvco.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
8 | | dvcobr.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
9 | 7, 8 | sstrd 3990 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
10 | 6, 9 | fssd 6745 |
. . . . 5
⊢ (𝜑 → 𝐺:𝑌⟶ℂ) |
11 | | dvco.y |
. . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝑇) |
12 | 2, 3, 4, 5, 10, 11 | eldv 25918 |
. . . 4
⊢ (𝜑 → (𝐶(𝑇 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
13 | 1, 12 | mpbid 231 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
14 | 13 | simpld 493 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌)) |
15 | | dvco.bf |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾) |
16 | | dvco.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
17 | 8, 16, 7 | dvcl 25919 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐺‘𝐶)(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ) |
18 | 15, 17 | mpdan 685 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℂ) |
19 | 18 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝐾 ∈ ℂ) |
20 | 16 | adantr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐹:𝑋⟶ℂ) |
21 | | eldifi 4126 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) → 𝑧 ∈ 𝑌) |
22 | | ffvelcdm 7095 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) ∈ 𝑋) |
23 | 6, 21, 22 | syl2an 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝑧) ∈ 𝑋) |
24 | 20, 23 | ffvelcdmd 7099 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐹‘(𝐺‘𝑧)) ∈ ℂ) |
25 | 24 | adantr 479 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐹‘(𝐺‘𝑧)) ∈ ℂ) |
26 | 6 | adantr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐺:𝑌⟶𝑋) |
27 | 5, 10, 11 | dvbss 25921 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑇 D 𝐺) ⊆ 𝑌) |
28 | | reldv 25890 |
. . . . . . . . . . . . . . 15
⊢ Rel
(𝑇 D 𝐺) |
29 | | releldm 5950 |
. . . . . . . . . . . . . . 15
⊢ ((Rel
(𝑇 D 𝐺) ∧ 𝐶(𝑇 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑇 D 𝐺)) |
30 | 28, 1, 29 | sylancr 585 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ dom (𝑇 D 𝐺)) |
31 | 27, 30 | sseldd 3980 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
32 | 31 | adantr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐶 ∈ 𝑌) |
33 | 26, 32 | ffvelcdmd 7099 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝐶) ∈ 𝑋) |
34 | 20, 33 | ffvelcdmd 7099 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐹‘(𝐺‘𝐶)) ∈ ℂ) |
35 | 34 | adantr 479 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐹‘(𝐺‘𝐶)) ∈ ℂ) |
36 | 25, 35 | subcld 11621 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) ∈ ℂ) |
37 | 10 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝐺:𝑌⟶ℂ) |
38 | 21 | ad2antlr 725 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝑧 ∈ 𝑌) |
39 | 37, 38 | ffvelcdmd 7099 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐺‘𝑧) ∈ ℂ) |
40 | 31 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝐶 ∈ 𝑌) |
41 | 37, 40 | ffvelcdmd 7099 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐺‘𝐶) ∈ ℂ) |
42 | 39, 41 | subcld 11621 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ) |
43 | | simpr 483 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) |
44 | 39, 41 | subeq0ad 11631 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) = 0 ↔ (𝐺‘𝑧) = (𝐺‘𝐶))) |
45 | 44 | necon3abid 2967 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) ≠ 0 ↔ ¬ (𝐺‘𝑧) = (𝐺‘𝐶))) |
46 | 43, 45 | mpbird 256 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ≠ 0) |
47 | 36, 42, 46 | divcld 12041 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) ∈ ℂ) |
48 | 19, 47 | ifclda 4568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) ∈ ℂ) |
49 | 11, 5 | sstrd 3990 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
50 | 10, 49, 31 | dvlem 25916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
51 | | ssidd 4003 |
. . . . . 6
⊢ (𝜑 → ℂ ⊆
ℂ) |
52 | 3 | cnfldtopon 24790 |
. . . . . . . 8
⊢ 𝐽 ∈
(TopOn‘ℂ) |
53 | | txtopon 23586 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐽 ∈
(TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ ×
ℂ))) |
54 | 52, 52, 53 | mp2an 690 |
. . . . . . 7
⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ
× ℂ)) |
55 | 54 | toponrestid 22914 |
. . . . . 6
⊢ (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ ×
ℂ)) |
56 | 23 | anim1i 613 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶)) → ((𝐺‘𝑧) ∈ 𝑋 ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶))) |
57 | | eldifsn 4795 |
. . . . . . . . 9
⊢ ((𝐺‘𝑧) ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↔ ((𝐺‘𝑧) ∈ 𝑋 ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶))) |
58 | 56, 57 | sylibr 233 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶)) → (𝐺‘𝑧) ∈ (𝑋 ∖ {(𝐺‘𝐶)})) |
59 | 58 | anasss 465 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶))) → (𝐺‘𝑧) ∈ (𝑋 ∖ {(𝐺‘𝐶)})) |
60 | | eldifsni 4799 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) → 𝑦 ≠ (𝐺‘𝐶)) |
61 | | ifnefalse 4545 |
. . . . . . . . . 10
⊢ (𝑦 ≠ (𝐺‘𝐶) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
63 | 62 | adantl 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)})) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
64 | 6, 31 | ffvelcdmd 7099 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝐶) ∈ 𝑋) |
65 | 16, 9, 64 | dvlem 25916 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)})) → (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))) ∈ ℂ) |
66 | 63, 65 | eqeltrd 2826 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)})) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) ∈ ℂ) |
67 | | limcresi 25905 |
. . . . . . . . 9
⊢ (𝐺 limℂ 𝐶) ⊆ ((𝐺 ↾ (𝑌 ∖ {𝐶})) limℂ 𝐶) |
68 | 6 | feqmptd 6971 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧))) |
69 | 68 | reseq1d 5988 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ↾ (𝑌 ∖ {𝐶})) = ((𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧)) ↾ (𝑌 ∖ {𝐶}))) |
70 | | difss 4131 |
. . . . . . . . . . . 12
⊢ (𝑌 ∖ {𝐶}) ⊆ 𝑌 |
71 | | resmpt 6046 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∖ {𝐶}) ⊆ 𝑌 → ((𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧)) ↾ (𝑌 ∖ {𝐶})) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧))) |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧)) ↾ (𝑌 ∖ {𝐶})) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) |
73 | 69, 72 | eqtrdi 2782 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ↾ (𝑌 ∖ {𝐶})) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧))) |
74 | 73 | oveq1d 7439 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 ↾ (𝑌 ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
75 | 67, 74 | sseqtrid 4032 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 limℂ 𝐶) ⊆ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
76 | | eqid 2726 |
. . . . . . . . . . . 12
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌) |
77 | 76, 3 | dvcnp2 25940 |
. . . . . . . . . . 11
⊢ (((𝑇 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑇) ∧ 𝐶 ∈ dom (𝑇 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
78 | 5, 10, 11, 30, 77 | syl31anc 1370 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
79 | 3, 76 | cnplimc 25907 |
. . . . . . . . . . 11
⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
80 | 49, 31, 79 | syl2anc 582 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
81 | 78, 80 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶))) |
82 | 81 | simprd 494 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)) |
83 | 75, 82 | sseldd 3980 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
84 | | eqid 2726 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
85 | | eqid 2726 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
86 | 84, 3, 85, 8, 16, 7 | eldv 25918 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺‘𝐶)(𝑆 D 𝐹)𝐾 ↔ ((𝐺‘𝐶) ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶))))) |
87 | 15, 86 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺‘𝐶) ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶)))) |
88 | 87 | simprd 494 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶))) |
89 | 62 | mpteq2ia 5256 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))))) = (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
90 | 89 | oveq1i 7434 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))))) limℂ (𝐺‘𝐶)) = ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶)) |
91 | 88, 90 | eleqtrrdi 2837 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))))) limℂ (𝐺‘𝐶))) |
92 | | eqeq1 2730 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑧) → (𝑦 = (𝐺‘𝐶) ↔ (𝐺‘𝑧) = (𝐺‘𝐶))) |
93 | | fveq2 6901 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑧))) |
94 | 93 | oveq1d 7439 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) = ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶)))) |
95 | | oveq1 7431 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑧) → (𝑦 − (𝐺‘𝐶)) = ((𝐺‘𝑧) − (𝐺‘𝐶))) |
96 | 94, 95 | oveq12d 7442 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑧) → (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) |
97 | 92, 96 | ifbieq2d 4559 |
. . . . . . 7
⊢ (𝑦 = (𝐺‘𝑧) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))) |
98 | | iftrue 4539 |
. . . . . . . 8
⊢ ((𝐺‘𝑧) = (𝐺‘𝐶) → if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) = 𝐾) |
99 | 98 | ad2antll 727 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ (𝐺‘𝑧) = (𝐺‘𝐶))) → if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) = 𝐾) |
100 | 59, 66, 83, 91, 97, 99 | limcco 25913 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))) limℂ 𝐶)) |
101 | 13 | simprd 494 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
102 | 3 | mpomulcn 24876 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
103 | 5, 10, 11 | dvcl 25919 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶(𝑇 D 𝐺)𝐿) → 𝐿 ∈ ℂ) |
104 | 1, 103 | mpdan 685 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ ℂ) |
105 | 18, 104 | opelxpd 5721 |
. . . . . . 7
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ (ℂ ×
ℂ)) |
106 | 54 | toponunii 22909 |
. . . . . . . 8
⊢ (ℂ
× ℂ) = ∪ (𝐽 ×t 𝐽) |
107 | 106 | cncnpi 23273 |
. . . . . . 7
⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 〈𝐾, 𝐿〉 ∈ (ℂ × ℂ))
→ (𝑢 ∈ ℂ,
𝑣 ∈ ℂ ↦
(𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, 𝐿〉)) |
108 | 102, 105,
107 | sylancr 585 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, 𝐿〉)) |
109 | 48, 50, 51, 51, 3, 55, 100, 101, 108 | limccnp2 25912 |
. . . . 5
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
110 | | df-mpt 5237 |
. . . . . 6
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} |
111 | 110 | oveq1i 7434 |
. . . . 5
⊢ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶) = ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶) |
112 | 109, 111 | eleqtrdi 2836 |
. . . 4
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) ∈ ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶)) |
113 | | ovmpot 7587 |
. . . . 5
⊢ ((𝐾 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) = (𝐾 · 𝐿)) |
114 | 18, 104, 113 | syl2anc 582 |
. . . 4
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) = (𝐾 · 𝐿)) |
115 | | ovmpot 7587 |
. . . . . . . . 9
⊢
((if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) ∈ ℂ ∧ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
116 | 48, 50, 115 | syl2anc 582 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
117 | 116 | eqeq2d 2737 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↔ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))) |
118 | 117 | pm5.32da 577 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) ↔ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))))) |
119 | 118 | opabbidv 5219 |
. . . . 5
⊢ (𝜑 → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))}) |
120 | | df-mpt 5237 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} |
121 | 120 | eqcomi 2735 |
. . . . . . . 8
⊢
{〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
122 | 121 | eqeq2i 2739 |
. . . . . . 7
⊢
({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} ↔ {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))) |
123 | 122 | biimpi 215 |
. . . . . 6
⊢
({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))) |
124 | 123 | oveq1d 7439 |
. . . . 5
⊢
({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} → ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
125 | 119, 124 | syl 17 |
. . . 4
⊢ (𝜑 → ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
126 | 112, 114,
125 | 3eltr3d 2840 |
. . 3
⊢ (𝜑 → (𝐾 · 𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
127 | | oveq1 7431 |
. . . . . . . 8
⊢ (𝐾 = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → (𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
128 | 127 | eqeq1d 2728 |
. . . . . . 7
⊢ (𝐾 = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → ((𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) ↔ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)))) |
129 | | oveq1 7431 |
. . . . . . . 8
⊢ ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
130 | 129 | eqeq1d 2728 |
. . . . . . 7
⊢ ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → (((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) ↔ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)))) |
131 | 19 | mul01d 11463 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐾 · 0) = 0) |
132 | 9 | adantr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑋 ⊆ ℂ) |
133 | 132, 23 | sseldd 3980 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ) |
134 | 132, 33 | sseldd 3980 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ) |
135 | 133, 134 | subeq0ad 11631 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) = 0 ↔ (𝐺‘𝑧) = (𝐺‘𝐶))) |
136 | 135 | biimpar 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐺‘𝑧) − (𝐺‘𝐶)) = 0) |
137 | 136 | oveq1d 7439 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) = (0 / (𝑧 − 𝐶))) |
138 | 49 | adantr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑌 ⊆ ℂ) |
139 | 21 | adantl 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑧 ∈ 𝑌) |
140 | 138, 139 | sseldd 3980 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑧 ∈ ℂ) |
141 | 138, 32 | sseldd 3980 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐶 ∈ ℂ) |
142 | 140, 141 | subcld 11621 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ) |
143 | | eldifsni 4799 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) → 𝑧 ≠ 𝐶) |
144 | 143 | adantl 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑧 ≠ 𝐶) |
145 | 140, 141,
144 | subne0d 11630 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0) |
146 | 142, 145 | div0d 12040 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (0 / (𝑧 − 𝐶)) = 0) |
147 | 146 | adantr 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (0 / (𝑧 − 𝐶)) = 0) |
148 | 137, 147 | eqtrd 2766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) = 0) |
149 | 148 | oveq2d 7440 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝐾 · 0)) |
150 | | fveq2 6901 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑧) = (𝐺‘𝐶) → (𝐹‘(𝐺‘𝑧)) = (𝐹‘(𝐺‘𝐶))) |
151 | 24, 34 | subeq0ad 11631 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) = 0 ↔ (𝐹‘(𝐺‘𝑧)) = (𝐹‘(𝐺‘𝐶)))) |
152 | 150, 151 | imbitrrid 245 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((𝐺‘𝑧) = (𝐺‘𝐶) → ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) = 0)) |
153 | 152 | imp 405 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) = 0) |
154 | 153 | oveq1d 7439 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) = (0 / (𝑧 − 𝐶))) |
155 | 154, 147 | eqtrd 2766 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) = 0) |
156 | 131, 149,
155 | 3eqtr4d 2776 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
157 | 142 | adantr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝑧 − 𝐶) ∈ ℂ) |
158 | 145 | adantr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝑧 − 𝐶) ≠ 0) |
159 | 36, 42, 157, 46, 158 | dmdcan2d 12071 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
160 | 128, 130,
156, 159 | ifbothda 4571 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
161 | | fvco3 7001 |
. . . . . . . . 9
⊢ ((𝐺:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → ((𝐹 ∘ 𝐺)‘𝑧) = (𝐹‘(𝐺‘𝑧))) |
162 | 6, 21, 161 | syl2an 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((𝐹 ∘ 𝐺)‘𝑧) = (𝐹‘(𝐺‘𝑧))) |
163 | 6, 31 | fvco3d 7002 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) |
164 | 163 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) |
165 | 162, 164 | oveq12d 7442 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) = ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶)))) |
166 | 165 | oveq1d 7439 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
167 | 160, 166 | eqtr4d 2769 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
168 | 167 | mpteq2dva 5253 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶)))) |
169 | 168 | oveq1d 7439 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
170 | 126, 169 | eleqtrd 2828 |
. 2
⊢ (𝜑 → (𝐾 · 𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
171 | | eqid 2726 |
. . 3
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
172 | 16, 6 | fcod 6754 |
. . 3
⊢ (𝜑 → (𝐹 ∘ 𝐺):𝑌⟶ℂ) |
173 | 2, 3, 171, 5, 172, 11 | eldv 25918 |
. 2
⊢ (𝜑 → (𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿) ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌) ∧ (𝐾 · 𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
174 | 14, 170, 173 | mpbir2and 711 |
1
⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿)) |