| Step | Hyp | Ref
| Expression |
| 1 | | lhop1.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 2 | | lhop1.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 3 | | lhop1lem.db |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ≤ 𝐵) |
| 4 | | iooss2 13423 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐷 ≤ 𝐵) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵)) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵)) |
| 6 | | lhop1lem.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝐴(,)𝐷)) |
| 7 | 5, 6 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝐴(,)𝐵)) |
| 8 | 1, 7 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑋) ∈ ℝ) |
| 9 | 8 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑋) ∈ ℂ) |
| 10 | | lhop1.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
| 11 | 10, 7 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝑋) ∈ ℝ) |
| 12 | 11 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑋) ∈ ℂ) |
| 13 | | lhop1.gn0 |
. . . . . 6
⊢ (𝜑 → ¬ 0 ∈ ran 𝐺) |
| 14 | 10 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn (𝐴(,)𝐵)) |
| 15 | | fnfvelrn 7100 |
. . . . . . . . 9
⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑋 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑋) ∈ ran 𝐺) |
| 16 | 14, 7, 15 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝑋) ∈ ran 𝐺) |
| 17 | | eleq1 2829 |
. . . . . . . 8
⊢ ((𝐺‘𝑋) = 0 → ((𝐺‘𝑋) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺)) |
| 18 | 16, 17 | syl5ibcom 245 |
. . . . . . 7
⊢ (𝜑 → ((𝐺‘𝑋) = 0 → 0 ∈ ran 𝐺)) |
| 19 | 18 | necon3bd 2954 |
. . . . . 6
⊢ (𝜑 → (¬ 0 ∈ ran 𝐺 → (𝐺‘𝑋) ≠ 0)) |
| 20 | 13, 19 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑋) ≠ 0) |
| 21 | 9, 12, 20 | divcld 12043 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ) |
| 22 | | limccl 25910 |
. . . . 5
⊢ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐴) ⊆ ℂ |
| 23 | | lhop1.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐴)) |
| 24 | 22, 23 | sselid 3981 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 25 | 21, 24 | subcld 11620 |
. . 3
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶) ∈ ℂ) |
| 26 | 25 | abscld 15475 |
. 2
⊢ (𝜑 → (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ∈ ℝ) |
| 27 | | lhop1lem.e |
. . 3
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 28 | 27 | rpred 13077 |
. 2
⊢ (𝜑 → 𝐸 ∈ ℝ) |
| 29 | | 2re 12340 |
. . . 4
⊢ 2 ∈
ℝ |
| 30 | 29 | a1i 11 |
. . 3
⊢ (𝜑 → 2 ∈
ℝ) |
| 31 | 30, 28 | remulcld 11291 |
. 2
⊢ (𝜑 → (2 · 𝐸) ∈
ℝ) |
| 32 | | cnxmet 24793 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 33 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → (abs ∘ − )
∈ (∞Met‘ℂ)) |
| 34 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → 𝑣 ∈
(TopOpen‘ℂfld)) |
| 35 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → 𝐴 ∈ 𝑣) |
| 36 | | eliooord 13446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (𝐴(,)𝐷) → (𝐴 < 𝑋 ∧ 𝑋 < 𝐷)) |
| 37 | 6, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 < 𝑋 ∧ 𝑋 < 𝐷)) |
| 38 | 37 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 < 𝑋) |
| 39 | | lhop1.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 40 | | ioossre 13448 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴(,)𝐷) ⊆ ℝ |
| 41 | 40, 6 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 42 | | difrp 13073 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐴 < 𝑋 ↔ (𝑋 − 𝐴) ∈
ℝ+)) |
| 43 | 39, 41, 42 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 < 𝑋 ↔ (𝑋 − 𝐴) ∈
ℝ+)) |
| 44 | 38, 43 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 − 𝐴) ∈
ℝ+) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → (𝑋 − 𝐴) ∈
ℝ+) |
| 46 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 47 | 46 | cnfldtopn 24802 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
| 48 | 47 | mopni3 24507 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣) ∧ (𝑋 − 𝐴) ∈ ℝ+) →
∃𝑟 ∈
ℝ+ (𝑟 <
(𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣)) |
| 49 | 33, 34, 35, 45, 48 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑟 ∈ ℝ+
(𝑟 < (𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣)) |
| 50 | | ssrin 4242 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴(ball‘(abs ∘ −
))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ (𝐴(,)𝑋))) |
| 51 | | lbioo 13418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
𝐴 ∈ (𝐴(,)𝑋) |
| 52 | | disjsn 4711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝑋)) |
| 53 | 51, 52 | mpbir 231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴(,)𝑋) ∩ {𝐴}) = ∅ |
| 54 | | disj3 4454 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴(,)𝑋) ∩ {𝐴}) = ∅ ↔ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴})) |
| 55 | 53, 54 | mpbi 230 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝑋) = ((𝐴(,)𝑋) ∖ {𝐴}) |
| 56 | 55 | ineq2i 4217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∩ (𝐴(,)𝑋)) = (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) |
| 57 | 50, 56 | sseqtrdi 4024 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴(ball‘(abs ∘ −
))𝑟) ⊆ 𝑣 → ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) |
| 58 | | lhop1lem.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑅 = (𝐴 + (𝑟 / 2)) |
| 59 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ∈ ℝ) |
| 60 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℝ+) |
| 61 | 60 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℝ) |
| 62 | 61 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈ ℝ) |
| 63 | 59, 62 | readdcld 11290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴 + (𝑟 / 2)) ∈ ℝ) |
| 64 | 58, 63 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ ℝ) |
| 65 | 64 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ ℂ) |
| 66 | 39 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ∈ ℂ) |
| 68 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 69 | 68 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅 − 𝐴))) |
| 70 | 65, 67, 69 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(abs ∘ − )𝐴) = (abs‘(𝑅 − 𝐴))) |
| 71 | 58 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 − 𝐴) = ((𝐴 + (𝑟 / 2)) − 𝐴) |
| 72 | 61 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℂ) |
| 73 | 72 | halfcld 12511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈ ℂ) |
| 74 | 67, 73 | pncan2d 11622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐴 + (𝑟 / 2)) − 𝐴) = (𝑟 / 2)) |
| 75 | 71, 74 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅 − 𝐴) = (𝑟 / 2)) |
| 76 | 75 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘(𝑅 − 𝐴)) = (abs‘(𝑟 / 2))) |
| 77 | 60 | rphalfcld 13089 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈
ℝ+) |
| 78 | 77 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) ∈ ℝ) |
| 79 | 77 | rpge0d 13081 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 0 ≤ (𝑟 / 2)) |
| 80 | 78, 79 | absidd 15461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘(𝑟 / 2)) = (𝑟 / 2)) |
| 81 | 70, 76, 80 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(abs ∘ − )𝐴) = (𝑟 / 2)) |
| 82 | | rphalflt 13064 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
| 83 | 60, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) < 𝑟) |
| 84 | 81, 83 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(abs ∘ − )𝐴) < 𝑟) |
| 85 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
| 86 | 61 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 ∈ ℝ*) |
| 87 | | elbl3 24402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟)) |
| 88 | 85, 86, 67, 65, 87 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐴) < 𝑟)) |
| 89 | 84, 88 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ (𝐴(ball‘(abs ∘ − ))𝑟)) |
| 90 | 59, 77 | ltaddrpd 13110 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 < (𝐴 + (𝑟 / 2))) |
| 91 | 90, 58 | breqtrrdi 5185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 < 𝑅) |
| 92 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 ∈ ℝ) |
| 93 | 92, 59 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑋 − 𝐴) ∈ ℝ) |
| 94 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑟 < (𝑋 − 𝐴)) |
| 95 | 78, 61, 93, 83, 94 | lttrd 11422 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑟 / 2) < (𝑋 − 𝐴)) |
| 96 | 59, 78, 92 | ltaddsub2d 11864 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐴 + (𝑟 / 2)) < 𝑋 ↔ (𝑟 / 2) < (𝑋 − 𝐴))) |
| 97 | 95, 96 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴 + (𝑟 / 2)) < 𝑋) |
| 98 | 58, 97 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 < 𝑋) |
| 99 | 59 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ∈
ℝ*) |
| 100 | 41 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
| 101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 ∈
ℝ*) |
| 102 | | elioo2 13428 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℝ*
∧ 𝑋 ∈
ℝ*) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅 ∧ 𝑅 < 𝑋))) |
| 103 | 99, 101, 102 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅 ∈ (𝐴(,)𝑋) ↔ (𝑅 ∈ ℝ ∧ 𝐴 < 𝑅 ∧ 𝑅 < 𝑋))) |
| 104 | 64, 91, 98, 103 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ (𝐴(,)𝑋)) |
| 105 | 89, 104 | elind 4200 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))) |
| 106 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹‘𝑋) ∈ ℂ) |
| 107 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 108 | | lhop1lem.d |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 109 | 108 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
| 110 | 37 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑋 < 𝐷) |
| 111 | 41, 108, 110 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑋 ≤ 𝐷) |
| 112 | 100, 109,
2, 111, 3 | xrletrd 13204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑋 ≤ 𝐵) |
| 113 | | iooss2 13423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ ℝ*
∧ 𝑋 ≤ 𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) |
| 114 | 2, 112, 113 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) |
| 115 | 114 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) |
| 116 | 115, 104 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈ (𝐴(,)𝐵)) |
| 117 | 107, 116 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹‘𝑅) ∈ ℝ) |
| 118 | 117 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹‘𝑅) ∈ ℂ) |
| 119 | 106, 118 | subcld 11620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐹‘𝑋) − (𝐹‘𝑅)) ∈ ℂ) |
| 120 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺‘𝑋) ∈ ℂ) |
| 121 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
| 122 | 121, 116 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺‘𝑅) ∈ ℝ) |
| 123 | 122 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺‘𝑅) ∈ ℂ) |
| 124 | 120, 123 | subcld 11620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ∈ ℂ) |
| 125 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑅 → (𝐺‘𝑧) = (𝐺‘𝑅)) |
| 126 | 125 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑅 → ((𝐺‘𝑋) − (𝐺‘𝑧)) = ((𝐺‘𝑋) − (𝐺‘𝑅))) |
| 127 | 126 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑅 → (((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0 ↔ ((𝐺‘𝑋) − (𝐺‘𝑅)) ≠ 0)) |
| 128 | | lhop1.gd0 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐺)) |
| 129 | 128 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
| 130 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐺‘𝑋) ∈ ℂ) |
| 131 | 114 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝐴(,)𝐵)) |
| 132 | 10 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℝ) |
| 133 | 131, 132 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐺‘𝑧) ∈ ℝ) |
| 134 | 133 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐺‘𝑧) ∈ ℂ) |
| 135 | 130, 134 | subeq0ad 11630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺‘𝑋) − (𝐺‘𝑧)) = 0 ↔ (𝐺‘𝑋) = (𝐺‘𝑧))) |
| 136 | | ioossre 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 137 | 136, 131 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ) |
| 138 | 137 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝑧 ∈ ℝ) |
| 139 | 41 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝑋 ∈ ℝ) |
| 140 | | eliooord 13446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ (𝐴(,)𝑋) → (𝐴 < 𝑧 ∧ 𝑧 < 𝑋)) |
| 141 | 140 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐴 < 𝑧 ∧ 𝑧 < 𝑋)) |
| 142 | 141 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 < 𝑋) |
| 143 | 142 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝑧 < 𝑋) |
| 144 | 39 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 145 | 144 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 ∈
ℝ*) |
| 146 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝐵 ∈
ℝ*) |
| 147 | 141 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝐴 < 𝑧) |
| 148 | 100, 109,
2, 110, 3 | xrltletrd 13203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 𝑋 < 𝐵) |
| 149 | 148 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 < 𝐵) |
| 150 | | iccssioo 13456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < 𝑧 ∧ 𝑋 < 𝐵)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵)) |
| 151 | 145, 146,
147, 149, 150 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵)) |
| 152 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧[,]𝑋) ⊆ (𝐴(,)𝐵)) |
| 153 | | ax-resscn 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ℝ
⊆ ℂ |
| 154 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 155 | | fss 6752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
| 156 | 10, 153, 155 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
| 157 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
| 158 | | lhop1.ig |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
| 159 | | dvcn 25957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 160 | 154, 156,
157, 158, 159 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 161 | | cncfcdm 24924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((ℝ
⊆ ℂ ∧ 𝐺
∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ)) |
| 162 | 153, 160,
161 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐺:(𝐴(,)𝐵)⟶ℝ)) |
| 163 | 10, 162 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 164 | 163 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 165 | | rescncf 24923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑧[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ))) |
| 166 | 152, 164,
165 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝐺 ↾ (𝑧[,]𝑋)) ∈ ((𝑧[,]𝑋)–cn→ℝ)) |
| 167 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ℝ ⊆
ℂ) |
| 168 | 156 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
| 169 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝐴(,)𝐵) ⊆ ℝ) |
| 170 | 152, 136 | sstrdi 3996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧[,]𝑋) ⊆ ℝ) |
| 171 | | tgioo4 24826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 172 | 46, 171 | dvres 25946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑧[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋)))) |
| 173 | 167, 168,
169, 170, 172 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋)))) |
| 174 | | iccntr 24843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈ ℝ ∧ 𝑋 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋)) |
| 175 | 138, 139,
174 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋)) = (𝑧(,)𝑋)) |
| 176 | 175 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋))) |
| 177 | 173, 176 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑧(,)𝑋))) |
| 178 | 177 | dmeqd 5916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋))) |
| 179 | | ioossicc 13473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧(,)𝑋) ⊆ (𝑧[,]𝑋) |
| 180 | 179, 152 | sstrid 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧(,)𝑋) ⊆ (𝐴(,)𝐵)) |
| 181 | 158 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
| 182 | 180, 181 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺)) |
| 183 | | ssdmres 6031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑧(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋)) |
| 184 | 182, 183 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom ((ℝ D 𝐺) ↾ (𝑧(,)𝑋)) = (𝑧(,)𝑋)) |
| 185 | 178, 184 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → dom (ℝ D (𝐺 ↾ (𝑧[,]𝑋))) = (𝑧(,)𝑋)) |
| 186 | 137 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ ℝ*) |
| 187 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈
ℝ*) |
| 188 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ ℝ) |
| 189 | 137, 188,
142 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ≤ 𝑋) |
| 190 | | ubicc2 13505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑧
≤ 𝑋) → 𝑋 ∈ (𝑧[,]𝑋)) |
| 191 | 186, 187,
189, 190 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑋 ∈ (𝑧[,]𝑋)) |
| 192 | 191 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = (𝐺‘𝑋)) |
| 193 | | lbicc2 13504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑧
≤ 𝑋) → 𝑧 ∈ (𝑧[,]𝑋)) |
| 194 | 186, 187,
189, 193 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → 𝑧 ∈ (𝑧[,]𝑋)) |
| 195 | 194 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = (𝐺‘𝑧)) |
| 196 | 192, 195 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) ↔ (𝐺‘𝑋) = (𝐺‘𝑧))) |
| 197 | 196 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧)) |
| 198 | 197 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((𝐺 ↾ (𝑧[,]𝑋))‘𝑧) = ((𝐺 ↾ (𝑧[,]𝑋))‘𝑋)) |
| 199 | 138, 139,
143, 166, 185, 198 | rolle 26028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0) |
| 200 | 177 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤)) |
| 201 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 ∈ (𝑧(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑧(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
| 202 | 200, 201 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
| 203 | | dvf 25942 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
| 204 | 158 | feq2d 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ
D 𝐺):(𝐴(,)𝐵)⟶ℂ)) |
| 205 | 203, 204 | mpbii 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
| 206 | 205 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
| 207 | 206 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
| 208 | 207 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
| 209 | 180 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵)) |
| 210 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((ℝ D 𝐺) Fn
(𝐴(,)𝐵) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺)) |
| 211 | 208, 209,
210 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺)) |
| 212 | 202, 211 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺)) |
| 213 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((ℝ D (𝐺
↾ (𝑧[,]𝑋)))‘𝑤) = 0 → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
| 214 | 212, 213 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) ∧ 𝑤 ∈ (𝑧(,)𝑋)) → (((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
| 215 | 214 | rexlimdva 3155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → (∃𝑤 ∈ (𝑧(,)𝑋)((ℝ D (𝐺 ↾ (𝑧[,]𝑋)))‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
| 216 | 199, 215 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) ∧ (𝐺‘𝑋) = (𝐺‘𝑧)) → 0 ∈ ran (ℝ D 𝐺)) |
| 217 | 216 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) = (𝐺‘𝑧) → 0 ∈ ran (ℝ D 𝐺))) |
| 218 | 135, 217 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐺‘𝑋) − (𝐺‘𝑧)) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
| 219 | 218 | necon3bd 2954 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0)) |
| 220 | 129, 219 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0) |
| 221 | 220 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0) |
| 222 | 221 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∀𝑧 ∈ (𝐴(,)𝑋)((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0) |
| 223 | 127, 222,
104 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ≠ 0) |
| 224 | 119, 124,
223 | divcld 12043 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) ∈ ℂ) |
| 225 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐶 ∈ ℂ) |
| 226 | 224, 225 | subcld 11620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶) ∈ ℂ) |
| 227 | 226 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ∈ ℝ) |
| 228 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐸 ∈ ℝ) |
| 229 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐷 ∈
ℝ*) |
| 230 | 110 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 < 𝐷) |
| 231 | | iccssioo 13456 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ ℝ*
∧ 𝐷 ∈
ℝ*) ∧ (𝐴 < 𝑅 ∧ 𝑋 < 𝐷)) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷)) |
| 232 | 99, 229, 91, 230, 231 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐷)) |
| 233 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝐷) ⊆ (𝐴(,)𝐵)) |
| 234 | 232, 233 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅[,]𝑋) ⊆ (𝐴(,)𝐵)) |
| 235 | | fss 6752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
| 236 | 1, 153, 235 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
| 237 | | lhop1.if |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 238 | | dvcn 25957 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 239 | 154, 236,
157, 237, 238 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 240 | | cncfcdm 24924 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
| 241 | 153, 239,
240 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
| 242 | 1, 241 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 243 | 242 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 244 | | rescncf 24923 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))) |
| 245 | 234, 243,
244 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐹 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)) |
| 246 | 163 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 247 | | rescncf 24923 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅[,]𝑋) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℝ) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ))) |
| 248 | 234, 246,
247 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐺 ↾ (𝑅[,]𝑋)) ∈ ((𝑅[,]𝑋)–cn→ℝ)) |
| 249 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ℝ ⊆
ℂ) |
| 250 | 236 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
| 251 | 136 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝐵) ⊆ ℝ) |
| 252 | | iccssre 13469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑅[,]𝑋) ⊆ ℝ) |
| 253 | 64, 92, 252 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅[,]𝑋) ⊆ ℝ) |
| 254 | 46, 171 | dvres 25946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
| 255 | 249, 250,
251, 253, 254 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
| 256 | | iccntr 24843 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋)) |
| 257 | 64, 92, 256 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)) = (𝑅(,)𝑋)) |
| 258 | 257 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋))) |
| 259 | 255, 258 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐹) ↾ (𝑅(,)𝑋))) |
| 260 | 259 | dmeqd 5916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋))) |
| 261 | 59, 64, 91 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐴 ≤ 𝑅) |
| 262 | | iooss1 13422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑅) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋)) |
| 263 | 99, 261, 262 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝑋)) |
| 264 | 111 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑋 ≤ 𝐷) |
| 265 | | iooss2 13423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐷 ∈ ℝ*
∧ 𝑋 ≤ 𝐷) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷)) |
| 266 | 229, 264,
265 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐷)) |
| 267 | 263, 266 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐷)) |
| 268 | 267, 233 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ (𝐴(,)𝐵)) |
| 269 | 237 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 270 | 268, 269 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹)) |
| 271 | | ssdmres 6031 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
| 272 | 270, 271 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom ((ℝ D 𝐹) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
| 273 | 260, 272 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐹 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋)) |
| 274 | 156 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
| 275 | 46, 171 | dvres 25946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ) ∧ ((𝐴(,)𝐵) ⊆ ℝ ∧ (𝑅[,]𝑋) ⊆ ℝ)) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
| 276 | 249, 274,
251, 253, 275 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋)))) |
| 277 | 257 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D 𝐺) ↾ ((int‘(topGen‘ran
(,)))‘(𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋))) |
| 278 | 276, 277 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = ((ℝ D 𝐺) ↾ (𝑅(,)𝑋))) |
| 279 | 278 | dmeqd 5916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋))) |
| 280 | 158 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
| 281 | 268, 280 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺)) |
| 282 | | ssdmres 6031 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅(,)𝑋) ⊆ dom (ℝ D 𝐺) ↔ dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
| 283 | 281, 282 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom ((ℝ D 𝐺) ↾ (𝑅(,)𝑋)) = (𝑅(,)𝑋)) |
| 284 | 279, 283 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → dom (ℝ D (𝐺 ↾ (𝑅[,]𝑋))) = (𝑅(,)𝑋)) |
| 285 | 64, 92, 98, 245, 248, 273, 284 | cmvth 26029 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤))) |
| 286 | 64 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ∈
ℝ*) |
| 287 | 286 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈
ℝ*) |
| 288 | 100 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈
ℝ*) |
| 289 | 64, 92, 98 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → 𝑅 ≤ 𝑋) |
| 290 | 289 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ≤ 𝑋) |
| 291 | | ubicc2 13505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑅
≤ 𝑋) → 𝑋 ∈ (𝑅[,]𝑋)) |
| 292 | 287, 288,
290, 291 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑋 ∈ (𝑅[,]𝑋)) |
| 293 | 292 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐹‘𝑋)) |
| 294 | | lbicc2 13504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑅
≤ 𝑋) → 𝑅 ∈ (𝑅[,]𝑋)) |
| 295 | 287, 288,
290, 294 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑅 ∈ (𝑅[,]𝑋)) |
| 296 | 295 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐹‘𝑅)) |
| 297 | 293, 296 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐹‘𝑋) − (𝐹‘𝑅))) |
| 298 | 278 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤)) |
| 299 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐺) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
| 300 | 298, 299 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐺)‘𝑤)) |
| 301 | 297, 300 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐹‘𝑋) − (𝐹‘𝑅)) · ((ℝ D 𝐺)‘𝑤))) |
| 302 | 292 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) = (𝐺‘𝑋)) |
| 303 | 295 | fvresd 6926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅) = (𝐺‘𝑅)) |
| 304 | 302, 303 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) = ((𝐺‘𝑋) − (𝐺‘𝑅))) |
| 305 | 259 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤)) |
| 306 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ (𝑅(,)𝑋) → (((ℝ D 𝐹) ↾ (𝑅(,)𝑋))‘𝑤) = ((ℝ D 𝐹)‘𝑤)) |
| 307 | 305, 306 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤) = ((ℝ D 𝐹)‘𝑤)) |
| 308 | 304, 307 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((𝐺‘𝑋) − (𝐺‘𝑅)) · ((ℝ D 𝐹)‘𝑤))) |
| 309 | 124 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ∈ ℂ) |
| 310 | | dvf 25942 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
| 311 | 237 | feq2d 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℂ)) |
| 312 | 310, 311 | mpbii 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
| 313 | 312 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
| 314 | 268 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐵)) |
| 315 | 313, 314 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ) |
| 316 | 309, 315 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((𝐺‘𝑋) − (𝐺‘𝑅)) · ((ℝ D 𝐹)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅)))) |
| 317 | 308, 316 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅)))) |
| 318 | 301, 317 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹‘𝑋) − (𝐹‘𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅))))) |
| 319 | 119 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐹‘𝑋) − (𝐹‘𝑅)) ∈ ℂ) |
| 320 | 205 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
| 321 | 320, 314 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ℂ) |
| 322 | 223 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑅)) ≠ 0) |
| 323 | 128 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
| 324 | 320 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
| 325 | 324, 314,
210 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺)) |
| 326 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((ℝ D 𝐺)‘𝑤) = 0 → (((ℝ D 𝐺)‘𝑤) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
| 327 | 325, 326 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((ℝ D 𝐺)‘𝑤) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
| 328 | 327 | necon3bd 2954 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((ℝ D 𝐺)‘𝑤) ≠ 0)) |
| 329 | 323, 328 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((ℝ D 𝐺)‘𝑤) ≠ 0) |
| 330 | 319, 309,
315, 321, 322, 329 | divmuleqd 12089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) ↔ (((𝐹‘𝑋) − (𝐹‘𝑅)) · ((ℝ D 𝐺)‘𝑤)) = (((ℝ D 𝐹)‘𝑤) · ((𝐺‘𝑋) − (𝐺‘𝑅))))) |
| 331 | 318, 330 | bitr4d 282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ (((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))) |
| 332 | 331 | rexbidva 3177 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)((((𝐹 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐹 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐺 ↾ (𝑅[,]𝑋)))‘𝑤)) = ((((𝐺 ↾ (𝑅[,]𝑋))‘𝑋) − ((𝐺 ↾ (𝑅[,]𝑋))‘𝑅)) · ((ℝ D (𝐹 ↾ (𝑅[,]𝑋)))‘𝑤)) ↔ ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)))) |
| 333 | 285, 332 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))) |
| 334 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑤 → ((ℝ D 𝐹)‘𝑡) = ((ℝ D 𝐹)‘𝑤)) |
| 335 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑤 → ((ℝ D 𝐺)‘𝑡) = ((ℝ D 𝐺)‘𝑤)) |
| 336 | 334, 335 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑤 → (((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤))) |
| 337 | 336 | fvoveq1d 7453 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑤 → (abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶))) |
| 338 | 337 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑤 → ((abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)) |
| 339 | | lhop1lem.t |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸) |
| 340 | 339 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ∀𝑡 ∈ (𝐴(,)𝐷)(abs‘((((ℝ D 𝐹)‘𝑡) / ((ℝ D 𝐺)‘𝑡)) − 𝐶)) < 𝐸) |
| 341 | 267 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → 𝑤 ∈ (𝐴(,)𝐷)) |
| 342 | 338, 340,
341 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸) |
| 343 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶))) |
| 344 | 343 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → ((abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸 ↔ (abs‘((((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) − 𝐶)) < 𝐸)) |
| 345 | 342, 344 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) ∧ 𝑤 ∈ (𝑅(,)𝑋)) → ((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸)) |
| 346 | 345 | rexlimdva 3155 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (∃𝑤 ∈ (𝑅(,)𝑋)(((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) = (((ℝ D 𝐹)‘𝑤) / ((ℝ D 𝐺)‘𝑤)) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸)) |
| 347 | 333, 346 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) < 𝐸) |
| 348 | 227, 228,
347 | ltled 11409 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ≤ 𝐸) |
| 349 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑅 → (𝐹‘𝑢) = (𝐹‘𝑅)) |
| 350 | 349 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑅 → ((𝐹‘𝑋) − (𝐹‘𝑢)) = ((𝐹‘𝑋) − (𝐹‘𝑅))) |
| 351 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑅 → (𝐺‘𝑢) = (𝐺‘𝑅)) |
| 352 | 351 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑅 → ((𝐺‘𝑋) − (𝐺‘𝑢)) = ((𝐺‘𝑋) − (𝐺‘𝑅))) |
| 353 | 350, 352 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑅 → (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) = (((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅)))) |
| 354 | 353 | fvoveq1d 7453 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑅 → (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) = (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶))) |
| 355 | 354 | breq1d 5153 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑅 → ((abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ≤ 𝐸)) |
| 356 | 355 | rspcev 3622 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋)) ∧ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑅)) / ((𝐺‘𝑋) − (𝐺‘𝑅))) − 𝐶)) ≤ 𝐸) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
| 357 | 105, 348,
356 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
| 358 | 357 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
| 359 | | ssrexv 4053 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴(ball‘(abs ∘ −
))𝑟) ∩ (𝐴(,)𝑋)) ⊆ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → (∃𝑢 ∈ ((𝐴(ball‘(abs ∘ − ))𝑟) ∩ (𝐴(,)𝑋))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
| 360 | 57, 358, 359 | syl2imc 41 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ (𝑟 ∈ ℝ+ ∧ 𝑟 < (𝑋 − 𝐴))) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
| 361 | 360 | anassrs 467 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < (𝑋 − 𝐴)) → ((𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣 → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
| 362 | 361 | expimpd 453 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 < (𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
| 363 | 362 | rexlimdva 3155 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → (∃𝑟 ∈ ℝ+
(𝑟 < (𝑋 − 𝐴) ∧ (𝐴(ball‘(abs ∘ − ))𝑟) ⊆ 𝑣) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
| 364 | 49, 363 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
| 365 | | inss2 4238 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ ((𝐴(,)𝑋) ∖ {𝐴}) |
| 366 | | difss 4136 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝑋) ∖ {𝐴}) ⊆ (𝐴(,)𝑋) |
| 367 | 365, 366 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋) |
| 368 | 367 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → 𝑢 ∈ (𝐴(,)𝑋)) |
| 369 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑢 → (𝐹‘𝑧) = (𝐹‘𝑢)) |
| 370 | 369 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑢 → ((𝐹‘𝑋) − (𝐹‘𝑧)) = ((𝐹‘𝑋) − (𝐹‘𝑢))) |
| 371 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑢 → (𝐺‘𝑧) = (𝐺‘𝑢)) |
| 372 | 371 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑢 → ((𝐺‘𝑋) − (𝐺‘𝑧)) = ((𝐺‘𝑋) − (𝐺‘𝑢))) |
| 373 | 370, 372 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑢 → (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))) = (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢)))) |
| 374 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) |
| 375 | | ovex 7464 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) ∈ V |
| 376 | 373, 374,
375 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (𝐴(,)𝑋) → ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) = (((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢)))) |
| 377 | 376 | fvoveq1d 7453 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (𝐴(,)𝑋) → (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) = (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶))) |
| 378 | 377 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝐴(,)𝑋) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
| 379 | 368, 378 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) → ((abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ (abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸)) |
| 380 | 379 | rexbiia 3092 |
. . . . . . . . . 10
⊢
(∃𝑢 ∈
(𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘((((𝐹‘𝑋) − (𝐹‘𝑢)) / ((𝐺‘𝑋) − (𝐺‘𝑢))) − 𝐶)) ≤ 𝐸) |
| 381 | 364, 380 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸) |
| 382 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))) ∈ V |
| 383 | 382, 374 | fnmpti 6711 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) Fn (𝐴(,)𝑋) |
| 384 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) → (abs‘(𝑥 − 𝐶)) = (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶))) |
| 385 | 384 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) → ((abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)) |
| 386 | 385 | rexima 7258 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) Fn (𝐴(,)𝑋) ∧ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})) ⊆ (𝐴(,)𝑋)) → (∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸)) |
| 387 | 383, 367,
386 | mp2an 692 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ∃𝑢 ∈ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))(abs‘(((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))))‘𝑢) − 𝐶)) ≤ 𝐸) |
| 388 | 381, 387 | sylibr 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ∃𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
| 389 | | dfrex2 3073 |
. . . . . . . 8
⊢
(∃𝑥 ∈
((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴})))(abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
| 390 | 388, 389 | sylib 218 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ¬ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
| 391 | | ssrab 4073 |
. . . . . . . 8
⊢ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ↔ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ ℂ ∧ ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸)) |
| 392 | 391 | simprbi 496 |
. . . . . . 7
⊢ (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ∀𝑥 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸) |
| 393 | 390, 392 | nsyl 140 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐴 ∈ 𝑣)) → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) |
| 394 | 393 | expr 456 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈
(TopOpen‘ℂfld)) → (𝐴 ∈ 𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
| 395 | 394 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
| 396 | | ralinexa 3101 |
. . . 4
⊢
(∀𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 → ¬ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) ↔ ¬ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
| 397 | 395, 396 | sylib 218 |
. . 3
⊢ (𝜑 → ¬ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
| 398 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑥 = ((𝐹‘𝑋) / (𝐺‘𝑋)) → (abs‘(𝑥 − 𝐶)) = (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶))) |
| 399 | 398 | breq1d 5153 |
. . . . . . 7
⊢ (𝑥 = ((𝐹‘𝑋) / (𝐺‘𝑋)) → ((abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
| 400 | 399 | notbid 318 |
. . . . . 6
⊢ (𝑥 = ((𝐹‘𝑋) / (𝐺‘𝑋)) → (¬ (abs‘(𝑥 − 𝐶)) ≤ 𝐸 ↔ ¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
| 401 | 400 | elrab3 3693 |
. . . . 5
⊢ (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
| 402 | 21, 401 | syl 17 |
. . . 4
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ↔ ¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸)) |
| 403 | | eleq2 2830 |
. . . . . 6
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 ↔ ((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
| 404 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → (((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})) |
| 405 | 404 | anbi2d 630 |
. . . . . . 7
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ((𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ (𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
| 406 | 405 | rexbidv 3179 |
. . . . . 6
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢) ↔ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
| 407 | 403, 406 | imbi12d 344 |
. . . . 5
⊢ (𝑢 = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ((((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)) ↔ (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸})))) |
| 408 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐹‘𝑋) ∈ ℂ) |
| 409 | 1 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℝ) |
| 410 | 131, 409 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐹‘𝑧) ∈ ℝ) |
| 411 | 410 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (𝐹‘𝑧) ∈ ℂ) |
| 412 | 408, 411 | subcld 11620 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐹‘𝑋) − (𝐹‘𝑧)) ∈ ℂ) |
| 413 | 130, 134 | subcld 11620 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ ℂ) |
| 414 | | eldifsn 4786 |
. . . . . . . . 9
⊢ (((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ (ℂ ∖ {0}) ↔
(((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ ℂ ∧ ((𝐺‘𝑋) − (𝐺‘𝑧)) ≠ 0)) |
| 415 | 413, 220,
414 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → ((𝐺‘𝑋) − (𝐺‘𝑧)) ∈ (ℂ ∖
{0})) |
| 416 | | ssidd 4007 |
. . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 417 | | difss 4136 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ⊆ ℂ |
| 418 | 417 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
| 419 | 46 | cnfldtopon 24803 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 420 | | cnex 11236 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
| 421 | 420 | difexi 5330 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ V |
| 422 | | txrest 23639 |
. . . . . . . . . 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})))) |
| 423 | 419, 419,
420, 421, 422 | mp4an 693 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
(ℂ ∖ {0}))) = (((TopOpen‘ℂfld)
↾t ℂ) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) |
| 424 | | unicntop 24806 |
. . . . . . . . . . . 12
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
| 425 | 424 | restid 17478 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
| 426 | 419, 425 | ax-mp 5 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
| 427 | 426 | oveq1i 7441 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ↾t ℂ)
×t ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0}))) = ((TopOpen‘ℂfld)
×t ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0}))) |
| 428 | 423, 427 | eqtr2i 2766 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) = (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
(ℂ ∖ {0}))) |
| 429 | 9 | subid1d 11609 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑋) − 0) = (𝐹‘𝑋)) |
| 430 | | txtopon 23599 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
→ ((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ))) |
| 431 | 419, 419,
430 | mp2an 692 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ)) |
| 432 | 431 | toponrestid 22927 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
ℂ)) |
| 433 | | limcresi 25920 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) limℂ 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
| 434 | | ioossre 13448 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝑋) ⊆ ℝ |
| 435 | | resmpt 6055 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋))) |
| 436 | 434, 435 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) |
| 437 | 436 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) limℂ 𝐴) |
| 438 | 433, 437 | sseqtri 4032 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) limℂ 𝐴) |
| 439 | | cncfmptc 24938 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑋) ∈ ℝ ∧ ℝ ⊆
ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ∈ (ℝ–cn→ℝ)) |
| 440 | 8, 154, 154, 439 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) ∈ (ℝ–cn→ℝ)) |
| 441 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐴 → (𝐹‘𝑋) = (𝐹‘𝑋)) |
| 442 | 440, 39, 441 | cnmptlimc 25925 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐹‘𝑋)) limℂ 𝐴)) |
| 443 | 438, 442 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑋)) limℂ 𝐴)) |
| 444 | | limcresi 25920 |
. . . . . . . . . . . 12
⊢ (𝐹 limℂ 𝐴) ⊆ ((𝐹 ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
| 445 | 1, 114 | feqresmpt 6978 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧))) |
| 446 | 445 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧)) limℂ 𝐴)) |
| 447 | 444, 446 | sseqtrid 4026 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧)) limℂ 𝐴)) |
| 448 | | lhop1.f0 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐴)) |
| 449 | 447, 448 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑧)) limℂ 𝐴)) |
| 450 | 46 | subcn 24888 |
. . . . . . . . . . 11
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
| 451 | | 0cn 11253 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
| 452 | | opelxpi 5722 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑋) ∈ ℂ ∧ 0 ∈ ℂ)
→ 〈(𝐹‘𝑋), 0〉 ∈ (ℂ
× ℂ)) |
| 453 | 9, 451, 452 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈(𝐹‘𝑋), 0〉 ∈ (ℂ ×
ℂ)) |
| 454 | 431 | toponunii 22922 |
. . . . . . . . . . . 12
⊢ (ℂ
× ℂ) = ∪
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) |
| 455 | 454 | cncnpi 23286 |
. . . . . . . . . . 11
⊢ ((
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) ∧ 〈(𝐹‘𝑋), 0〉 ∈ (ℂ × ℂ))
→ − ∈ ((((TopOpen‘ℂfld)
×t (TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐹‘𝑋), 0〉)) |
| 456 | 450, 453,
455 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → − ∈
((((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐹‘𝑋), 0〉)) |
| 457 | 408, 411,
416, 416, 46, 432, 443, 449, 456 | limccnp2 25927 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹‘𝑋) − (𝐹‘𝑧))) limℂ 𝐴)) |
| 458 | 429, 457 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐹‘𝑋) − (𝐹‘𝑧))) limℂ 𝐴)) |
| 459 | 12 | subid1d 11609 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺‘𝑋) − 0) = (𝐺‘𝑋)) |
| 460 | | limcresi 25920 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) limℂ 𝐴) ⊆ (((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
| 461 | | resmpt 6055 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝑋) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋))) |
| 462 | 434, 461 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) |
| 463 | 462 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) limℂ 𝐴) |
| 464 | 460, 463 | sseqtri 4032 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) limℂ 𝐴) |
| 465 | | cncfmptc 24938 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑋) ∈ ℝ ∧ ℝ ⊆
ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ∈ (ℝ–cn→ℝ)) |
| 466 | 11, 154, 154, 465 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) ∈ (ℝ–cn→ℝ)) |
| 467 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐴 → (𝐺‘𝑋) = (𝐺‘𝑋)) |
| 468 | 466, 39, 467 | cnmptlimc 25925 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑋) ∈ ((𝑧 ∈ ℝ ↦ (𝐺‘𝑋)) limℂ 𝐴)) |
| 469 | 464, 468 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑋)) limℂ 𝐴)) |
| 470 | | limcresi 25920 |
. . . . . . . . . . . 12
⊢ (𝐺 limℂ 𝐴) ⊆ ((𝐺 ↾ (𝐴(,)𝑋)) limℂ 𝐴) |
| 471 | 10, 114 | feqresmpt 6978 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝑋)) = (𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧))) |
| 472 | 471 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 ↾ (𝐴(,)𝑋)) limℂ 𝐴) = ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧)) limℂ 𝐴)) |
| 473 | 470, 472 | sseqtrid 4026 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 limℂ 𝐴) ⊆ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧)) limℂ 𝐴)) |
| 474 | | lhop1.g0 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐴)) |
| 475 | 473, 474 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (𝐺‘𝑧)) limℂ 𝐴)) |
| 476 | | opelxpi 5722 |
. . . . . . . . . . . 12
⊢ (((𝐺‘𝑋) ∈ ℂ ∧ 0 ∈ ℂ)
→ 〈(𝐺‘𝑋), 0〉 ∈ (ℂ
× ℂ)) |
| 477 | 12, 451, 476 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈(𝐺‘𝑋), 0〉 ∈ (ℂ ×
ℂ)) |
| 478 | 454 | cncnpi 23286 |
. . . . . . . . . . 11
⊢ ((
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) ∧ 〈(𝐺‘𝑋), 0〉 ∈ (ℂ × ℂ))
→ − ∈ ((((TopOpen‘ℂfld)
×t (TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐺‘𝑋), 0〉)) |
| 479 | 450, 477,
478 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → − ∈
((((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈(𝐺‘𝑋), 0〉)) |
| 480 | 130, 134,
416, 416, 46, 432, 469, 475, 479 | limccnp2 25927 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺‘𝑋) − 0) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺‘𝑋) − (𝐺‘𝑧))) limℂ 𝐴)) |
| 481 | 459, 480 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝑋) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ ((𝐺‘𝑋) − (𝐺‘𝑧))) limℂ 𝐴)) |
| 482 | | eqid 2737 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) = ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0})) |
| 483 | 46, 482 | divcn 24892 |
. . . . . . . . 9
⊢ / ∈
(((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld)) |
| 484 | | eldifsn 4786 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑋) ∈ (ℂ ∖ {0}) ↔
((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑋) ≠ 0)) |
| 485 | 12, 20, 484 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑋) ∈ (ℂ ∖
{0})) |
| 486 | 9, 485 | opelxpd 5724 |
. . . . . . . . 9
⊢ (𝜑 → 〈(𝐹‘𝑋), (𝐺‘𝑋)〉 ∈ (ℂ × (ℂ
∖ {0}))) |
| 487 | | resttopon 23169 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (ℂ ∖ {0}) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0})) ∈ (TopOn‘(ℂ ∖ {0}))) |
| 488 | 419, 417,
487 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})) |
| 489 | | txtopon 23599 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) ∈ (TopOn‘(ℂ ∖ {0}))) →
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) ∈ (TopOn‘(ℂ × (ℂ ∖
{0})))) |
| 490 | 419, 488,
489 | mp2an 692 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) ∈ (TopOn‘(ℂ × (ℂ ∖
{0}))) |
| 491 | 490 | toponunii 22922 |
. . . . . . . . . 10
⊢ (ℂ
× (ℂ ∖ {0})) = ∪
((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) |
| 492 | 491 | cncnpi 23286 |
. . . . . . . . 9
⊢ (( /
∈ (((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld)) ∧ 〈(𝐹‘𝑋), (𝐺‘𝑋)〉 ∈ (ℂ × (ℂ
∖ {0}))) → / ∈ ((((TopOpen‘ℂfld)
×t ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0}))) CnP
(TopOpen‘ℂfld))‘〈(𝐹‘𝑋), (𝐺‘𝑋)〉)) |
| 493 | 483, 486,
492 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → / ∈
((((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) CnP (TopOpen‘ℂfld))‘〈(𝐹‘𝑋), (𝐺‘𝑋)〉)) |
| 494 | 412, 415,
416, 418, 46, 428, 458, 481, 493 | limccnp2 25927 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) limℂ 𝐴)) |
| 495 | 412, 413,
220 | divcld 12043 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝑋)) → (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧))) ∈ ℂ) |
| 496 | 495 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))):(𝐴(,)𝑋)⟶ℂ) |
| 497 | 434, 153 | sstri 3993 |
. . . . . . . . 9
⊢ (𝐴(,)𝑋) ⊆ ℂ |
| 498 | 497 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝑋) ⊆ ℂ) |
| 499 | 496, 498,
66, 46 | ellimc2 25912 |
. . . . . . 7
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) limℂ 𝐴) ↔ (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))))) |
| 500 | 494, 499 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢)))) |
| 501 | 500 | simprd 495 |
. . . . 5
⊢ (𝜑 → ∀𝑢 ∈
(TopOpen‘ℂfld)(((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ 𝑢))) |
| 502 | | notrab 4322 |
. . . . . 6
⊢ (ℂ
∖ {𝑥 ∈ ℂ
∣ (abs‘(𝑥
− 𝐶)) ≤ 𝐸}) = {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} |
| 503 | 68 | cnmetdval 24791 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝐶 − 𝑥))) |
| 504 | | abssub 15365 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(abs‘(𝐶 − 𝑥)) = (abs‘(𝑥 − 𝐶))) |
| 505 | 503, 504 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐶))) |
| 506 | 24, 505 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐶(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐶))) |
| 507 | 506 | breq1d 5153 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝐶(abs ∘ − )𝑥) ≤ 𝐸 ↔ (abs‘(𝑥 − 𝐶)) ≤ 𝐸)) |
| 508 | 507 | rabbidva 3443 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (abs‘(𝑥 − 𝐶)) ≤ 𝐸}) |
| 509 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
| 510 | 28 | rexrd 11311 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
| 511 | | eqid 2737 |
. . . . . . . . . 10
⊢ {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} = {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} |
| 512 | 47, 511 | blcld 24518 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℝ*) → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 513 | 509, 24, 510, 512 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ (𝐶(abs ∘ − )𝑥) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 514 | 508, 513 | eqeltrrd 2842 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ (abs‘(𝑥 − 𝐶)) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 515 | 424 | cldopn 23039 |
. . . . . . 7
⊢ ({𝑥 ∈ ℂ ∣
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ∈
(Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖
{𝑥 ∈ ℂ ∣
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) ∈
(TopOpen‘ℂfld)) |
| 516 | 514, 515 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ℂ ∖ {𝑥 ∈ ℂ ∣
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}) ∈
(TopOpen‘ℂfld)) |
| 517 | 502, 516 | eqeltrrid 2846 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} ∈
(TopOpen‘ℂfld)) |
| 518 | 407, 501,
517 | rspcdva 3623 |
. . . 4
⊢ (𝜑 → (((𝐹‘𝑋) / (𝐺‘𝑋)) ∈ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸} → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
| 519 | 402, 518 | sylbird 260 |
. . 3
⊢ (𝜑 → (¬ (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴(,)𝑋) ↦ (((𝐹‘𝑋) − (𝐹‘𝑧)) / ((𝐺‘𝑋) − (𝐺‘𝑧)))) “ (𝑣 ∩ ((𝐴(,)𝑋) ∖ {𝐴}))) ⊆ {𝑥 ∈ ℂ ∣ ¬
(abs‘(𝑥 − 𝐶)) ≤ 𝐸}))) |
| 520 | 397, 519 | mt3d 148 |
. 2
⊢ (𝜑 → (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) ≤ 𝐸) |
| 521 | 28 | recnd 11289 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 522 | 521 | mullidd 11279 |
. . 3
⊢ (𝜑 → (1 · 𝐸) = 𝐸) |
| 523 | | 1red 11262 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
| 524 | | 1lt2 12437 |
. . . . 5
⊢ 1 <
2 |
| 525 | 524 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 < 2) |
| 526 | 523, 30, 27, 525 | ltmul1dd 13132 |
. . 3
⊢ (𝜑 → (1 · 𝐸) < (2 · 𝐸)) |
| 527 | 522, 526 | eqbrtrrd 5167 |
. 2
⊢ (𝜑 → 𝐸 < (2 · 𝐸)) |
| 528 | 26, 28, 31, 520, 527 | lelttrd 11419 |
1
⊢ (𝜑 → (abs‘(((𝐹‘𝑋) / (𝐺‘𝑋)) − 𝐶)) < (2 · 𝐸)) |