Step | Hyp | Ref
| Expression |
1 | | dvf 23477 |
. . . . 5
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ) |
3 | | ffun 5961 |
. . . 4
⊢ ((ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ → Fun
(ℝ D 𝐺)) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → Fun (ℝ D 𝐺)) |
5 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
7 | | ftc1cnnc.g |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
8 | | ftc1cnnc.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | | ftc1cnnc.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
10 | | ftc1cnnc.le |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
11 | | ssid 3587 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵) |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
13 | | ioossre 12106 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
15 | | ftc1cnnc.i |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
16 | | ftc1cnnc.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
17 | | cncff 22504 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
19 | 7, 8, 9, 10, 12, 14, 15, 18 | ftc1lem2 23603 |
. . . . . 6
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
20 | | iccssre 12126 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
21 | 8, 9, 20 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
22 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
23 | 22 | tgioo2 22414 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
24 | 6, 19, 21, 23, 22 | dvbssntr 23470 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) |
25 | | iccntr 22432 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
26 | 8, 9, 25 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
27 | 24, 26 | sseqtrd 3604 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆ (𝐴(,)𝐵)) |
28 | | retop 22375 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ Top |
29 | 23, 28 | eqeltrri 2685 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ↾t ℝ)
∈ Top |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) →
((TopOpen‘ℂfld) ↾t ℝ) ∈
Top) |
31 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ) |
32 | | iooretop 22379 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
33 | 32, 23 | eleqtri 2686 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
35 | | ioossicc 12130 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
36 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
37 | | uniretop 22376 |
. . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) |
38 | 23 | unieqi 4381 |
. . . . . . . . . . . 12
⊢ ∪ (topGen‘ran (,)) = ∪
((TopOpen‘ℂfld) ↾t
ℝ) |
39 | 37, 38 | eqtri 2632 |
. . . . . . . . . . 11
⊢ ℝ =
∪ ((TopOpen‘ℂfld)
↾t ℝ) |
40 | 39 | ssntr 20672 |
. . . . . . . . . 10
⊢
(((((TopOpen‘ℂfld) ↾t ℝ)
∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) ∧ ((𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t ℝ) ∧
(𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
41 | 30, 31, 34, 36, 40 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
42 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵)) |
43 | 41, 42 | sseldd 3569 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
44 | 18 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
45 | | cnxmet 22386 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
46 | 13, 5 | sstri 3577 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ ℂ |
47 | | xmetres2 21976 |
. . . . . . . . . . . . . 14
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))) |
48 | 45, 46, 47 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) |
49 | 48 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))) |
50 | 45 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
51 | | ssid 3587 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
⊆ ℂ |
52 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) |
53 | 22 | cnfldtop 22397 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(TopOpen‘ℂfld) ∈ Top |
54 | 22 | cnfldtopon 22396 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
55 | 54 | toponunii 20547 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
56 | 55 | restid 15917 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
57 | 53, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
58 | 57 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
59 | 22, 52, 58 | cncfcn 22520 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
60 | 46, 51, 59 | mp2an 704 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld)) |
61 | 16, 60 | syl6eleq 2698 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
62 | | resttopon 20775 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
63 | 54, 46, 62 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) |
64 | 63 | toponunii 20547 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
65 | 64 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ (𝐴(,)𝐵) ↔ 𝑐 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
66 | 65 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
67 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
68 | 67 | cncnpi 20892 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
∧ 𝑐 ∈ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐)) |
69 | 61, 66, 68 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐)) |
70 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) = ((abs ∘ − ) ↾
((𝐴(,)𝐵) × (𝐴(,)𝐵))) |
71 | 22 | cnfldtopn 22395 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
72 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) = (MetOpen‘((abs ∘ −
) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) |
73 | 70, 71, 72 | metrest 22139 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))))) |
74 | 45, 46, 73 | mp2an 704 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) |
75 | 74 | oveq1i 6559 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld)) = ((MetOpen‘((abs ∘ −
) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld)) |
76 | 75 | fveq1i 6104 |
. . . . . . . . . . . . . 14
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐) = (((MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐) |
77 | 69, 76 | syl6eleq 2698 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐)) |
78 | 77 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝐹 ∈ (((MetOpen‘((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐)) |
79 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
80 | 72, 71 | metcnpi2 22160 |
. . . . . . . . . . . 12
⊢ (((((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) ∧ (abs ∘ − ) ∈
(∞Met‘ℂ)) ∧ (𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐) ∧ 𝑤 ∈ ℝ+)) →
∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤)) |
81 | 49, 50, 78, 79, 80 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤)) |
82 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑢 ∈ (𝐴(,)𝐵)) |
83 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵)) |
84 | 82, 83 | ovresd 6699 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (𝑢(abs ∘ − )𝑐)) |
85 | | elioore 12076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℝ) |
86 | 85 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℂ) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑢 ∈ ℂ) |
88 | 46 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ) |
89 | 88 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ) |
90 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (abs
∘ − ) = (abs ∘ − ) |
91 | 90 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢 − 𝑐))) |
92 | 87, 89, 91 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢 − 𝑐))) |
93 | 84, 92 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (abs‘(𝑢 − 𝑐))) |
94 | 93 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 ↔ (abs‘(𝑢 − 𝑐)) < 𝑣)) |
95 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ 𝐹:(𝐴(,)𝐵)⟶ℂ) |
96 | 95 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑢) ∈ ℂ) |
97 | 44 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
98 | 90 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑢) ∈ ℂ ∧ (𝐹‘𝑐) ∈ ℂ) → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑐)))) |
99 | 96, 97, 98 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑐)))) |
100 | 99 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤 ↔ (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) |
101 | 94, 100 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) ↔ ((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) |
102 | 101 | ralbidva 2968 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) ↔ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) |
103 | | simprll 798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) |
104 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ≠ 𝑐) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ≠ 𝑐) |
106 | 21 | ssdifssd 3710 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℝ) |
107 | 106 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → 𝑧 ∈ ℝ) |
108 | 107 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → 𝑧 ∈ ℝ) |
109 | 108 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ ℝ) |
110 | | elioore 12076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℝ) |
111 | 110 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ ℝ) |
112 | 109, 111 | lttri2d 10055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (𝑧 ≠ 𝑐 ↔ (𝑧 < 𝑐 ∨ 𝑐 < 𝑧))) |
113 | 112 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 ≠ 𝑐) → (𝑧 < 𝑐 ∨ 𝑐 < 𝑧)) |
114 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑠 = 𝑧 → (𝐺‘𝑠) = (𝐺‘𝑧)) |
115 | 114 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 = 𝑧 → ((𝐺‘𝑠) − (𝐺‘𝑐)) = ((𝐺‘𝑧) − (𝐺‘𝑐))) |
116 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 = 𝑧 → (𝑠 − 𝑐) = (𝑧 − 𝑐)) |
117 | 115, 116 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 𝑧 → (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
118 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) = (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) |
119 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) ∈ V |
120 | 117, 118,
119 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
121 | 120 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
122 | 121 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
123 | 19 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
124 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ∈ (𝐴[,]𝐵)) |
125 | 124 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → 𝑧 ∈ (𝐴[,]𝐵)) |
126 | 125 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ (𝐴[,]𝐵)) |
127 | 123, 126 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺‘𝑧) ∈ ℂ) |
128 | 35 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ (𝐴[,]𝐵)) |
129 | 19 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑐) ∈ ℂ) |
130 | 128, 129 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑐) ∈ ℂ) |
131 | 130 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺‘𝑐) ∈ ℂ) |
132 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℝ) |
133 | 132 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℂ) |
134 | 88 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑐 ∈ ℂ) |
135 | | ltne 10013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑐 ≠ 𝑧) |
136 | 135 | necomd 2837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑧 ≠ 𝑐) |
137 | 109, 136 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ≠ 𝑐) |
138 | 127, 131,
133, 134, 137 | div2subd 10730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) = (((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧))) |
139 | 122, 138 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧))) |
140 | 139 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐)) = ((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐))) |
141 | 140 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐)))) |
142 | 8 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐴 ∈ ℝ) |
143 | 9 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐵 ∈ ℝ) |
144 | 10 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐴 ≤ 𝐵) |
145 | 16 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
146 | 15 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐹 ∈
𝐿1) |
147 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴(,)𝐵)) |
148 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑤 ∈ ℝ+) |
149 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑣 ∈ ℝ+) |
150 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) |
151 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = 𝑦 → (𝑢 − 𝑐) = (𝑦 − 𝑐)) |
152 | 151 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝑦 → (abs‘(𝑢 − 𝑐)) = (abs‘(𝑦 − 𝑐))) |
153 | 152 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝑦 → ((abs‘(𝑢 − 𝑐)) < 𝑣 ↔ (abs‘(𝑦 − 𝑐)) < 𝑣)) |
154 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = 𝑦 → (𝐹‘𝑢) = (𝐹‘𝑦)) |
155 | 154 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = 𝑦 → ((𝐹‘𝑢) − (𝐹‘𝑐)) = ((𝐹‘𝑦) − (𝐹‘𝑐))) |
156 | 155 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝑦 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑐)))) |
157 | 156 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝑦 → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
158 | 153, 157 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑦 → (((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) ↔ ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤))) |
159 | 158 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((∀𝑢 ∈
(𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
160 | 150, 159 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
161 | 103, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ (𝐴[,]𝐵)) |
162 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑧 − 𝑐)) < 𝑣) |
163 | 128 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴[,]𝐵)) |
164 | 110 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ) |
165 | 164 | subidd 10259 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ (𝐴(,)𝐵) → (𝑐 − 𝑐) = 0) |
166 | 165 | abs00bd 13879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 ∈ (𝐴(,)𝐵) → (abs‘(𝑐 − 𝑐)) = 0) |
167 | 166 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑐 − 𝑐)) = 0) |
168 | 149 | rpgt0d 11751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 0 < 𝑣) |
169 | 167, 168 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑐 − 𝑐)) < 𝑣) |
170 | 7, 142, 143, 144, 145, 146, 147, 118, 148, 149, 160, 161, 162, 163, 169 | ftc1cnnclem 32653 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐))) < 𝑤) |
171 | 141, 170 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
172 | 120 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → (((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐)) = ((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐))) |
173 | 172 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
174 | 173 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
175 | 174 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
176 | 7, 142, 143, 144, 145, 146, 147, 118, 148, 149, 160, 163, 169, 161, 162 | ftc1cnnclem 32653 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐))) < 𝑤) |
177 | 175, 176 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
178 | 171, 177 | jaodan 822 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ (𝑧 < 𝑐 ∨ 𝑐 < 𝑧)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
179 | 113, 178 | syldan 486 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 ≠ 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
180 | 105, 179 | mpdan 699 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
181 | 180 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → ((abs‘(𝑧 − 𝑐)) < 𝑣 → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
182 | 181 | adantld 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → ((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
183 | 182 | expr 641 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) → ((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
184 | 183 | ralrimdva 2952 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
185 | 102, 184 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
186 | 185 | anassrs 678 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) ∧ 𝑣 ∈ ℝ+)
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
187 | 186 | reximdva 3000 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
(∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∃𝑣 ∈ ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
188 | 81, 187 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
189 | 188 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ∀𝑤 ∈ ℝ+ ∃𝑣 ∈ ℝ+
∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
190 | 19 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
191 | 21, 5 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
192 | 191 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℂ) |
193 | 128 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴[,]𝐵)) |
194 | 190, 192,
193 | dvlem 23466 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)) ∈ ℂ) |
195 | 194, 118 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))):((𝐴[,]𝐵) ∖ {𝑐})⟶ℂ) |
196 | 191 | ssdifssd 3710 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ) |
197 | 196 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ) |
198 | 88 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ) |
199 | 195, 197,
198 | ellimc3 23449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐) ↔ ((𝐹‘𝑐) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)))) |
200 | 44, 189, 199 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)) |
201 | | eqid 2610 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
ℝ) |
202 | 201, 22, 118, 6, 19, 21 | eldv 23468 |
. . . . . . . . 9
⊢ (𝜑 → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) ↔ (𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)))) |
203 | 202 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) ↔ (𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)))) |
204 | 43, 200, 203 | mpbir2and 959 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐(ℝ D 𝐺)(𝐹‘𝑐)) |
205 | | vex 3176 |
. . . . . . . 8
⊢ 𝑐 ∈ V |
206 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘𝑐) ∈ V |
207 | 205, 206 | breldm 5251 |
. . . . . . 7
⊢ (𝑐(ℝ D 𝐺)(𝐹‘𝑐) → 𝑐 ∈ dom (ℝ D 𝐺)) |
208 | 204, 207 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ dom (ℝ D 𝐺)) |
209 | 208 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ dom (ℝ D 𝐺))) |
210 | 209 | ssrdv 3574 |
. . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ dom (ℝ D 𝐺)) |
211 | 27, 210 | eqssd 3585 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
212 | | df-fn 5807 |
. . 3
⊢ ((ℝ
D 𝐺) Fn (𝐴(,)𝐵) ↔ (Fun (ℝ D 𝐺) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵))) |
213 | 4, 211, 212 | sylanbrc 695 |
. 2
⊢ (𝜑 → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
214 | | ffn 5958 |
. . 3
⊢ (𝐹:(𝐴(,)𝐵)⟶ℂ → 𝐹 Fn (𝐴(,)𝐵)) |
215 | 18, 214 | syl 17 |
. 2
⊢ (𝜑 → 𝐹 Fn (𝐴(,)𝐵)) |
216 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → Fun (ℝ D 𝐺)) |
217 | | funbrfv 6144 |
. . 3
⊢ (Fun
(ℝ D 𝐺) → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) → ((ℝ D 𝐺)‘𝑐) = (𝐹‘𝑐))) |
218 | 216, 204,
217 | sylc 63 |
. 2
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑐) = (𝐹‘𝑐)) |
219 | 213, 215,
218 | eqfnfvd 6222 |
1
⊢ (𝜑 → (ℝ D 𝐺) = 𝐹) |