Step | Hyp | Ref
| Expression |
1 | | ftc1.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
2 | | ftc1.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | | ftc1.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | | ftc1.le |
. . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
5 | | ftc1.s |
. . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
6 | | ftc1.d |
. . . 4
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
7 | | ftc1.i |
. . . 4
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
8 | | ftc1.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) |
9 | | ftc1.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) |
10 | | ftc1.j |
. . . 4
⊢ 𝐽 = (𝐿 ↾t
ℝ) |
11 | | ftc1.k |
. . . 4
⊢ 𝐾 = (𝐿 ↾t 𝐷) |
12 | | ftc1.l |
. . . 4
⊢ 𝐿 =
(TopOpen‘ℂfld) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | ftc1lem3 25200 |
. . 3
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
14 | 5, 8 | sseldd 3927 |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝐷) |
15 | 13, 14 | ffvelrnd 6959 |
. 2
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
16 | | cnxmet 23934 |
. . . . . 6
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
17 | | ax-resscn 10929 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
18 | 6, 17 | sstrdi 3938 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ ℂ) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐷 ⊆
ℂ) |
20 | | xmetres2 23512 |
. . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝐷
× 𝐷)) ∈
(∞Met‘𝐷)) |
21 | 16, 19, 20 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((abs
∘ − ) ↾ (𝐷 × 𝐷)) ∈ (∞Met‘𝐷)) |
22 | 16 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
23 | | eqid 2740 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (𝐷 × 𝐷)) = ((abs ∘ − ) ↾ (𝐷 × 𝐷)) |
24 | 12 | cnfldtopn 23943 |
. . . . . . . . . . . 12
⊢ 𝐿 = (MetOpen‘(abs ∘
− )) |
25 | | eqid 2740 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝐷 × 𝐷))) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) |
26 | 23, 24, 25 | metrest 23678 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → (𝐿 ↾t 𝐷) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) |
27 | 16, 18, 26 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 ↾t 𝐷) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) |
28 | 11, 27 | eqtrid 2792 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) |
29 | 28 | oveq1d 7286 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 CnP 𝐿) = ((MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) CnP 𝐿)) |
30 | 29 | fveq1d 6773 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 CnP 𝐿)‘𝐶) = (((MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) CnP 𝐿)‘𝐶)) |
31 | 9, 30 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) CnP 𝐿)‘𝐶)) |
32 | 31 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐹 ∈ (((MetOpen‘((abs
∘ − ) ↾ (𝐷 × 𝐷))) CnP 𝐿)‘𝐶)) |
33 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
34 | 25, 24 | metcnpi2 23699 |
. . . . 5
⊢ (((((abs
∘ − ) ↾ (𝐷 × 𝐷)) ∈ (∞Met‘𝐷) ∧ (abs ∘ − )
∈ (∞Met‘ℂ)) ∧ (𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) CnP 𝐿)‘𝐶) ∧ 𝑤 ∈ ℝ+)) →
∃𝑣 ∈
ℝ+ ∀𝑦 ∈ 𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤)) |
35 | 21, 22, 32, 33, 34 | syl22anc 836 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑦 ∈ 𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤)) |
36 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
37 | 14 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝐶 ∈ 𝐷) |
38 | 36, 37 | ovresd 7433 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) = (𝑦(abs ∘ − )𝐶)) |
39 | 18 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ 𝐷 ⊆
ℂ) |
40 | 39 | sselda 3926 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ ℂ) |
41 | | iccssre 13160 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
42 | 2, 3, 41 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
43 | 42, 17 | sstrdi 3938 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
44 | | ioossicc 13164 |
. . . . . . . . . . . . . . 15
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
45 | 44, 8 | sselid 3924 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) |
46 | 43, 45 | sseldd 3927 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℂ) |
47 | 46 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝐶 ∈ ℂ) |
48 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ) = (abs ∘ − ) |
49 | 48 | cnmetdval 23932 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑦(abs ∘ − )𝐶) = (abs‘(𝑦 − 𝐶))) |
50 | 40, 47, 49 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝑦(abs ∘ − )𝐶) = (abs‘(𝑦 − 𝐶))) |
51 | 38, 50 | eqtrd 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) = (abs‘(𝑦 − 𝐶))) |
52 | 51 | breq1d 5089 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 ↔ (abs‘(𝑦 − 𝐶)) < 𝑣)) |
53 | 13 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ 𝐹:𝐷⟶ℂ) |
54 | 53 | ffvelrnda 6958 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℂ) |
55 | 15 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝐹‘𝐶) ∈ ℂ) |
56 | 48 | cnmetdval 23932 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) = (abs‘((𝐹‘𝑦) − (𝐹‘𝐶)))) |
57 | 54, 55, 56 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) = (abs‘((𝐹‘𝑦) − (𝐹‘𝐶)))) |
58 | 57 | breq1d 5089 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) |
59 | 52, 58 | imbi12d 345 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) ↔ ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) |
60 | 59 | ralbidva 3122 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑦 ∈
𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) ↔ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) |
61 | | simprll 776 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) |
62 | | eldifsni 4729 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) → 𝑠 ≠ 𝐶) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑠 ≠ 𝐶) |
64 | 2 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐴 ∈ ℝ) |
65 | 3 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐵 ∈ ℝ) |
66 | 4 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐴 ≤ 𝐵) |
67 | 5 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → (𝐴(,)𝐵) ⊆ 𝐷) |
68 | 6 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐷 ⊆ ℝ) |
69 | 7 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐹 ∈
𝐿1) |
70 | 8 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐶 ∈ (𝐴(,)𝐵)) |
71 | 9 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) |
72 | | ftc1.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
73 | | simplrl 774 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑤 ∈ ℝ+) |
74 | | simplrr 775 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑣 ∈ ℝ+) |
75 | | simprlr 777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) |
76 | | fvoveq1 7294 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑢 → (abs‘(𝑦 − 𝐶)) = (abs‘(𝑢 − 𝐶))) |
77 | 76 | breq1d 5089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → ((abs‘(𝑦 − 𝐶)) < 𝑣 ↔ (abs‘(𝑢 − 𝐶)) < 𝑣)) |
78 | 77 | imbrov2fvoveq 7296 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → (((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) ↔ ((abs‘(𝑢 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝐶))) < 𝑤))) |
79 | 78 | rspccva 3560 |
. . . . . . . . . . . . . 14
⊢
((∀𝑦 ∈
𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) ∧ 𝑢 ∈ 𝐷) → ((abs‘(𝑢 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝐶))) < 𝑤)) |
80 | 75, 79 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) ∧ 𝑢 ∈ 𝐷) → ((abs‘(𝑢 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝐶))) < 𝑤)) |
81 | 61 | eldifad 3904 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑠 ∈ (𝐴[,]𝐵)) |
82 | | simprr 770 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → (abs‘(𝑠 − 𝐶)) < 𝑣) |
83 | 1, 64, 65, 66, 67, 68, 69, 70, 71, 10, 11, 12, 72, 73, 74, 80, 81, 82 | ftc1lem5 25202 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) ∧ 𝑠 ≠ 𝐶) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤) |
84 | 63, 83 | mpdan 684 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤) |
85 | 84 | expr 457 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) → ((abs‘(𝑠 − 𝐶)) < 𝑣 → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) |
86 | 85 | adantld 491 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) → ((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) |
87 | 86 | expr 457 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) → ((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) |
88 | 87 | ralrimdva 3115 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑦 ∈
𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) → ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) |
89 | 60, 88 | sylbid 239 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑦 ∈
𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) → ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) |
90 | 89 | anassrs 468 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑣 ∈ ℝ+)
→ (∀𝑦 ∈
𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) → ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) |
91 | 90 | reximdva 3205 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(∃𝑣 ∈
ℝ+ ∀𝑦 ∈ 𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) → ∃𝑣 ∈ ℝ+ ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) |
92 | 35, 91 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) |
93 | 92 | ralrimiva 3110 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑣 ∈ ℝ+
∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) |
94 | 1, 2, 3, 4, 5, 6, 7, 13 | ftc1lem2 25198 |
. . . . 5
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
95 | 94, 43, 45 | dvlem 25058 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
96 | 95, 72 | fmptd 6985 |
. . 3
⊢ (𝜑 → 𝐻:((𝐴[,]𝐵) ∖ {𝐶})⟶ℂ) |
97 | 43 | ssdifssd 4082 |
. . 3
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝐶}) ⊆ ℂ) |
98 | 96, 97, 46 | ellimc3 25041 |
. 2
⊢ (𝜑 → ((𝐹‘𝐶) ∈ (𝐻 limℂ 𝐶) ↔ ((𝐹‘𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)))) |
99 | 15, 93, 98 | mpbir2and 710 |
1
⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐻 limℂ 𝐶)) |