Step | Hyp | Ref
| Expression |
1 | | dvf 24804 |
. . . . 5
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ) |
3 | 2 | ffund 6549 |
. . 3
⊢ (𝜑 → Fun (ℝ D 𝐺)) |
4 | | ax-resscn 10786 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
6 | | ftc1cnnc.g |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
7 | | ftc1cnnc.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
8 | | ftc1cnnc.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
9 | | ftc1cnnc.le |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
10 | | ssidd 3924 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
11 | | ioossre 12996 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
13 | | ftc1cnnc.i |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
14 | | ftc1cnnc.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
15 | | cncff 23790 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
17 | 6, 7, 8, 9, 10, 12, 13, 16 | ftc1lem2 24933 |
. . . . . 6
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
18 | | iccssre 13017 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
19 | 7, 8, 18 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
20 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
21 | 20 | tgioo2 23700 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
22 | 5, 17, 19, 21, 20 | dvbssntr 24797 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) |
23 | | iccntr 23718 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
24 | 7, 8, 23 | syl2anc 587 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
25 | 22, 24 | sseqtrd 3941 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆ (𝐴(,)𝐵)) |
26 | | retop 23659 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ Top |
27 | 21, 26 | eqeltrri 2835 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t ℝ)
∈ Top |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) →
((TopOpen‘ℂfld) ↾t ℝ) ∈
Top) |
29 | 19 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ) |
30 | | iooretop 23663 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
31 | 30, 21 | eleqtri 2836 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
33 | | ioossicc 13021 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
34 | 33 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
35 | | uniretop 23660 |
. . . . . . . . . 10
⊢ ℝ =
∪ (topGen‘ran (,)) |
36 | 21 | unieqi 4832 |
. . . . . . . . . 10
⊢ ∪ (topGen‘ran (,)) = ∪
((TopOpen‘ℂfld) ↾t
ℝ) |
37 | 35, 36 | eqtri 2765 |
. . . . . . . . 9
⊢ ℝ =
∪ ((TopOpen‘ℂfld)
↾t ℝ) |
38 | 37 | ssntr 21955 |
. . . . . . . 8
⊢
(((((TopOpen‘ℂfld) ↾t ℝ)
∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) ∧ ((𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t ℝ) ∧
(𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
39 | 28, 29, 32, 34, 38 | syl22anc 839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
40 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵)) |
41 | 39, 40 | sseldd 3902 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
42 | 16 | ffvelrnda 6904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
43 | | cnxmet 23670 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
44 | 11, 4 | sstri 3910 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ⊆ ℂ |
45 | | xmetres2 23259 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))) |
46 | 43, 44, 45 | mp2an 692 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) |
47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))) |
48 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
49 | | ssid 3923 |
. . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ |
50 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) |
51 | 20 | cnfldtopon 23680 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
52 | 51 | toponrestid 21818 |
. . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
53 | 20, 50, 52 | cncfcn 23807 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
54 | 44, 49, 53 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld)) |
55 | 14, 54 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
56 | | resttopon 22058 |
. . . . . . . . . . . . . . . . 17
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
57 | 51, 44, 56 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) |
58 | 57 | toponunii 21813 |
. . . . . . . . . . . . . . 15
⊢ (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
59 | 58 | eleq2i 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ (𝐴(,)𝐵) ↔ 𝑐 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
60 | 59 | biimpi 219 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
61 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
62 | 61 | cncnpi 22175 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
∧ 𝑐 ∈ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐)) |
63 | 55, 60, 62 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐)) |
64 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) = ((abs ∘ − ) ↾
((𝐴(,)𝐵) × (𝐴(,)𝐵))) |
65 | 20 | cnfldtopn 23679 |
. . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
66 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) = (MetOpen‘((abs ∘ −
) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) |
67 | 64, 65, 66 | metrest 23422 |
. . . . . . . . . . . . . . 15
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))))) |
68 | 43, 44, 67 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) |
69 | 68 | oveq1i 7223 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld)) = ((MetOpen‘((abs ∘ −
) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld)) |
70 | 69 | fveq1i 6718 |
. . . . . . . . . . . 12
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐) = (((MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐) |
71 | 63, 70 | eleqtrdi 2848 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐)) |
72 | 71 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝐹 ∈ (((MetOpen‘((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐)) |
73 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
74 | 66, 65 | metcnpi2 23443 |
. . . . . . . . . 10
⊢ (((((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) ∧ (abs ∘ − ) ∈
(∞Met‘ℂ)) ∧ (𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐) ∧ 𝑤 ∈ ℝ+)) →
∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤)) |
75 | 47, 48, 72, 73, 74 | syl22anc 839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤)) |
76 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑢 ∈ (𝐴(,)𝐵)) |
77 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵)) |
78 | 76, 77 | ovresd 7375 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (𝑢(abs ∘ − )𝑐)) |
79 | | elioore 12965 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℝ) |
80 | 79 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℂ) |
81 | 44 | sseli 3896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ) |
82 | 81 | ad3antlr 731 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ) |
83 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
84 | 83 | cnmetdval 23668 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢 − 𝑐))) |
85 | 80, 82, 84 | syl2an2 686 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢 − 𝑐))) |
86 | 78, 85 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (abs‘(𝑢 − 𝑐))) |
87 | 86 | breq1d 5063 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 ↔ (abs‘(𝑢 − 𝑐)) < 𝑣)) |
88 | 16 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ 𝐹:(𝐴(,)𝐵)⟶ℂ) |
89 | 88 | ffvelrnda 6904 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑢) ∈ ℂ) |
90 | 42 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
91 | 83 | cnmetdval 23668 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑢) ∈ ℂ ∧ (𝐹‘𝑐) ∈ ℂ) → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑐)))) |
92 | 89, 90, 91 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑐)))) |
93 | 92 | breq1d 5063 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤 ↔ (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) |
94 | 87, 93 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) ↔ ((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) |
95 | 94 | ralbidva 3117 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) ↔ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) |
96 | | simprll 779 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) |
97 | | eldifsni 4703 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ≠ 𝑐) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ≠ 𝑐) |
99 | 19 | ssdifssd 4057 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℝ) |
100 | 99 | sselda 3901 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → 𝑧 ∈ ℝ) |
101 | 100 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → 𝑧 ∈ ℝ) |
102 | 101 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ ℝ) |
103 | | elioore 12965 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℝ) |
104 | 103 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ ℝ) |
105 | 102, 104 | lttri2d 10971 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (𝑧 ≠ 𝑐 ↔ (𝑧 < 𝑐 ∨ 𝑐 < 𝑧))) |
106 | 105 | biimpa 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 ≠ 𝑐) → (𝑧 < 𝑐 ∨ 𝑐 < 𝑧)) |
107 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 = 𝑧 → (𝐺‘𝑠) = (𝐺‘𝑧)) |
108 | 107 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑠 = 𝑧 → ((𝐺‘𝑠) − (𝐺‘𝑐)) = ((𝐺‘𝑧) − (𝐺‘𝑐))) |
109 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑠 = 𝑧 → (𝑠 − 𝑐) = (𝑧 − 𝑐)) |
110 | 108, 109 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 = 𝑧 → (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
111 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) = (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) |
112 | | ovex 7246 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) ∈ V |
113 | 110, 111,
112 | fvmpt 6818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
114 | 113 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
115 | 114 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
116 | 17 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
117 | | eldifi 4041 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ∈ (𝐴[,]𝐵)) |
118 | 117 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → 𝑧 ∈ (𝐴[,]𝐵)) |
119 | 118 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ (𝐴[,]𝐵)) |
120 | 116, 119 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺‘𝑧) ∈ ℂ) |
121 | 33 | sseli 3896 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ (𝐴[,]𝐵)) |
122 | 17 | ffvelrnda 6904 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑐) ∈ ℂ) |
123 | 121, 122 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑐) ∈ ℂ) |
124 | 123 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺‘𝑐) ∈ ℂ) |
125 | 102 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℝ) |
126 | 125 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℂ) |
127 | 81 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑐 ∈ ℂ) |
128 | | ltne 10929 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑐 ≠ 𝑧) |
129 | 128 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑧 ≠ 𝑐) |
130 | 102, 129 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ≠ 𝑐) |
131 | 120, 124,
126, 127, 130 | div2subd 11658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) = (((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧))) |
132 | 115, 131 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧))) |
133 | 132 | fvoveq1d 7235 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐)))) |
134 | 7 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐴 ∈ ℝ) |
135 | 8 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐵 ∈ ℝ) |
136 | 9 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐴 ≤ 𝐵) |
137 | 14 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
138 | 13 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐹 ∈
𝐿1) |
139 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴(,)𝐵)) |
140 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑤 ∈ ℝ+) |
141 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑣 ∈ ℝ+) |
142 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) |
143 | | fvoveq1 7236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑦 → (abs‘(𝑢 − 𝑐)) = (abs‘(𝑦 − 𝑐))) |
144 | 143 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑦 → ((abs‘(𝑢 − 𝑐)) < 𝑣 ↔ (abs‘(𝑦 − 𝑐)) < 𝑣)) |
145 | 144 | imbrov2fvoveq 7238 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑦 → (((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) ↔ ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤))) |
146 | 145 | rspccva 3536 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑢 ∈
(𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
147 | 142, 146 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
148 | 96, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ (𝐴[,]𝐵)) |
149 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑧 − 𝑐)) < 𝑣) |
150 | 121 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴[,]𝐵)) |
151 | 103 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ) |
152 | 151 | subidd 11177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈ (𝐴(,)𝐵) → (𝑐 − 𝑐) = 0) |
153 | 152 | abs00bd 14855 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ (𝐴(,)𝐵) → (abs‘(𝑐 − 𝑐)) = 0) |
154 | 153 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑐 − 𝑐)) = 0) |
155 | 141 | rpgt0d 12631 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 0 < 𝑣) |
156 | 154, 155 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑐 − 𝑐)) < 𝑣) |
157 | 6, 134, 135, 136, 137, 138, 139, 111, 140, 141, 147, 148, 149, 150, 156 | ftc1cnnclem 35585 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐))) < 𝑤) |
158 | 133, 157 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
159 | 113 | fvoveq1d 7235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
160 | 159 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
161 | 160 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
162 | 6, 134, 135, 136, 137, 138, 139, 111, 140, 141, 147, 150, 156, 148, 149 | ftc1cnnclem 35585 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐))) < 𝑤) |
163 | 161, 162 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
164 | 158, 163 | jaodan 958 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ (𝑧 < 𝑐 ∨ 𝑐 < 𝑧)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
165 | 106, 164 | syldan 594 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 ≠ 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
166 | 98, 165 | mpdan 687 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
167 | 166 | expr 460 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → ((abs‘(𝑧 − 𝑐)) < 𝑣 → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
168 | 167 | adantld 494 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → ((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
169 | 168 | expr 460 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) → ((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
170 | 169 | ralrimdva 3110 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
171 | 95, 170 | sylbid 243 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
172 | 171 | anassrs 471 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) ∧ 𝑣 ∈ ℝ+)
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
173 | 172 | reximdva 3193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
(∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∃𝑣 ∈ ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
174 | 75, 173 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
175 | 174 | ralrimiva 3105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ∀𝑤 ∈ ℝ+ ∃𝑣 ∈ ℝ+
∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
176 | 17 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
177 | 19, 4 | sstrdi 3913 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
178 | 177 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℂ) |
179 | 121 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴[,]𝐵)) |
180 | 176, 178,
179 | dvlem 24793 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)) ∈ ℂ) |
181 | 180 | fmpttd 6932 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))):((𝐴[,]𝐵) ∖ {𝑐})⟶ℂ) |
182 | 177 | ssdifssd 4057 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ) |
183 | 182 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ) |
184 | 81 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ) |
185 | 181, 183,
184 | ellimc3 24776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐) ↔ ((𝐹‘𝑐) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)))) |
186 | 42, 175, 185 | mpbir2and 713 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)) |
187 | | eqid 2737 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
ℝ) |
188 | 187, 20, 111, 5, 17, 19 | eldv 24795 |
. . . . . . 7
⊢ (𝜑 → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) ↔ (𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)))) |
189 | 188 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) ↔ (𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)))) |
190 | 41, 186, 189 | mpbir2and 713 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐(ℝ D 𝐺)(𝐹‘𝑐)) |
191 | | vex 3412 |
. . . . . 6
⊢ 𝑐 ∈ V |
192 | | fvex 6730 |
. . . . . 6
⊢ (𝐹‘𝑐) ∈ V |
193 | 191, 192 | breldm 5777 |
. . . . 5
⊢ (𝑐(ℝ D 𝐺)(𝐹‘𝑐) → 𝑐 ∈ dom (ℝ D 𝐺)) |
194 | 190, 193 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ dom (ℝ D 𝐺)) |
195 | 25, 194 | eqelssd 3922 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
196 | | df-fn 6383 |
. . 3
⊢ ((ℝ
D 𝐺) Fn (𝐴(,)𝐵) ↔ (Fun (ℝ D 𝐺) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵))) |
197 | 3, 195, 196 | sylanbrc 586 |
. 2
⊢ (𝜑 → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
198 | 16 | ffnd 6546 |
. 2
⊢ (𝜑 → 𝐹 Fn (𝐴(,)𝐵)) |
199 | 3 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → Fun (ℝ D 𝐺)) |
200 | | funbrfv 6763 |
. . 3
⊢ (Fun
(ℝ D 𝐺) → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) → ((ℝ D 𝐺)‘𝑐) = (𝐹‘𝑐))) |
201 | 199, 190,
200 | sylc 65 |
. 2
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑐) = (𝐹‘𝑐)) |
202 | 197, 198,
201 | eqfnfvd 6855 |
1
⊢ (𝜑 → (ℝ D 𝐺) = 𝐹) |