| 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 26080 | . . 3
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) | 
| 14 | 5, 8 | sseldd 3983 | . . 3
⊢ (𝜑 → 𝐶 ∈ 𝐷) | 
| 15 | 13, 14 | ffvelcdmd 7104 | . 2
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) | 
| 16 |  | cnxmet 24794 | . . . . . 6
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 17 |  | ax-resscn 11213 | . . . . . . . 8
⊢ ℝ
⊆ ℂ | 
| 18 | 6, 17 | sstrdi 3995 | . . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ ℂ) | 
| 19 | 18 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐷 ⊆
ℂ) | 
| 20 |  | xmetres2 24372 | . . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝐷
× 𝐷)) ∈
(∞Met‘𝐷)) | 
| 21 | 16, 19, 20 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((abs
∘ − ) ↾ (𝐷 × 𝐷)) ∈ (∞Met‘𝐷)) | 
| 22 | 16 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) | 
| 23 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (𝐷 × 𝐷)) = ((abs ∘ − ) ↾ (𝐷 × 𝐷)) | 
| 24 | 12 | cnfldtopn 24803 | . . . . . . . . . . . 12
⊢ 𝐿 = (MetOpen‘(abs ∘
− )) | 
| 25 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝐷 × 𝐷))) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) | 
| 26 | 23, 24, 25 | metrest 24538 | . . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → (𝐿 ↾t 𝐷) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) | 
| 27 | 16, 18, 26 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (𝐿 ↾t 𝐷) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) | 
| 28 | 11, 27 | eqtrid 2788 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) | 
| 29 | 28 | oveq1d 7447 | . . . . . . . 8
⊢ (𝜑 → (𝐾 CnP 𝐿) = ((MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) CnP 𝐿)) | 
| 30 | 29 | fveq1d 6907 | . . . . . . 7
⊢ (𝜑 → ((𝐾 CnP 𝐿)‘𝐶) = (((MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) CnP 𝐿)‘𝐶)) | 
| 31 | 9, 30 | eleqtrd 2842 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) CnP 𝐿)‘𝐶)) | 
| 32 | 31 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐹 ∈ (((MetOpen‘((abs
∘ − ) ↾ (𝐷 × 𝐷))) CnP 𝐿)‘𝐶)) | 
| 33 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) | 
| 34 | 25, 24 | metcnpi2 24559 | . . . . 5
⊢ (((((abs
∘ − ) ↾ (𝐷 × 𝐷)) ∈ (∞Met‘𝐷) ∧ (abs ∘ − )
∈ (∞Met‘ℂ)) ∧ (𝐹 ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) CnP 𝐿)‘𝐶) ∧ 𝑤 ∈ ℝ+)) →
∃𝑣 ∈
ℝ+ ∀𝑦 ∈ 𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤)) | 
| 35 | 21, 22, 32, 33, 34 | syl22anc 838 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑦 ∈ 𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤)) | 
| 36 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) | 
| 37 | 14 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝐶 ∈ 𝐷) | 
| 38 | 36, 37 | ovresd 7601 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) = (𝑦(abs ∘ − )𝐶)) | 
| 39 | 18 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ 𝐷 ⊆
ℂ) | 
| 40 | 39 | sselda 3982 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ ℂ) | 
| 41 |  | iccssre 13470 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 42 | 2, 3, 41 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | 
| 43 | 42, 17 | sstrdi 3995 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) | 
| 44 |  | ioossicc 13474 | . . . . . . . . . . . . . . 15
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | 
| 45 | 44, 8 | sselid 3980 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) | 
| 46 | 43, 45 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 47 | 46 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → 𝐶 ∈ ℂ) | 
| 48 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 49 | 48 | cnmetdval 24792 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑦(abs ∘ − )𝐶) = (abs‘(𝑦 − 𝐶))) | 
| 50 | 40, 47, 49 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝑦(abs ∘ − )𝐶) = (abs‘(𝑦 − 𝐶))) | 
| 51 | 38, 50 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) = (abs‘(𝑦 − 𝐶))) | 
| 52 | 51 | breq1d 5152 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 ↔ (abs‘(𝑦 − 𝐶)) < 𝑣)) | 
| 53 | 13 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ 𝐹:𝐷⟶ℂ) | 
| 54 | 53 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℂ) | 
| 55 | 15 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (𝐹‘𝐶) ∈ ℂ) | 
| 56 | 48 | cnmetdval 24792 | . . . . . . . . . . 11
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) = (abs‘((𝐹‘𝑦) − (𝐹‘𝐶)))) | 
| 57 | 54, 55, 56 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) = (abs‘((𝐹‘𝑦) − (𝐹‘𝐶)))) | 
| 58 | 57 | breq1d 5152 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) | 
| 59 | 52, 58 | imbi12d 344 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑦 ∈ 𝐷) → (((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) ↔ ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) | 
| 60 | 59 | ralbidva 3175 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑦 ∈
𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) ↔ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) | 
| 61 |  | simprll 778 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) | 
| 62 |  | eldifsni 4789 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) → 𝑠 ≠ 𝐶) | 
| 63 | 61, 62 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑠 ≠ 𝐶) | 
| 64 | 2 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐴 ∈ ℝ) | 
| 65 | 3 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐵 ∈ ℝ) | 
| 66 | 4 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐴 ≤ 𝐵) | 
| 67 | 5 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → (𝐴(,)𝐵) ⊆ 𝐷) | 
| 68 | 6 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐷 ⊆ ℝ) | 
| 69 | 7 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐹 ∈
𝐿1) | 
| 70 | 8 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐶 ∈ (𝐴(,)𝐵)) | 
| 71 | 9 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) | 
| 72 |  | ftc1.h | . . . . . . . . . . . . 13
⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) | 
| 73 |  | simplrl 776 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑤 ∈ ℝ+) | 
| 74 |  | simplrr 777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑣 ∈ ℝ+) | 
| 75 |  | simprlr 779 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) | 
| 76 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑢 → (abs‘(𝑦 − 𝐶)) = (abs‘(𝑢 − 𝐶))) | 
| 77 | 76 | breq1d 5152 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → ((abs‘(𝑦 − 𝐶)) < 𝑣 ↔ (abs‘(𝑢 − 𝐶)) < 𝑣)) | 
| 78 | 77 | imbrov2fvoveq 7457 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → (((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) ↔ ((abs‘(𝑢 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝐶))) < 𝑤))) | 
| 79 | 78 | rspccva 3620 | . . . . . . . . . . . . . 14
⊢
((∀𝑦 ∈
𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) ∧ 𝑢 ∈ 𝐷) → ((abs‘(𝑢 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝐶))) < 𝑤)) | 
| 80 | 75, 79 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) ∧ 𝑢 ∈ 𝐷) → ((abs‘(𝑢 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑢) − (𝐹‘𝐶))) < 𝑤)) | 
| 81 | 61 | eldifad 3962 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 82 |  | simprr 772 | . . . . . . . . . . . . 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 26082 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) ∧ 𝑠 ≠ 𝐶) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤) | 
| 84 | 63, 83 | mpdan 687 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤)) ∧ (abs‘(𝑠 − 𝐶)) < 𝑣)) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤) | 
| 85 | 84 | expr 456 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) → ((abs‘(𝑠 − 𝐶)) < 𝑣 → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) | 
| 86 | 85 | adantld 490 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ∧ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤))) → ((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) | 
| 87 | 86 | expr 456 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
∧ 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) → ((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) | 
| 88 | 87 | ralrimdva 3153 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑦 ∈
𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑣 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝑤) → ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) | 
| 89 | 60, 88 | sylbid 240 | . . . . . 6
⊢ ((𝜑 ∧ (𝑤 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+))
→ (∀𝑦 ∈
𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) → ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) | 
| 90 | 89 | anassrs 467 | . . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑣 ∈ ℝ+)
→ (∀𝑦 ∈
𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) → ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) | 
| 91 | 90 | reximdva 3167 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(∃𝑣 ∈
ℝ+ ∀𝑦 ∈ 𝐷 ((𝑦((abs ∘ − ) ↾ (𝐷 × 𝐷))𝐶) < 𝑣 → ((𝐹‘𝑦)(abs ∘ − )(𝐹‘𝐶)) < 𝑤) → ∃𝑣 ∈ ℝ+ ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤))) | 
| 92 | 35, 91 | mpd 15 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) | 
| 93 | 92 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑣 ∈ ℝ+
∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)) | 
| 94 | 1, 2, 3, 4, 5, 6, 7, 13 | ftc1lem2 26078 | . . . . 5
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) | 
| 95 | 94, 43, 45 | dvlem 25932 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) | 
| 96 | 95, 72 | fmptd 7133 | . . 3
⊢ (𝜑 → 𝐻:((𝐴[,]𝐵) ∖ {𝐶})⟶ℂ) | 
| 97 | 43 | ssdifssd 4146 | . . 3
⊢ (𝜑 → ((𝐴[,]𝐵) ∖ {𝐶}) ⊆ ℂ) | 
| 98 | 96, 97, 46 | ellimc3 25915 | . 2
⊢ (𝜑 → ((𝐹‘𝐶) ∈ (𝐻 limℂ 𝐶) ↔ ((𝐹‘𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝐶})((𝑠 ≠ 𝐶 ∧ (abs‘(𝑠 − 𝐶)) < 𝑣) → (abs‘((𝐻‘𝑠) − (𝐹‘𝐶))) < 𝑤)))) | 
| 99 | 15, 93, 98 | mpbir2and 713 | 1
⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐻 limℂ 𝐶)) |