| Step | Hyp | Ref
| Expression |
| 1 | | dvco.bg |
. . . 4
⊢ (𝜑 → 𝐶(𝑇 D 𝐺)𝐿) |
| 2 | | eqid 2737 |
. . . . 5
⊢ (𝐽 ↾t 𝑇) = (𝐽 ↾t 𝑇) |
| 3 | | dvco.j |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 4 | | eqid 2737 |
. . . . 5
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
| 5 | | dvcobr.t |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ ℂ) |
| 6 | | dvco.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑌⟶𝑋) |
| 7 | | dvco.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
| 8 | | dvcobr.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 9 | 7, 8 | sstrd 3994 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
| 10 | 6, 9 | fssd 6753 |
. . . . 5
⊢ (𝜑 → 𝐺:𝑌⟶ℂ) |
| 11 | | dvco.y |
. . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝑇) |
| 12 | 2, 3, 4, 5, 10, 11 | eldv 25933 |
. . . 4
⊢ (𝜑 → (𝐶(𝑇 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
| 13 | 1, 12 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
| 14 | 13 | simpld 494 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌)) |
| 15 | | dvco.bf |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝐶)(𝑆 D 𝐹)𝐾) |
| 16 | | dvco.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
| 17 | 8, 16, 7 | dvcl 25934 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐺‘𝐶)(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ) |
| 18 | 15, 17 | mpdan 687 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 19 | 18 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝐾 ∈ ℂ) |
| 20 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐹:𝑋⟶ℂ) |
| 21 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) → 𝑧 ∈ 𝑌) |
| 22 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) ∈ 𝑋) |
| 23 | 6, 21, 22 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝑧) ∈ 𝑋) |
| 24 | 20, 23 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐹‘(𝐺‘𝑧)) ∈ ℂ) |
| 25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐹‘(𝐺‘𝑧)) ∈ ℂ) |
| 26 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐺:𝑌⟶𝑋) |
| 27 | 5, 10, 11 | dvbss 25936 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑇 D 𝐺) ⊆ 𝑌) |
| 28 | | reldv 25905 |
. . . . . . . . . . . . . . 15
⊢ Rel
(𝑇 D 𝐺) |
| 29 | | releldm 5955 |
. . . . . . . . . . . . . . 15
⊢ ((Rel
(𝑇 D 𝐺) ∧ 𝐶(𝑇 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑇 D 𝐺)) |
| 30 | 28, 1, 29 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ dom (𝑇 D 𝐺)) |
| 31 | 27, 30 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐶 ∈ 𝑌) |
| 33 | 26, 32 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝐶) ∈ 𝑋) |
| 34 | 20, 33 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐹‘(𝐺‘𝐶)) ∈ ℂ) |
| 35 | 34 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐹‘(𝐺‘𝐶)) ∈ ℂ) |
| 36 | 25, 35 | subcld 11620 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) ∈ ℂ) |
| 37 | 10 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝐺:𝑌⟶ℂ) |
| 38 | 21 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝑧 ∈ 𝑌) |
| 39 | 37, 38 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐺‘𝑧) ∈ ℂ) |
| 40 | 31 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → 𝐶 ∈ 𝑌) |
| 41 | 37, 40 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐺‘𝐶) ∈ ℂ) |
| 42 | 39, 41 | subcld 11620 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ) |
| 43 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) |
| 44 | 39, 41 | subeq0ad 11630 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) = 0 ↔ (𝐺‘𝑧) = (𝐺‘𝐶))) |
| 45 | 44 | necon3abid 2977 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) ≠ 0 ↔ ¬ (𝐺‘𝑧) = (𝐺‘𝐶))) |
| 46 | 43, 45 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ≠ 0) |
| 47 | 36, 42, 46 | divcld 12043 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) ∈ ℂ) |
| 48 | 19, 47 | ifclda 4561 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) ∈ ℂ) |
| 49 | 11, 5 | sstrd 3994 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
| 50 | 10, 49, 31 | dvlem 25931 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
| 51 | | ssidd 4007 |
. . . . . 6
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 52 | 3 | cnfldtopon 24803 |
. . . . . . . 8
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 53 | | txtopon 23599 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐽 ∈
(TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ ×
ℂ))) |
| 54 | 52, 52, 53 | mp2an 692 |
. . . . . . 7
⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ
× ℂ)) |
| 55 | 54 | toponrestid 22927 |
. . . . . 6
⊢ (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ ×
ℂ)) |
| 56 | 23 | anim1i 615 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶)) → ((𝐺‘𝑧) ∈ 𝑋 ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶))) |
| 57 | | eldifsn 4786 |
. . . . . . . . 9
⊢ ((𝐺‘𝑧) ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↔ ((𝐺‘𝑧) ∈ 𝑋 ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶))) |
| 58 | 56, 57 | sylibr 234 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶)) → (𝐺‘𝑧) ∈ (𝑋 ∖ {(𝐺‘𝐶)})) |
| 59 | 58 | anasss 466 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ (𝐺‘𝑧) ≠ (𝐺‘𝐶))) → (𝐺‘𝑧) ∈ (𝑋 ∖ {(𝐺‘𝐶)})) |
| 60 | | eldifsni 4790 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) → 𝑦 ≠ (𝐺‘𝐶)) |
| 61 | | ifnefalse 4537 |
. . . . . . . . . 10
⊢ (𝑦 ≠ (𝐺‘𝐶) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
| 63 | 62 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)})) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
| 64 | 6, 31 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝐶) ∈ 𝑋) |
| 65 | 16, 9, 64 | dvlem 25931 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)})) → (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))) ∈ ℂ) |
| 66 | 63, 65 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)})) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) ∈ ℂ) |
| 67 | | limcresi 25920 |
. . . . . . . . 9
⊢ (𝐺 limℂ 𝐶) ⊆ ((𝐺 ↾ (𝑌 ∖ {𝐶})) limℂ 𝐶) |
| 68 | 6 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧))) |
| 69 | 68 | reseq1d 5996 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ↾ (𝑌 ∖ {𝐶})) = ((𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧)) ↾ (𝑌 ∖ {𝐶}))) |
| 70 | | difss 4136 |
. . . . . . . . . . . 12
⊢ (𝑌 ∖ {𝐶}) ⊆ 𝑌 |
| 71 | | resmpt 6055 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∖ {𝐶}) ⊆ 𝑌 → ((𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧)) ↾ (𝑌 ∖ {𝐶})) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧))) |
| 72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑌 ↦ (𝐺‘𝑧)) ↾ (𝑌 ∖ {𝐶})) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) |
| 73 | 69, 72 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ↾ (𝑌 ∖ {𝐶})) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧))) |
| 74 | 73 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 ↾ (𝑌 ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
| 75 | 67, 74 | sseqtrid 4026 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 limℂ 𝐶) ⊆ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
| 76 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌) |
| 77 | 76, 3 | dvcnp2 25955 |
. . . . . . . . . . 11
⊢ (((𝑇 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑇) ∧ 𝐶 ∈ dom (𝑇 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
| 78 | 5, 10, 11, 30, 77 | syl31anc 1375 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
| 79 | 3, 76 | cnplimc 25922 |
. . . . . . . . . . 11
⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
| 80 | 49, 31, 79 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
| 81 | 78, 80 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶))) |
| 82 | 81 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)) |
| 83 | 75, 82 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
| 84 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
| 85 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
| 86 | 84, 3, 85, 8, 16, 7 | eldv 25933 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺‘𝐶)(𝑆 D 𝐹)𝐾 ↔ ((𝐺‘𝐶) ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶))))) |
| 87 | 15, 86 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺‘𝐶) ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶)))) |
| 88 | 87 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶))) |
| 89 | 62 | mpteq2ia 5245 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))))) = (𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) |
| 90 | 89 | oveq1i 7441 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))))) limℂ (𝐺‘𝐶)) = ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) limℂ (𝐺‘𝐶)) |
| 91 | 88, 90 | eleqtrrdi 2852 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ((𝑦 ∈ (𝑋 ∖ {(𝐺‘𝐶)}) ↦ if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))))) limℂ (𝐺‘𝐶))) |
| 92 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑧) → (𝑦 = (𝐺‘𝐶) ↔ (𝐺‘𝑧) = (𝐺‘𝐶))) |
| 93 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺‘𝑧) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑧))) |
| 94 | 93 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑧) → ((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) = ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶)))) |
| 95 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺‘𝑧) → (𝑦 − (𝐺‘𝐶)) = ((𝐺‘𝑧) − (𝐺‘𝐶))) |
| 96 | 94, 95 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑧) → (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) |
| 97 | 92, 96 | ifbieq2d 4552 |
. . . . . . 7
⊢ (𝑦 = (𝐺‘𝑧) → if(𝑦 = (𝐺‘𝐶), 𝐾, (((𝐹‘𝑦) − (𝐹‘(𝐺‘𝐶))) / (𝑦 − (𝐺‘𝐶)))) = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))) |
| 98 | | iftrue 4531 |
. . . . . . . 8
⊢ ((𝐺‘𝑧) = (𝐺‘𝐶) → if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) = 𝐾) |
| 99 | 98 | ad2antll 729 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ (𝐺‘𝑧) = (𝐺‘𝐶))) → if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) = 𝐾) |
| 100 | 59, 66, 83, 91, 97, 99 | limcco 25928 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))) limℂ 𝐶)) |
| 101 | 13 | simprd 495 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
| 102 | 3 | mpomulcn 24891 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
| 103 | 5, 10, 11 | dvcl 25934 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶(𝑇 D 𝐺)𝐿) → 𝐿 ∈ ℂ) |
| 104 | 1, 103 | mpdan 687 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ ℂ) |
| 105 | 18, 104 | opelxpd 5724 |
. . . . . . 7
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ (ℂ ×
ℂ)) |
| 106 | 54 | toponunii 22922 |
. . . . . . . 8
⊢ (ℂ
× ℂ) = ∪ (𝐽 ×t 𝐽) |
| 107 | 106 | cncnpi 23286 |
. . . . . . 7
⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 〈𝐾, 𝐿〉 ∈ (ℂ × ℂ))
→ (𝑢 ∈ ℂ,
𝑣 ∈ ℂ ↦
(𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, 𝐿〉)) |
| 108 | 102, 105,
107 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, 𝐿〉)) |
| 109 | 48, 50, 51, 51, 3, 55, 100, 101, 108 | limccnp2 25927 |
. . . . 5
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
| 110 | | df-mpt 5226 |
. . . . . 6
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} |
| 111 | 110 | oveq1i 7441 |
. . . . 5
⊢ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶) = ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶) |
| 112 | 109, 111 | eleqtrdi 2851 |
. . . 4
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) ∈ ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶)) |
| 113 | | ovmpot 7594 |
. . . . 5
⊢ ((𝐾 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) = (𝐾 · 𝐿)) |
| 114 | 18, 104, 113 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝐿) = (𝐾 · 𝐿)) |
| 115 | | ovmpot 7594 |
. . . . . . . . 9
⊢
((if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) ∈ ℂ ∧ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
| 116 | 48, 50, 115 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
| 117 | 116 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↔ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))) |
| 118 | 117 | pm5.32da 579 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) ↔ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))))) |
| 119 | 118 | opabbidv 5209 |
. . . . 5
⊢ (𝜑 → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))}) |
| 120 | | df-mpt 5226 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} |
| 121 | 120 | eqcomi 2746 |
. . . . . . . 8
⊢
{〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
| 122 | 121 | eqeq2i 2750 |
. . . . . . 7
⊢
({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} ↔ {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))) |
| 123 | 122 | biimpi 216 |
. . . . . 6
⊢
({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))) |
| 124 | 123 | oveq1d 7446 |
. . . . 5
⊢
({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} → ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
| 125 | 119, 124 | syl 17 |
. . . 4
⊢ (𝜑 → ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ (𝑌 ∖ {𝐶}) ∧ 𝑤 = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))} limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
| 126 | 112, 114,
125 | 3eltr3d 2855 |
. . 3
⊢ (𝜑 → (𝐾 · 𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
| 127 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝐾 = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → (𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
| 128 | 127 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝐾 = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → ((𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) ↔ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)))) |
| 129 | | oveq1 7438 |
. . . . . . . 8
⊢ ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
| 130 | 129 | eqeq1d 2739 |
. . . . . . 7
⊢ ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) = if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) → (((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) ↔ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)))) |
| 131 | 19 | mul01d 11460 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐾 · 0) = 0) |
| 132 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑋 ⊆ ℂ) |
| 133 | 132, 23 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ) |
| 134 | 132, 33 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ) |
| 135 | 133, 134 | subeq0ad 11630 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) = 0 ↔ (𝐺‘𝑧) = (𝐺‘𝐶))) |
| 136 | 135 | biimpar 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐺‘𝑧) − (𝐺‘𝐶)) = 0) |
| 137 | 136 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) = (0 / (𝑧 − 𝐶))) |
| 138 | 49 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑌 ⊆ ℂ) |
| 139 | 21 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑧 ∈ 𝑌) |
| 140 | 138, 139 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑧 ∈ ℂ) |
| 141 | 138, 32 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝐶 ∈ ℂ) |
| 142 | 140, 141 | subcld 11620 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ) |
| 143 | | eldifsni 4790 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) → 𝑧 ≠ 𝐶) |
| 144 | 143 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → 𝑧 ≠ 𝐶) |
| 145 | 140, 141,
144 | subne0d 11629 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0) |
| 146 | 142, 145 | div0d 12042 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (0 / (𝑧 − 𝐶)) = 0) |
| 147 | 146 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (0 / (𝑧 − 𝐶)) = 0) |
| 148 | 137, 147 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) = 0) |
| 149 | 148 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝐾 · 0)) |
| 150 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑧) = (𝐺‘𝐶) → (𝐹‘(𝐺‘𝑧)) = (𝐹‘(𝐺‘𝐶))) |
| 151 | 24, 34 | subeq0ad 11630 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) = 0 ↔ (𝐹‘(𝐺‘𝑧)) = (𝐹‘(𝐺‘𝐶)))) |
| 152 | 150, 151 | imbitrrid 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((𝐺‘𝑧) = (𝐺‘𝐶) → ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) = 0)) |
| 153 | 152 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) = 0) |
| 154 | 153 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) = (0 / (𝑧 − 𝐶))) |
| 155 | 154, 147 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶)) = 0) |
| 156 | 131, 149,
155 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝐾 · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
| 157 | 142 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝑧 − 𝐶) ∈ ℂ) |
| 158 | 145 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → (𝑧 − 𝐶) ≠ 0) |
| 159 | 36, 42, 157, 46, 158 | dmdcan2d 12073 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) ∧ ¬ (𝐺‘𝑧) = (𝐺‘𝐶)) → ((((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
| 160 | 128, 130,
156, 159 | ifbothda 4564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
| 161 | | fvco3 7008 |
. . . . . . . . 9
⊢ ((𝐺:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → ((𝐹 ∘ 𝐺)‘𝑧) = (𝐹‘(𝐺‘𝑧))) |
| 162 | 6, 21, 161 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((𝐹 ∘ 𝐺)‘𝑧) = (𝐹‘(𝐺‘𝑧))) |
| 163 | 6, 31 | fvco3d 7009 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) |
| 164 | 163 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) |
| 165 | 162, 164 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) = ((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶)))) |
| 166 | 165 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / (𝑧 − 𝐶))) |
| 167 | 160, 166 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
| 168 | 167 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶)))) |
| 169 | 168 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (if((𝐺‘𝑧) = (𝐺‘𝐶), 𝐾, (((𝐹‘(𝐺‘𝑧)) − (𝐹‘(𝐺‘𝐶))) / ((𝐺‘𝑧) − (𝐺‘𝐶)))) · (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
| 170 | 126, 169 | eleqtrd 2843 |
. 2
⊢ (𝜑 → (𝐾 · 𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
| 171 | | eqid 2737 |
. . 3
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
| 172 | 16, 6 | fcod 6761 |
. . 3
⊢ (𝜑 → (𝐹 ∘ 𝐺):𝑌⟶ℂ) |
| 173 | 2, 3, 171, 5, 172, 11 | eldv 25933 |
. 2
⊢ (𝜑 → (𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿) ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑇))‘𝑌) ∧ (𝐾 · 𝐿) ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ ((((𝐹 ∘ 𝐺)‘𝑧) − ((𝐹 ∘ 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
| 174 | 14, 170, 173 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐶(𝑇 D (𝐹 ∘ 𝐺))(𝐾 · 𝐿)) |