Step | Hyp | Ref
| Expression |
1 | | lhop1.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
2 | | lhop1.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
3 | | lhop1lem.db |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ≤ 𝐵) |
4 | | iooss2 12082 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐷 ≤ 𝐵) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵)) |
5 | 2, 3, 4 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵)) |
6 | | lhop1lem.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝐴(,)𝐷)) |
7 | 5, 6 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝐴(,)𝐵)) |
8 | 1, 7 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑋) ∈ ℝ) |
9 | 8 | recnd 9947 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑋) ∈ ℂ) |
10 | | lhop1.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
11 | 10, 7 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝑋) ∈ ℝ) |
12 | 11 | recnd 9947 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑋) ∈ ℂ) |
13 | | lhop1.gn0 |
. . . . . 6
⊢ (𝜑 → ¬ 0 ∈ ran 𝐺) |
14 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐺:(𝐴(,)𝐵)⟶ℝ → 𝐺 Fn (𝐴(,)𝐵)) |
15 | 10, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn (𝐴(,)𝐵)) |
16 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑋) ∈ ran 𝐺) |
17 | 15, 7, 16 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝑋) ∈ ran 𝐺) |
18 | | eleq1 2676 |
. . . . . . . 8
⊢ ((𝐺‘𝑋) = 0 → ((𝐺‘𝑋) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺)) |
19 | 17, 18 | syl5ibcom 234 |
. . . . . . 7
⊢ (𝜑 → ((𝐺‘𝑋) = 0 → 0 ∈ ran 𝐺)) |
20 | 19 | necon3bd 2796 |
. . . . . 6
⊢ (𝜑 → (¬ 0 ∈ ran 𝐺 → (𝐺‘𝑋) ≠ 0)) |
21 | 13, 20 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑋) ≠ 0) |
22 | 9, 12, 21 | divcld 10680 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ) |
23 | | limccl 23445 |
. . . . 5
⊢ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐴) ⊆ ℂ |
24 | | lhop1.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐴)) |
25 | 23, 24 | sseldi 3566 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
26 | 22, 25 | subcld 10271 |
. . 3
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶) ∈ ℂ) |
27 | 26 | abscld 14023 |
. 2
⊢ (𝜑 → (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ∈ ℝ) |
28 | | lhop1lem.e |
. . 3
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
29 | 28 | rpred 11748 |
. 2
⊢ (𝜑 → 𝐸 ∈ ℝ) |
30 | | 2re 10967 |
. . . 4
⊢ 2 ∈
ℝ |
31 | 30 | a1i 11 |
. . 3
⊢ (𝜑 → 2 ∈
ℝ) |
32 | 31, 29 | remulcld 9949 |
. 2
⊢ (𝜑 → (2 · 𝐸) ∈
ℝ) |
33 | | cnxmet 22386 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → (abs ∘ − )
∈ (∞Met‘ℂ)) |
35 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → 𝑣 ∈
(TopOpen‘ℂfld)) |
36 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → 𝐴 ∈ 𝑣) |
37 | | eliooord 12104 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (𝐴(,)𝐷) → (𝐴 < 𝑋 ∧ 𝑋 < 𝐷)) |
38 | 6, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 < 𝑋 ∧ 𝑋 < 𝐷)) |
39 | 38 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 < 𝑋) |
40 | | lhop1.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
41 | | ioossre 12106 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴(,)𝐷) ⊆ ℝ |
42 | 41, 6 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℝ) |
43 | | difrp 11744 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ (𝑋 − 𝐴) ∈
ℝ+)) |
44 | 40, 42, 43 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 < 𝑋 ↔ (𝑋 − 𝐴) ∈
ℝ+)) |
45 | 39, 44 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 − 𝐴) ∈
ℝ+) |
46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → (𝑋 − 𝐴) ∈
ℝ+) |
47 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
48 | 47 | cnfldtopn 22395 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
49 | 48 | mopni3 22109 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣) ∧ (𝑋 − 𝐴) ∈ ℝ+) →
∃𝑟 ∈
ℝ+ (𝑟 <
(𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣)) |
50 | 34, 35, 36, 46, 49 | syl31anc 1321 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑟 ∈ ℝ+
(𝑟 < (𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣)) |
51 | | lhop1lem.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑅 = (𝐴 + (𝑟 / 2)) |
52 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ∈ ℝ) |
53 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℝ+) |
54 | 53 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℝ) |
55 | 54 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈ ℝ) |
56 | 52, 55 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴 + (𝑟 / 2)) ∈ ℝ) |
57 | 51, 56 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ ℝ) |
58 | 57 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ ℂ) |
59 | 40 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ ℂ) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ∈ ℂ) |
61 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (abs
∘ − ) = (abs ∘ − ) |
62 | 61 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅 − 𝐴))) |
63 | 58, 60, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅 − 𝐴))) |
64 | 51 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 − 𝐴) = ((𝐴 + (𝑟 / 2)) − 𝐴) |
65 | 54 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℂ) |
66 | 65 | halfcld 11154 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈ ℂ) |
67 | 60, 66 | pncan2d 10273 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐴 + (𝑟 / 2)) − 𝐴) = (𝑟 / 2)) |
68 | 64, 67 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅 − 𝐴) = (𝑟 / 2)) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘(𝑅 − 𝐴)) = (abs‘(𝑟 / 2))) |
70 | 53 | rphalfcld 11760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈
ℝ+) |
71 | 70 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈ ℝ) |
72 | 70 | rpge0d 11752 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 0 ≤ (𝑟 / 2)) |
73 | 71, 72 | absidd 14009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘(𝑟 / 2)) = (𝑟 / 2)) |
74 | 63, 69, 73 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(abs ∘ − )𝐴) = (𝑟 / 2)) |
75 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
76 | 53, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) < 𝑟) |
77 | 74, 76 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(abs ∘ − )𝐴) < 𝑟) |
78 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
79 | 54 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℝ*) |
80 | | elbl3 22007 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟)) |
81 | 78, 79, 60, 58, 80 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟)) |
82 | 77, 81 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟)) |
83 | 52, 70 | ltaddrpd 11781 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 < (𝐴 + (𝑟 / 2))) |
84 | 83, 51 | syl6breqr 4625 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 < 𝑅) |
85 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 ∈ ℝ) |
86 | 85, 52 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑋 − 𝐴) ∈ ℝ) |
87 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 < (𝑋 − 𝐴)) |
88 | 71, 54, 86, 76, 87 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) < (𝑋 − 𝐴)) |
89 | 52, 71, 85 | ltaddsub2d 10507 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐴 + (𝑟 / 2)) < 𝑋 ↔ (𝑟 / 2) < (𝑋 − 𝐴))) |
90 | 88, 89 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴 + (𝑟 / 2)) < 𝑋) |
91 | 51, 90 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 < 𝑋) |
92 | 52 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ∈
ℝ*) |
93 | 42 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 ∈
ℝ*) |
95 | | elioo2 12087 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℝ*
∧ 𝑋 ∈
ℝ*) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅 ∧ 𝑅 < 𝑋))) |
96 | 92, 94, 95 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅 ∧ 𝑅 < 𝑋))) |
97 | 57, 84, 91, 96 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ (𝐴(,)𝑋)) |
98 | 82, 97 | elind 3760 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))) |
99 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹‘𝑋) ∈ ℂ) |
100 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
101 | | lhop1lem.d |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐷 ∈ ℝ) |
102 | 101 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
103 | 38 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑋 < 𝐷) |
104 | 42, 101, 103 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑋 ≤ 𝐷) |
105 | 93, 102, 2, 104, 3 | xrletrd 11869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑋 ≤ 𝐵) |
106 | | iooss2 12082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ ℝ*
∧ 𝑋 ≤ 𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) |
107 | 2, 105, 106 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) |
108 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) |
109 | 108, 97 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ (𝐴(,)𝐵)) |
110 | 100, 109 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹‘𝑅) ∈ ℝ) |
111 | 110 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹‘𝑅) ∈ ℂ) |
112 | 99, 111 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐹‘𝑋) − (𝐹‘𝑅)) ∈ ℂ) |
113 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺‘𝑋) ∈ ℂ) |
114 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
115 | 114, 109 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺‘𝑅) ∈ ℝ) |
116 | 115 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺‘𝑅) ∈ ℂ) |
117 | 113, 116 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ∈ ℂ) |
118 | | lhop1.gd0 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐺)) |
119 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
120 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐺‘𝑋) ∈ ℂ) |
121 | 107 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝐴(,)𝐵)) |
122 | 10 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℝ) |
123 | 121, 122 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐺‘𝑧) ∈ ℝ) |
124 | 123 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐺‘𝑧) ∈ ℂ) |
125 | 120, 124 | subeq0ad 10281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺‘𝑋) − (𝐺‘𝑧)) = 0 ↔ (𝐺‘𝑋) = (𝐺‘𝑧))) |
126 | | ioossre 12106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐴(,)𝐵) ⊆ ℝ |
127 | 126, 121 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ) |
128 | 127 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝑧 ∈ ℝ) |
129 | 42 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝑋 ∈ ℝ) |
130 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ (𝐴(,)𝑋) → (𝐴 < 𝑧 ∧ 𝑧 < 𝑋)) |
131 | 130 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐴 < 𝑧 ∧ 𝑧 < 𝑋)) |
132 | 131 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 < 𝑋) |
133 | 132 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝑧 < 𝑋) |
134 | 40 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
135 | 134 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 ∈
ℝ*) |
136 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝐵 ∈
ℝ*) |
137 | 131 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 < 𝑧) |
138 | 93, 102, 2, 103, 3 | xrltletrd 11868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 𝑋 < 𝐵) |
139 | 138 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 < 𝐵) |
140 | | iccssioo 12113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝑧 ∧ 𝑋 < 𝐵)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵)) |
141 | 135, 136,
137, 139, 140 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵)) |
142 | 141 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵)) |
143 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ℝ
⊆ ℂ |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ℝ ⊆
ℂ) |
145 | | fss 5969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
146 | 10, 143, 145 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
147 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
148 | | lhop1.ig |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
149 | | dvcn 23490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
150 | 144, 146,
147, 148, 149 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
151 | | cncffvrn 22509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((ℝ
⊆ ℂ ∧ 𝐺
∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ)) |
152 | 143, 150,
151 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ)) |
153 | 10, 152 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
154 | 153 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
155 | | rescncf 22508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑧[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ))) |
156 | 142, 154,
155 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ)) |
157 | 143 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ℝ ⊆
ℂ) |
158 | 146 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
159 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝐴(,)𝐵) ⊆ ℝ) |
160 | 142, 126 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧[,]𝑋) ⊆ ℝ) |
161 | 47 | tgioo2 22414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
162 | 47, 161 | dvres 23481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑧[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋)))) |
163 | 157, 158,
159, 160, 162 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋)))) |
164 | | iccntr 22432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋)) |
165 | 128, 129,
164 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋)) |
166 | 165 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋))) |
167 | 163, 166 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋))) |
168 | 167 | dmeqd 5248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋))) |
169 | | ioossicc 12130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧(,)𝑋) ⊆ (𝑧[,]𝑋) |
170 | 169, 142 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧(,)𝑋) ⊆ (𝐴(,)𝐵)) |
171 | 148 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
172 | 170, 171 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺)) |
173 | | ssdmres 5340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋)) |
174 | 172, 173 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋)) |
175 | 168, 174 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = (𝑧(,)𝑋)) |
176 | 127 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ*) |
177 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈
ℝ*) |
178 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ) |
179 | 127, 178,
132 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ≤ 𝑋) |
180 | | ubicc2 12160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑧
≤ 𝑋) → 𝑋 ∈ (𝑧[,]𝑋)) |
181 | 176, 177,
179, 180 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ (𝑧[,]𝑋)) |
182 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑋 ∈ (𝑧[,]𝑋) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺‘𝑋)) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺‘𝑋)) |
184 | | lbicc2 12159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑧
≤ 𝑋) → 𝑧 ∈ (𝑧[,]𝑋)) |
185 | 176, 177,
179, 184 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝑧[,]𝑋)) |
186 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ (𝑧[,]𝑋) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺‘𝑧)) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺‘𝑧)) |
188 | 183, 187 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) ↔ (𝐺‘𝑋) = (𝐺‘𝑧))) |
189 | 188 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧)) |
190 | 189 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋)) |
191 | 128, 129,
133, 156, 175, 190 | rolle 23557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0) |
192 | 167 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤)) |
193 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 ∈ (𝑧(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
194 | 192, 193 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
195 | | dvf 23477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
196 | 148 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ
D 𝐺):(𝐴(,)𝐵)⟶ℂ)) |
197 | 195, 196 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
198 | 197 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
199 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((ℝ
D 𝐺):(𝐴(,)𝐵)⟶ℂ → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
200 | 198, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
201 | 200 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
202 | 170 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵)) |
203 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((ℝ D 𝐺) Fn
(𝐴(,)𝐵) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺)) |
204 | 201, 202,
203 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺)) |
205 | 194, 204 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺)) |
206 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((ℝ D (𝐺
↾ (𝑧[,]𝑋)))‘𝑤) = 0 → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
207 | 205, 206 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
208 | 207 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
209 | 191, 208 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 0 ∈ ran (ℝ D 𝐺)) |
210 | 209 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) = (𝐺‘𝑧) → 0 ∈ ran (ℝ D 𝐺))) |
211 | 125, 210 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺‘𝑋) − (𝐺‘𝑧)) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
212 | 211 | necon3bd 2796 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0)) |
213 | 119, 212 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0) |
214 | 213 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0) |
215 | 214 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0) |
216 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑅 → (𝐺‘𝑧) = (𝐺‘𝑅)) |
217 | 216 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑅 → ((𝐺‘𝑋) − (𝐺‘𝑧)) = ((𝐺‘𝑋) − (𝐺‘𝑅))) |
218 | 217 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑅 → (((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0 ↔ ((𝐺‘𝑋) − (𝐺‘𝑅)) ≠ 0)) |
219 | 218 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ (𝐴(,)𝑋) → (∀𝑧 ∈ (𝐴(,)𝑋)((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0 → ((𝐺‘𝑋) − (𝐺‘𝑅)) ≠ 0)) |
220 | 97, 215, 219 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ≠ 0) |
221 | 112, 117,
220 | divcld 10680 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) ∈ ℂ) |
222 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐶 ∈ ℂ) |
223 | 221, 222 | subcld 10271 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶) ∈ ℂ) |
224 | 223 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ∈ ℝ) |
225 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐸 ∈ ℝ) |
226 | 102 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐷 ∈
ℝ*) |
227 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 < 𝐷) |
228 | | iccssioo 12113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) ∧ (𝐴 < 𝑅 ∧ 𝑋 < 𝐷)) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷)) |
229 | 92, 226, 84, 227, 228 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷)) |
230 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵)) |
231 | 229, 230 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐵)) |
232 | | fss 5969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
233 | 1, 143, 232 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
234 | | lhop1.if |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
235 | | dvcn 23490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
236 | 144, 233,
147, 234, 235 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
237 | | cncffvrn 22509 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
238 | 143, 236,
237 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
239 | 1, 238 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
240 | 239 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
241 | | rescncf 22508 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))) |
242 | 231, 240,
241 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)) |
243 | 153 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
244 | | rescncf 22508 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))) |
245 | 231, 243,
244 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)) |
246 | 143 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ℝ ⊆
ℂ) |
247 | 233 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
248 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝐵) ⊆ ℝ) |
249 | | iccssre 12126 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑅[,]𝑋) ⊆ ℝ) |
250 | 57, 85, 249 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅[,]𝑋) ⊆ ℝ) |
251 | 47, 161 | dvres 23481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
252 | 246, 247,
248, 250, 251 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
253 | | iccntr 22432 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋)) |
254 | 57, 85, 253 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋)) |
255 | 254 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋))) |
256 | 252, 255 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋))) |
257 | 256 | dmeqd 5248 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋))) |
258 | 52, 57, 84 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ≤ 𝑅) |
259 | | iooss1 12081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑅) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋)) |
260 | 92, 258, 259 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋)) |
261 | 104 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 ≤ 𝐷) |
262 | | iooss2 12082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐷 ∈ ℝ*
∧ 𝑋 ≤ 𝐷) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷)) |
263 | 226, 261,
262 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷)) |
264 | 260, 263 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐷)) |
265 | 264, 230 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐵)) |
266 | 234 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
267 | 265, 266 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹)) |
268 | | ssdmres 5340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
269 | 267, 268 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
270 | 257, 269 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋)) |
271 | 146 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
272 | 47, 161 | dvres 23481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
273 | 246, 271,
248, 250, 272 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
274 | 254 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋))) |
275 | 273, 274 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋))) |
276 | 275 | dmeqd 5248 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋))) |
277 | 148 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
278 | 265, 277 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺)) |
279 | | ssdmres 5340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
280 | 278, 279 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
281 | 276, 280 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋)) |
282 | 57, 85, 91, 242, 245, 270, 281 | cmvth 23558 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤))) |
283 | 57 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈
ℝ*) |
284 | 283 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈
ℝ*) |
285 | 93 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈
ℝ*) |
286 | 57, 85, 91 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ≤ 𝑋) |
287 | 286 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ≤ 𝑋) |
288 | | ubicc2 12160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑅
≤ 𝑋) → 𝑋 ∈ (𝑅[,]𝑋)) |
289 | 284, 285,
287, 288 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ (𝑅[,]𝑋)) |
290 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑋 ∈ (𝑅[,]𝑋) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹‘𝑋)) |
291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹‘𝑋)) |
292 | | lbicc2 12159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑅
≤ 𝑋) → 𝑅 ∈ (𝑅[,]𝑋)) |
293 | 284, 285,
287, 292 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ (𝑅[,]𝑋)) |
294 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑅 ∈ (𝑅[,]𝑋) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹‘𝑅)) |
295 | 293, 294 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹‘𝑅)) |
296 | 291, 295 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐹‘𝑋) − (𝐹‘𝑅))) |
297 | 275 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤)) |
298 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
299 | 297, 298 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
300 | 296, 299 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐹‘𝑋) − (𝐹‘𝑅)) · ((ℝ D 𝐺)‘𝑤))) |
301 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑋 ∈ (𝑅[,]𝑋) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺‘𝑋)) |
302 | 289, 301 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺‘𝑋)) |
303 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑅 ∈ (𝑅[,]𝑋) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺‘𝑅)) |
304 | 293, 303 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺‘𝑅)) |
305 | 302, 304 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐺‘𝑋) − (𝐺‘𝑅))) |
306 | 256 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤)) |
307 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐹)‘𝑤)) |
308 | 306, 307 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐹)‘𝑤)) |
309 | 305, 308 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐺‘𝑋) − (𝐺‘𝑅)) · ((ℝ D 𝐹)‘𝑤))) |
310 | 117 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ∈ ℂ) |
311 | | dvf 23477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
312 | 234 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℂ)) |
313 | 311, 312 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
314 | 313 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
315 | 265 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵)) |
316 | 314, 315 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ) |
317 | 310, 316 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺‘𝑋) − (𝐺‘𝑅)) · ((ℝ D 𝐹)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅)))) |
318 | 309, 317 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅)))) |
319 | 300, 318 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹‘𝑋) − (𝐹‘𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅))))) |
320 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹‘𝑋) − (𝐹‘𝑅)) ∈ ℂ) |
321 | 197 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
322 | 321, 315 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ℂ) |
323 | 220 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ≠ 0) |
324 | 118 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
325 | 321, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
326 | 325, 315,
203 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺)) |
327 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((ℝ D 𝐺)‘𝑤) = 0 → (((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
328 | 326, 327 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((ℝ D 𝐺)‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
329 | 328 | necon3bd 2796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((ℝ D 𝐺)‘𝑤) ≠ 0)) |
330 | 324, 329 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ≠ 0) |
331 | 320, 310,
316, 322, 323, 330 | divmuleqd 10726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) ↔ (((𝐹‘𝑋) − (𝐹‘𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅))))) |
332 | 319, 331 | bitr4d 270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))) |
333 | 332 | rexbidva 3031 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))) |
334 | 282, 333 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))) |
335 | 264 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐷)) |
336 | | lhop1lem.t |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸) |
337 | 336 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸) |
338 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑤 → ((ℝ D 𝐹)‘𝑡) = ((ℝ D 𝐹)‘𝑤)) |
339 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑤 → ((ℝ D 𝐺)‘𝑡) = ((ℝ D 𝐺)‘𝑤)) |
340 | 338, 339 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑤 → (((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))) |
341 | 340 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑤 → ((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶) = ((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) |
342 | 341 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑤 → (abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶))) |
343 | 342 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑤 → ((abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)) |
344 | 343 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ (𝐴(,)𝐷) → (∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)) |
345 | 335, 337,
344 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸) |
346 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶) = ((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) |
347 | 346 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶))) |
348 | 347 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)) |
349 | 345, 348 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸)) |
350 | 349 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸)) |
351 | 334, 350 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸) |
352 | 224, 225,
351 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ≤ 𝐸) |
353 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑅 → (𝐹‘𝑢) = (𝐹‘𝑅)) |
354 | 353 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑅 → ((𝐹‘𝑋) − (𝐹‘𝑢)) = ((𝐹‘𝑋) − (𝐹‘𝑅))) |
355 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑅 → (𝐺‘𝑢) = (𝐺‘𝑅)) |
356 | 355 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑅 → ((𝐺‘𝑋) − (𝐺‘𝑢)) = ((𝐺‘𝑋) − (𝐺‘𝑅))) |
357 | 354, 356 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑅 → (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) = (((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅)))) |
358 | 357 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑅 → ((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶) = ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) |
359 | 358 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑅 → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) = (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶))) |
360 | 359 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑅 → ((abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ≤ 𝐸)) |
361 | 360 | rspcev 3282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ∧ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ≤ 𝐸) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
362 | 98, 352, 361 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
363 | 362 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
364 | | ssrin 3800 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴(ball‘(abs ∘ −
))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ (𝐴(,)𝑋))) |
365 | | lbioo 12077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ¬
𝐴 ∈ (𝐴(,)𝑋) |
366 | | disjsn 4192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝑋)) |
367 | 365, 366 | mpbir 220 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴(,)𝑋) ∩ {𝐴}) = ∅ |
368 | | disj3 3973 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴})) |
369 | 367, 368 | mpbi 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴}) |
370 | 369 | ineq2i 3773 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∩ (𝐴(,)𝑋)) = (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) |
371 | 364, 370 | syl6sseq 3614 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴(ball‘(abs ∘ −
))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) |
372 | | ssrexv 3630 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴(ball‘(abs ∘ −
))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
373 | 371, 372 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴(ball‘(abs ∘ −
))𝑟) ⊆ 𝑣 → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
374 | 363, 373 | syl5com 31 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
375 | 374 | anassrs 678 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < (𝑋 − 𝐴)) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
376 | 375 | expimpd 627 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 < (𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
377 | 376 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → (∃𝑟 ∈ ℝ+
(𝑟 < (𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
378 | 50, 377 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
379 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ ((𝐴(,)𝑋) ∖ {𝐴}) |
380 | | difss 3699 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝑋) ∖ {𝐴}) ⊆ (𝐴(,)𝑋) |
381 | 379, 380 | sstri 3577 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋) |
382 | 381 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → 𝑢 ∈ (𝐴(,)𝑋)) |
383 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑢 → (𝐹‘𝑧) = (𝐹‘𝑢)) |
384 | 383 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑢 → ((𝐹‘𝑋) − (𝐹‘𝑧)) = ((𝐹‘𝑋) − (𝐹‘𝑢))) |
385 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑢 → (𝐺‘𝑧) = (𝐺‘𝑢)) |
386 | 385 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑢 → ((𝐺‘𝑋) − (𝐺‘𝑧)) = ((𝐺‘𝑋) − (𝐺‘𝑢))) |
387 | 384, 386 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑢 → (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))) = (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢)))) |
388 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) |
389 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) ∈ V |
390 | 387, 388,
389 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (𝐴(,)𝑋) → ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) = (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢)))) |
391 | 390 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (𝐴(,)𝑋) → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶) = ((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) |
392 | 391 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (𝐴(,)𝑋) → (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) = (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶))) |
393 | 392 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝐴(,)𝑋) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
394 | 382, 393 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
395 | 394 | rexbiia 3022 |
. . . . . . . . . 10
⊢
(∃𝑢 ∈
(𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
396 | 378, 395 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸) |
397 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))) ∈ V |
398 | 397, 388 | fnmpti 5935 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) Fn (𝐴(,)𝑋) |
399 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) → (𝑥 − 𝐶) = (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) |
400 | 399 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) → (abs‘(𝑥 − 𝐶)) = (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶))) |
401 | 400 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) → ((abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)) |
402 | 401 | rexima 6401 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) Fn (𝐴(,)𝑋) ∧ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)) → (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)) |
403 | 398, 381,
402 | mp2an 704 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸) |
404 | 396, 403 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
405 | | dfrex2 2979 |
. . . . . . . 8
⊢
(∃𝑥 ∈
((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
406 | 404, 405 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
407 | | ssrab 3643 |
. . . . . . . 8
⊢ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ↔ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ ℂ ∧ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸)) |
408 | 407 | simprbi 479 |
. . . . . . 7
⊢ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
409 | 406, 408 | nsyl 134 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) |
410 | 409 | expr 641 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈
(TopOpen‘ℂfld)) → (𝐴 ∈ 𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
411 | 410 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
412 | | ralinexa 2980 |
. . . 4
⊢
(∀𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) ↔ ¬ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
413 | 411, 412 | sylib 207 |
. . 3
⊢ (𝜑 → ¬ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
414 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = ((𝐹‘𝑋) / (𝐺‘𝑋)) → (𝑥 − 𝐶) = (((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) |
415 | 414 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = ((𝐹‘𝑋) / (𝐺‘𝑋)) → (abs‘(𝑥 − 𝐶)) = (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶))) |
416 | 415 | breq1d 4593 |
. . . . . . 7
⊢ (𝑥 = ((𝐹‘𝑋) / (𝐺‘𝑋)) → ((abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
417 | 416 | notbid 307 |
. . . . . 6
⊢ (𝑥 = ((𝐹‘𝑋) / (𝐺‘𝑋)) → (¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
418 | 417 | elrab3 3332 |
. . . . 5
⊢ (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
419 | 22, 418 | syl 17 |
. . . 4
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
420 | | notrab 3863 |
. . . . . 6
⊢ (ℂ
∖ {𝑥 ∈ ℂ
∣ (abs‘(𝑥
− 𝐶)) ≤ 𝐸}) = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} |
421 | 61 | cnmetdval 22384 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝐶 − 𝑥))) |
422 | | abssub 13914 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(abs‘(𝐶 − 𝑥)) = (abs‘(𝑥 − 𝐶))) |
423 | 421, 422 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐶))) |
424 | 25, 423 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐶))) |
425 | 424 | breq1d 4593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝐶(abs ∘ − )𝑥) ≤ 𝐸 ↔ (abs‘(𝑥 − 𝐶)) ≤ 𝐸)) |
426 | 425 | rabbidva 3163 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (abs‘(𝑥 − 𝐶)) ≤ 𝐸}) |
427 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
428 | 29 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
429 | | eqid 2610 |
. . . . . . . . . 10
⊢ {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} |
430 | 48, 429 | blcld 22120 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ*) → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld))) |
431 | 427, 25, 428, 430 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld))) |
432 | 426, 431 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ (abs‘(𝑥 − 𝐶)) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld))) |
433 | 47 | cnfldtopon 22396 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
434 | 433 | toponunii 20547 |
. . . . . . . 8
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
435 | 434 | cldopn 20645 |
. . . . . . 7
⊢ ({𝑥 ∈ ℂ ∣
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖
{𝑥 ∈ ℂ ∣
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) ∈
(TopOpen‘ℂfld)) |
436 | 432, 435 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ℂ ∖ {𝑥 ∈ ℂ ∣
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) ∈
(TopOpen‘ℂfld)) |
437 | 420, 436 | syl5eqelr 2693 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ∈
(TopOpen‘ℂfld)) |
438 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐹‘𝑋) ∈ ℂ) |
439 | 1 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℝ) |
440 | 121, 439 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐹‘𝑧) ∈ ℝ) |
441 | 440 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐹‘𝑧) ∈ ℂ) |
442 | 438, 441 | subcld 10271 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐹‘𝑋) − (𝐹‘𝑧)) ∈ ℂ) |
443 | 120, 124 | subcld 10271 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ ℂ) |
444 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ (ℂ ∖ {0}) ↔
(((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ ℂ ∧ ((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0)) |
445 | 443, 213,
444 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ (ℂ ∖
{0})) |
446 | | ssid 3587 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
447 | 446 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) |
448 | | difss 3699 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ⊆ ℂ |
449 | 448 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
450 | | cnex 9896 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
451 | 450, 448 | ssexi 4731 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ V |
452 | | txrest 21244 |
. . . . . . . . . 10
⊢
((((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) ∧
(ℂ ∈ V ∧ (ℂ ∖ {0}) ∈ V)) →
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
(ℂ ∖ {0}))) = (((TopOpen‘ℂfld)
↾t ℂ) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0})))) |
453 | 433, 433,
450, 451, 452 | mp4an 705 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
(ℂ ∖ {0}))) = (((TopOpen‘ℂfld)
↾t ℂ) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) |
454 | 434 | restid 15917 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
455 | 433, 454 | ax-mp 5 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
456 | 455 | oveq1i 6559 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ↾t ℂ)
×t ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0}))) = ((TopOpen‘ℂfld)
×t ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0}))) |
457 | 453, 456 | eqtr2i 2633 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) = (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
(ℂ ∖ {0}))) |
458 | 9 | subid1d 10260 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑋) − 0) = (𝐹‘𝑋)) |
459 | | txtopon 21204 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
→ ((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ))) |
460 | 433, 433,
459 | mp2an 704 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ)) |
461 | 460 | toponunii 20547 |
. . . . . . . . . . . . 13
⊢ (ℂ
× ℂ) = ∪
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) |
462 | 461 | restid 15917 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ)) → (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
ℂ)) = ((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld))) |
463 | 460, 462 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
ℂ)) = ((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) |
464 | 463 | eqcomi 2619 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
ℂ)) |
465 | | limcresi 23455 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) limℂ 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
466 | | ioossre 12106 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝑋) ⊆ ℝ |
467 | | resmpt 5369 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋))) |
468 | 466, 467 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) |
469 | 468 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) limℂ 𝐴) |
470 | 465, 469 | sseqtri 3600 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) limℂ 𝐴) |
471 | | cncfmptc 22522 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑋) ∈ ℝ ∧ ℝ ⊆
ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ∈ (ℝ–cn→ℝ)) |
472 | 8, 144, 144, 471 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ∈ (ℝ–cn→ℝ)) |
473 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐴 → (𝐹‘𝑋) = (𝐹‘𝑋)) |
474 | 472, 40, 473 | cnmptlimc 23460 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) limℂ 𝐴)) |
475 | 470, 474 | sseldi 3566 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) limℂ 𝐴)) |
476 | | limcresi 23455 |
. . . . . . . . . . . 12
⊢ (𝐹 limℂ 𝐴) ⊆ ((𝐹 ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
477 | 1, 107 | feqresmpt 6160 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧))) |
478 | 477 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧)) limℂ 𝐴)) |
479 | 476, 478 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧)) limℂ 𝐴)) |
480 | | lhop1.f0 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐴)) |
481 | 479, 480 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧)) limℂ 𝐴)) |
482 | 47 | subcn 22477 |
. . . . . . . . . . 11
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
483 | | 0cn 9911 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
484 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑋) ∈ ℂ ∧ 0 ∈ ℂ)
→ 〈(𝐹‘𝑋), 0〉 ∈ (ℂ
× ℂ)) |
485 | 9, 483, 484 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈(𝐹‘𝑋), 0〉 ∈ (ℂ ×
ℂ)) |
486 | 461 | cncnpi 20892 |
. . . . . . . . . . 11
⊢ ((
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) ∧ 〈(𝐹‘𝑋), 0〉 ∈ (ℂ × ℂ))
→ − ∈ ((((TopOpen‘ℂfld)
×t (TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐹‘𝑋), 0〉)) |
487 | 482, 485,
486 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → − ∈
((((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐹‘𝑋), 0〉)) |
488 | 438, 441,
447, 447, 47, 464, 475, 481, 487 | limccnp2 23462 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹‘𝑋) − (𝐹‘𝑧))) limℂ 𝐴)) |
489 | 458, 488 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹‘𝑋) − (𝐹‘𝑧))) limℂ 𝐴)) |
490 | 12 | subid1d 10260 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺‘𝑋) − 0) = (𝐺‘𝑋)) |
491 | | limcresi 23455 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) limℂ 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
492 | | resmpt 5369 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋))) |
493 | 466, 492 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) |
494 | 493 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) limℂ 𝐴) |
495 | 491, 494 | sseqtri 3600 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) limℂ 𝐴) |
496 | | cncfmptc 22522 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑋) ∈ ℝ ∧ ℝ ⊆
ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ∈ (ℝ–cn→ℝ)) |
497 | 11, 144, 144, 496 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ∈ (ℝ–cn→ℝ)) |
498 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐴 → (𝐺‘𝑋) = (𝐺‘𝑋)) |
499 | 497, 40, 498 | cnmptlimc 23460 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) limℂ 𝐴)) |
500 | 495, 499 | sseldi 3566 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) limℂ 𝐴)) |
501 | | limcresi 23455 |
. . . . . . . . . . . 12
⊢ (𝐺 limℂ 𝐴) ⊆ ((𝐺 ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
502 | 10, 107 | feqresmpt 6160 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧))) |
503 | 502 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧)) limℂ 𝐴)) |
504 | 501, 503 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧)) limℂ 𝐴)) |
505 | | lhop1.g0 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐴)) |
506 | 504, 505 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧)) limℂ 𝐴)) |
507 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ (((𝐺‘𝑋) ∈ ℂ ∧ 0 ∈ ℂ)
→ 〈(𝐺‘𝑋), 0〉 ∈ (ℂ
× ℂ)) |
508 | 12, 483, 507 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈(𝐺‘𝑋), 0〉 ∈ (ℂ ×
ℂ)) |
509 | 461 | cncnpi 20892 |
. . . . . . . . . . 11
⊢ ((
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) ∧ 〈(𝐺‘𝑋), 0〉 ∈ (ℂ × ℂ))
→ − ∈ ((((TopOpen‘ℂfld)
×t (TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐺‘𝑋), 0〉)) |
510 | 482, 508,
509 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → − ∈
((((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐺‘𝑋), 0〉)) |
511 | 120, 124,
447, 447, 47, 464, 500, 506, 510 | limccnp2 23462 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺‘𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺‘𝑋) − (𝐺‘𝑧))) limℂ 𝐴)) |
512 | 490, 511 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺‘𝑋) − (𝐺‘𝑧))) limℂ 𝐴)) |
513 | | eqid 2610 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) = ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0})) |
514 | 47, 513 | divcn 22479 |
. . . . . . . . 9
⊢ / ∈
(((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld)) |
515 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑋) ∈ (ℂ ∖ {0}) ↔
((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑋) ≠ 0)) |
516 | 12, 21, 515 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑋) ∈ (ℂ ∖
{0})) |
517 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑋) ∈ ℂ ∧ (𝐺‘𝑋) ∈ (ℂ ∖ {0})) →
〈(𝐹‘𝑋), (𝐺‘𝑋)〉 ∈ (ℂ × (ℂ
∖ {0}))) |
518 | 9, 516, 517 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 〈(𝐹‘𝑋), (𝐺‘𝑋)〉 ∈ (ℂ × (ℂ
∖ {0}))) |
519 | | resttopon 20775 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (ℂ ∖ {0}) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0})) ∈ (TopOn‘(ℂ ∖ {0}))) |
520 | 433, 448,
519 | mp2an 704 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})) |
521 | | txtopon 21204 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))) →
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) ∈ (TopOn‘(ℂ × (ℂ ∖
{0})))) |
522 | 433, 520,
521 | mp2an 704 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) ∈ (TopOn‘(ℂ × (ℂ ∖
{0}))) |
523 | 522 | toponunii 20547 |
. . . . . . . . . 10
⊢ (ℂ
× (ℂ ∖ {0})) = ∪
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) |
524 | 523 | cncnpi 20892 |
. . . . . . . . 9
⊢ (( /
∈ (((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld)) ∧ 〈(𝐹‘𝑋), (𝐺‘𝑋)〉 ∈ (ℂ × (ℂ
∖ {0}))) → / ∈ ((((TopOpen‘ℂfld)
×t ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0}))) CnP
(TopOpen‘ℂfld))‘〈(𝐹‘𝑋), (𝐺‘𝑋)〉)) |
525 | 514, 518,
524 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → / ∈
((((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) CnP (TopOpen‘ℂfld))‘〈(𝐹‘𝑋), (𝐺‘𝑋)〉)) |
526 | 442, 445,
447, 449, 47, 457, 489, 512, 525 | limccnp2 23462 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) limℂ 𝐴)) |
527 | 442, 443,
213 | divcld 10680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))) ∈ ℂ) |
528 | 527, 388 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))):(𝐴(,)𝑋)⟶ℂ) |
529 | 466, 143 | sstri 3577 |
. . . . . . . . 9
⊢ (𝐴(,)𝑋) ⊆ ℂ |
530 | 529 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝑋) ⊆ ℂ) |
531 | 528, 530,
59, 47 | ellimc2 23447 |
. . . . . . 7
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) limℂ 𝐴) ↔ (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))))) |
532 | 526, 531 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))) |
533 | 532 | simprd 478 |
. . . . 5
⊢ (𝜑 → ∀𝑢 ∈
(TopOpen‘ℂfld)(((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))) |
534 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 ↔ ((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
535 | | sseq2 3590 |
. . . . . . . . 9
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
536 | 535 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ((𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ (𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
537 | 536 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
538 | 534, 537 | imbi12d 333 |
. . . . . 6
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ((((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) ↔ (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})))) |
539 | 538 | rspcv 3278 |
. . . . 5
⊢ ({𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ∈
(TopOpen‘ℂfld) → (∀𝑢 ∈
(TopOpen‘ℂfld)(((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})))) |
540 | 437, 533,
539 | sylc 63 |
. . . 4
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
541 | 419, 540 | sylbird 249 |
. . 3
⊢ (𝜑 → (¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
542 | 413, 541 | mt3d 139 |
. 2
⊢ (𝜑 → (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸) |
543 | 29 | recnd 9947 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ℂ) |
544 | 543 | mulid2d 9937 |
. . 3
⊢ (𝜑 → (1 · 𝐸) = 𝐸) |
545 | | 1red 9934 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
546 | | 1lt2 11071 |
. . . . 5
⊢ 1 <
2 |
547 | 546 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 < 2) |
548 | 545, 31, 28, 547 | ltmul1dd 11803 |
. . 3
⊢ (𝜑 → (1 · 𝐸) < (2 · 𝐸)) |
549 | 544, 548 | eqbrtrrd 4607 |
. 2
⊢ (𝜑 → 𝐸 < (2 · 𝐸)) |
550 | 27, 29, 32, 542, 549 | lelttrd 10074 |
1
⊢ (𝜑 → (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) < (2 · 𝐸)) |