Step | Hyp | Ref
| Expression |
1 | | dvf 23671 |
. . . . 5
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ) |
3 | | ffun 6048 |
. . . 4
⊢ ((ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ → Fun
(ℝ D 𝐺)) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → Fun (ℝ D 𝐺)) |
5 | | ax-resscn 9993 |
. . . . . . 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 3624 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵) |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
13 | | ioossre 12235 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
15 | | ftc1cnnc.i |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
16 | | ftc1cnnc.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
17 | | cncff 22696 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
19 | 7, 8, 9, 10, 12, 14, 15, 18 | ftc1lem2 23799 |
. . . . . 6
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
20 | | iccssre 12255 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
21 | 8, 9, 20 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
22 | | eqid 2622 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
23 | 22 | tgioo2 22606 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
24 | 6, 19, 21, 23, 22 | dvbssntr 23664 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) |
25 | | iccntr 22624 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
26 | 8, 9, 25 | syl2anc 693 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
27 | 24, 26 | sseqtrd 3641 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐺) ⊆ (𝐴(,)𝐵)) |
28 | | retop 22565 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ Top |
29 | 23, 28 | eqeltrri 2698 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ↾t ℝ)
∈ Top |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) →
((TopOpen‘ℂfld) ↾t ℝ) ∈
Top) |
31 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ) |
32 | | iooretop 22569 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
33 | 32, 23 | eleqtri 2699 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
35 | | ioossicc 12259 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
36 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
37 | | uniretop 22566 |
. . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) |
38 | 23 | unieqi 4445 |
. . . . . . . . . . . 12
⊢ ∪ (topGen‘ran (,)) = ∪
((TopOpen‘ℂfld) ↾t
ℝ) |
39 | 37, 38 | eqtri 2644 |
. . . . . . . . . . 11
⊢ ℝ =
∪ ((TopOpen‘ℂfld)
↾t ℝ) |
40 | 39 | ssntr 20862 |
. . . . . . . . . 10
⊢
(((((TopOpen‘ℂfld) ↾t ℝ)
∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) ∧ ((𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t ℝ) ∧
(𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
41 | 30, 31, 34, 36, 40 | syl22anc 1327 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
42 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵)) |
43 | 41, 42 | sseldd 3604 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵))) |
44 | 18 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
45 | | cnxmet 22576 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
46 | 13, 5 | sstri 3612 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ ℂ |
47 | | xmetres2 22166 |
. . . . . . . . . . . . . 14
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))) |
48 | 45, 46, 47 | mp2an 708 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) |
49 | 48 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))) |
50 | 45 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
51 | | ssid 3624 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
⊆ ℂ |
52 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) |
53 | 22 | cnfldtop 22587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(TopOpen‘ℂfld) ∈ Top |
54 | 22 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
55 | 54 | toponunii 20721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
56 | 55 | restid 16094 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
57 | 53, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
58 | 57 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
59 | 22, 52, 58 | cncfcn 22712 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
60 | 46, 51, 59 | mp2an 708 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld)) |
61 | 16, 60 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
62 | | resttopon 20965 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
63 | 54, 46, 62 | mp2an 708 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) |
64 | 63 | toponunii 20721 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
65 | 64 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ (𝐴(,)𝐵) ↔ 𝑐 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
66 | 65 | biimpi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
67 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
68 | 67 | cncnpi 21082 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
∧ 𝑐 ∈ ∪ ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐)) |
69 | 61, 66, 68 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐)) |
70 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) = ((abs ∘ − ) ↾
((𝐴(,)𝐵) × (𝐴(,)𝐵))) |
71 | 22 | cnfldtopn 22585 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
72 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) = (MetOpen‘((abs ∘ −
) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) |
73 | 70, 71, 72 | metrest 22329 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))))) |
74 | 45, 46, 73 | mp2an 708 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) |
75 | 74 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld)) = ((MetOpen‘((abs ∘ −
) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld)) |
76 | 75 | fveq1i 6192 |
. . . . . . . . . . . . . 14
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑐) = (((MetOpen‘((abs ∘ − )
↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐) |
77 | 69, 76 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐)) |
78 | 77 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝐹 ∈ (((MetOpen‘((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐)) |
79 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
80 | 72, 71 | metcnpi2 22350 |
. . . . . . . . . . . 12
⊢ (((((abs
∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) ∧ (abs ∘ − ) ∈
(∞Met‘ℂ)) ∧ (𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP
(TopOpen‘ℂfld))‘𝑐) ∧ 𝑤 ∈ ℝ+)) →
∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤)) |
81 | 49, 50, 78, 79, 80 | syl22anc 1327 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤)) |
82 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑢 ∈ (𝐴(,)𝐵)) |
83 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵)) |
84 | 82, 83 | ovresd 6801 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (𝑢(abs ∘ − )𝑐)) |
85 | | elioore 12205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℝ) |
86 | 85 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℂ) |
87 | 86 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑢 ∈ ℂ) |
88 | 46 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ) |
89 | 88 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ) |
90 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (abs
∘ − ) = (abs ∘ − ) |
91 | 90 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢 − 𝑐))) |
92 | 87, 89, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢 − 𝑐))) |
93 | 84, 92 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (abs‘(𝑢 − 𝑐))) |
94 | 93 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 ↔ (abs‘(𝑢 − 𝑐)) < 𝑣)) |
95 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ 𝐹:(𝐴(,)𝐵)⟶ℂ) |
96 | 95 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑢) ∈ ℂ) |
97 | 44 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
98 | 90 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑢) ∈ ℂ ∧ (𝐹‘𝑐) ∈ ℂ) → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑐)))) |
99 | 96, 97, 98 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) = (abs‘((𝐹‘𝑢) − (𝐹‘𝑐)))) |
100 | 99 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤 ↔ (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) |
101 | 94, 100 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) ↔ ((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) |
102 | 101 | ralbidva 2985 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) ↔ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) |
103 | | simprll 802 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) |
104 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ≠ 𝑐) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ≠ 𝑐) |
106 | 21 | ssdifssd 3748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℝ) |
107 | 106 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → 𝑧 ∈ ℝ) |
108 | 107 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → 𝑧 ∈ ℝ) |
109 | 108 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ ℝ) |
110 | | elioore 12205 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℝ) |
111 | 110 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ ℝ) |
112 | 109, 111 | lttri2d 10176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (𝑧 ≠ 𝑐 ↔ (𝑧 < 𝑐 ∨ 𝑐 < 𝑧))) |
113 | 112 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 ≠ 𝑐) → (𝑧 < 𝑐 ∨ 𝑐 < 𝑧)) |
114 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑠 = 𝑧 → (𝐺‘𝑠) = (𝐺‘𝑧)) |
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 = 𝑧 → ((𝐺‘𝑠) − (𝐺‘𝑐)) = ((𝐺‘𝑧) − (𝐺‘𝑐))) |
116 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 = 𝑧 → (𝑠 − 𝑐) = (𝑧 − 𝑐)) |
117 | 115, 116 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 𝑧 → (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
118 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) = (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) |
119 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) ∈ V |
120 | 117, 118,
119 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
121 | 120 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
122 | 121 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) |
123 | 19 | ad4antr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
124 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ∈ (𝐴[,]𝐵)) |
125 | 124 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → 𝑧 ∈ (𝐴[,]𝐵)) |
126 | 125 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ (𝐴[,]𝐵)) |
127 | 123, 126 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺‘𝑧) ∈ ℂ) |
128 | 35 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ (𝐴[,]𝐵)) |
129 | 19 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑐) ∈ ℂ) |
130 | 128, 129 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑐) ∈ ℂ) |
131 | 130 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺‘𝑐) ∈ ℂ) |
132 | 109 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℝ) |
133 | 132 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℂ) |
134 | 88 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑐 ∈ ℂ) |
135 | | ltne 10134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑐 ≠ 𝑧) |
136 | 135 | necomd 2849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑧 ≠ 𝑐) |
137 | 109, 136 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ≠ 𝑐) |
138 | 127, 131,
133, 134, 137 | div2subd 10851 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) = (((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧))) |
139 | 122, 138 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) = (((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧))) |
140 | 139 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐)) = ((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐))) |
141 | 140 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐)))) |
142 | 8 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐴 ∈ ℝ) |
143 | 9 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐵 ∈ ℝ) |
144 | 10 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐴 ≤ 𝐵) |
145 | 16 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
146 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝐹 ∈
𝐿1) |
147 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴(,)𝐵)) |
148 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑤 ∈ ℝ+) |
149 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑣 ∈ ℝ+) |
150 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) |
151 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = 𝑦 → (𝑢 − 𝑐) = (𝑦 − 𝑐)) |
152 | 151 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝑦 → (abs‘(𝑢 − 𝑐)) = (abs‘(𝑦 − 𝑐))) |
153 | 152 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝑦 → ((abs‘(𝑢 − 𝑐)) < 𝑣 ↔ (abs‘(𝑦 − 𝑐)) < 𝑣)) |
154 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = 𝑦 → (𝐹‘𝑢) = (𝐹‘𝑦)) |
155 | 154 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = 𝑦 → ((𝐹‘𝑢) − (𝐹‘𝑐)) = ((𝐹‘𝑦) − (𝐹‘𝑐))) |
156 | 155 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝑦 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) = (abs‘((𝐹‘𝑦) − (𝐹‘𝑐)))) |
157 | 156 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝑦 → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
158 | 153, 157 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑦 → (((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) ↔ ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤))) |
159 | 158 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((∀𝑢 ∈
(𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
160 | 150, 159 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝑤)) |
161 | 103, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑧 ∈ (𝐴[,]𝐵)) |
162 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑧 − 𝑐)) < 𝑣) |
163 | 128 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴[,]𝐵)) |
164 | 110 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ) |
165 | 164 | subidd 10380 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ (𝐴(,)𝐵) → (𝑐 − 𝑐) = 0) |
166 | 165 | abs00bd 14031 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 ∈ (𝐴(,)𝐵) → (abs‘(𝑐 − 𝑐)) = 0) |
167 | 166 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑐 − 𝑐)) = 0) |
168 | 149 | rpgt0d 11875 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → 0 < 𝑣) |
169 | 167, 168 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(𝑐 − 𝑐)) < 𝑣) |
170 | 7, 142, 143, 144, 145, 146, 147, 118, 148, 149, 160, 161, 162, 163, 169 | ftc1cnnclem 33483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘((((𝐺‘𝑐) − (𝐺‘𝑧)) / (𝑐 − 𝑧)) − (𝐹‘𝑐))) < 𝑤) |
171 | 141, 170 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
172 | 120 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → (((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐)) = ((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐))) |
173 | 172 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
174 | 173 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
175 | 174 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) = (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐)))) |
176 | 7, 142, 143, 144, 145, 146, 147, 118, 148, 149, 160, 163, 169, 161, 162 | ftc1cnnclem 33483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘((((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐)) − (𝐹‘𝑐))) < 𝑤) |
177 | 175, 176 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
178 | 171, 177 | jaodan 826 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ (𝑧 < 𝑐 ∨ 𝑐 < 𝑧)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
179 | 113, 178 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) ∧ 𝑧 ≠ 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
180 | 105, 179 | mpdan 702 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤)) ∧ (abs‘(𝑧 − 𝑐)) < 𝑣)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤) |
181 | 180 | expr 643 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → ((abs‘(𝑧 − 𝑐)) < 𝑣 → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
182 | 181 | adantld 483 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤))) → ((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
183 | 182 | expr 643 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) → ((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
184 | 183 | ralrimdva 2969 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((abs‘(𝑢 − 𝑐)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑐))) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
185 | 102, 184 | sylbid 230 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
186 | 185 | anassrs 680 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) ∧ 𝑣 ∈ ℝ+)
→ (∀𝑢 ∈
(𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
187 | 186 | reximdva 3017 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
(∃𝑣 ∈
ℝ+ ∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹‘𝑢)(abs ∘ − )(𝐹‘𝑐)) < 𝑤) → ∃𝑣 ∈ ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤))) |
188 | 81, 187 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
189 | 188 | ralrimiva 2966 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ∀𝑤 ∈ ℝ+ ∃𝑣 ∈ ℝ+
∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)) |
190 | 19 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
191 | 21, 5 | syl6ss 3615 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
192 | 191 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℂ) |
193 | 128 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴[,]𝐵)) |
194 | 190, 192,
193 | dvlem 23660 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)) ∈ ℂ) |
195 | 194, 118 | fmptd 6385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))):((𝐴[,]𝐵) ∖ {𝑐})⟶ℂ) |
196 | 191 | ssdifssd 3748 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ) |
197 | 196 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ) |
198 | 88 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ) |
199 | 195, 197,
198 | ellimc3 23643 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐) ↔ ((𝐹‘𝑐) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧 ≠ 𝑐 ∧ (abs‘(𝑧 − 𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐)))‘𝑧) − (𝐹‘𝑐))) < 𝑤)))) |
200 | 44, 189, 199 | mpbir2and 957 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)) |
201 | | eqid 2622 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
ℝ) |
202 | 201, 22, 118, 6, 19, 21 | eldv 23662 |
. . . . . . . . 9
⊢ (𝜑 → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) ↔ (𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)))) |
203 | 202 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) ↔ (𝑐 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹‘𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑠) − (𝐺‘𝑐)) / (𝑠 − 𝑐))) limℂ 𝑐)))) |
204 | 43, 200, 203 | mpbir2and 957 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐(ℝ D 𝐺)(𝐹‘𝑐)) |
205 | | vex 3203 |
. . . . . . . 8
⊢ 𝑐 ∈ V |
206 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐹‘𝑐) ∈ V |
207 | 205, 206 | breldm 5329 |
. . . . . . 7
⊢ (𝑐(ℝ D 𝐺)(𝐹‘𝑐) → 𝑐 ∈ dom (ℝ D 𝐺)) |
208 | 204, 207 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ dom (ℝ D 𝐺)) |
209 | 208 | ex 450 |
. . . . 5
⊢ (𝜑 → (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ dom (ℝ D 𝐺))) |
210 | 209 | ssrdv 3609 |
. . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ dom (ℝ D 𝐺)) |
211 | 27, 210 | eqssd 3620 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
212 | | df-fn 5891 |
. . 3
⊢ ((ℝ
D 𝐺) Fn (𝐴(,)𝐵) ↔ (Fun (ℝ D 𝐺) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵))) |
213 | 4, 211, 212 | sylanbrc 698 |
. 2
⊢ (𝜑 → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
214 | | ffn 6045 |
. . 3
⊢ (𝐹:(𝐴(,)𝐵)⟶ℂ → 𝐹 Fn (𝐴(,)𝐵)) |
215 | 18, 214 | syl 17 |
. 2
⊢ (𝜑 → 𝐹 Fn (𝐴(,)𝐵)) |
216 | 4 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → Fun (ℝ D 𝐺)) |
217 | | funbrfv 6234 |
. . 3
⊢ (Fun
(ℝ D 𝐺) → (𝑐(ℝ D 𝐺)(𝐹‘𝑐) → ((ℝ D 𝐺)‘𝑐) = (𝐹‘𝑐))) |
218 | 216, 204,
217 | sylc 65 |
. 2
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑐) = (𝐹‘𝑐)) |
219 | 213, 215,
218 | eqfnfvd 6314 |
1
⊢ (𝜑 → (ℝ D 𝐺) = 𝐹) |