Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1cnnc Structured version   Visualization version   GIF version

Theorem ftc1cnnc 35148
 Description: Choice-free proof of ftc1cn 24656. (Contributed by Brendan Leahy, 20-Nov-2017.)
Hypotheses
Ref Expression
ftc1cnnc.g 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
ftc1cnnc.a (𝜑𝐴 ∈ ℝ)
ftc1cnnc.b (𝜑𝐵 ∈ ℝ)
ftc1cnnc.le (𝜑𝐴𝐵)
ftc1cnnc.f (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
ftc1cnnc.i (𝜑𝐹 ∈ 𝐿1)
Assertion
Ref Expression
ftc1cnnc (𝜑 → (ℝ D 𝐺) = 𝐹)
Distinct variable groups:   𝑥,𝑡,𝐴   𝑥,𝐵,𝑡   𝑥,𝐹,𝑡   𝜑,𝑥,𝑡
Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1cnnc
Dummy variables 𝑦 𝑧 𝑠 𝑢 𝑣 𝑤 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvf 24520 . . . . 5 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
21a1i 11 . . . 4 (𝜑 → (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ)
32ffund 6492 . . 3 (𝜑 → Fun (ℝ D 𝐺))
4 ax-resscn 10586 . . . . . . 7 ℝ ⊆ ℂ
54a1i 11 . . . . . 6 (𝜑 → ℝ ⊆ ℂ)
6 ftc1cnnc.g . . . . . . 7 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
7 ftc1cnnc.a . . . . . . 7 (𝜑𝐴 ∈ ℝ)
8 ftc1cnnc.b . . . . . . 7 (𝜑𝐵 ∈ ℝ)
9 ftc1cnnc.le . . . . . . 7 (𝜑𝐴𝐵)
10 ssidd 3938 . . . . . . 7 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
11 ioossre 12789 . . . . . . . 8 (𝐴(,)𝐵) ⊆ ℝ
1211a1i 11 . . . . . . 7 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
13 ftc1cnnc.i . . . . . . 7 (𝜑𝐹 ∈ 𝐿1)
14 ftc1cnnc.f . . . . . . . 8 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
15 cncff 23508 . . . . . . . 8 (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
1614, 15syl 17 . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
176, 7, 8, 9, 10, 12, 13, 16ftc1lem2 24649 . . . . . 6 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
18 iccssre 12810 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
197, 8, 18syl2anc 587 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
20 eqid 2798 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
2120tgioo2 23418 . . . . . 6 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
225, 17, 19, 21, 20dvbssntr 24513 . . . . 5 (𝜑 → dom (ℝ D 𝐺) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
23 iccntr 23436 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
247, 8, 23syl2anc 587 . . . . 5 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
2522, 24sseqtrd 3955 . . . 4 (𝜑 → dom (ℝ D 𝐺) ⊆ (𝐴(,)𝐵))
26 retop 23377 . . . . . . . . . 10 (topGen‘ran (,)) ∈ Top
2721, 26eqeltrri 2887 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t ℝ) ∈ Top
2827a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t ℝ) ∈ Top)
2919adantr 484 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ)
30 iooretop 23381 . . . . . . . . . 10 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
3130, 21eleqtri 2888 . . . . . . . . 9 (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ)
3231a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ))
33 ioossicc 12814 . . . . . . . . 9 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
3433a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
35 uniretop 23378 . . . . . . . . . 10 ℝ = (topGen‘ran (,))
3621unieqi 4814 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
3735, 36eqtri 2821 . . . . . . . . 9 ℝ = ((TopOpen‘ℂfld) ↾t ℝ)
3837ssntr 21673 . . . . . . . 8 (((((TopOpen‘ℂfld) ↾t ℝ) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) ∧ ((𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ) ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)))
3928, 29, 32, 34, 38syl22anc 837 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)))
40 simpr 488 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵))
4139, 40sseldd 3916 . . . . . 6 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)))
4216ffvelrnda 6829 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐹𝑐) ∈ ℂ)
43 cnxmet 23388 . . . . . . . . . . . 12 (abs ∘ − ) ∈ (∞Met‘ℂ)
4411, 4sstri 3924 . . . . . . . . . . . 12 (𝐴(,)𝐵) ⊆ ℂ
45 xmetres2 22978 . . . . . . . . . . . 12 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)))
4643, 44, 45mp2an 691 . . . . . . . . . . 11 ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))
4746a1i 11 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)))
4843a1i 11 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → (abs ∘ − ) ∈ (∞Met‘ℂ))
49 ssid 3937 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
50 eqid 2798 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
5120cnfldtopon 23398 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
5251toponrestid 21536 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
5320, 50, 52cncfcn 23525 . . . . . . . . . . . . . . 15 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
5444, 49, 53mp2an 691 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
5514, 54eleqtrdi 2900 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
56 resttopon 21776 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
5751, 44, 56mp2an 691 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))
5857toponunii 21531 . . . . . . . . . . . . . . 15 (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
5958eleq2i 2881 . . . . . . . . . . . . . 14 (𝑐 ∈ (𝐴(,)𝐵) ↔ 𝑐 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
6059biimpi 219 . . . . . . . . . . . . 13 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
61 eqid 2798 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
6261cncnpi 21893 . . . . . . . . . . . . 13 ((𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ∧ 𝑐 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑐))
6355, 60, 62syl2an 598 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑐))
64 eqid 2798 . . . . . . . . . . . . . . . 16 ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) = ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))
6520cnfldtopn 23397 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
66 eqid 2798 . . . . . . . . . . . . . . . 16 (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) = (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))))
6764, 65, 66metrest 23141 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))))
6843, 44, 67mp2an 691 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))))
6968oveq1i 7146 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = ((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))
7069fveq1i 6647 . . . . . . . . . . . 12 ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑐) = (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐)
7163, 70eleqtrdi 2900 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐))
7271adantr 484 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝐹 ∈ (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐))
73 simpr 488 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
7466, 65metcnpi2 23162 . . . . . . . . . 10 (((((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ)) ∧ (𝐹 ∈ (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐) ∧ 𝑤 ∈ ℝ+)) → ∃𝑣 ∈ ℝ+𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤))
7547, 48, 72, 73, 74syl22anc 837 . . . . . . . . 9 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤))
76 simpr 488 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑢 ∈ (𝐴(,)𝐵))
77 simpllr 775 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵))
7876, 77ovresd 7297 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (𝑢(abs ∘ − )𝑐))
79 elioore 12759 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℝ)
8079recnd 10661 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℂ)
8144sseli 3911 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ)
8281ad3antlr 730 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ)
83 eqid 2798 . . . . . . . . . . . . . . . . . 18 (abs ∘ − ) = (abs ∘ − )
8483cnmetdval 23386 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢𝑐)))
8580, 82, 84syl2an2 685 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢𝑐)))
8678, 85eqtrd 2833 . . . . . . . . . . . . . . 15 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (abs‘(𝑢𝑐)))
8786breq1d 5041 . . . . . . . . . . . . . 14 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 ↔ (abs‘(𝑢𝑐)) < 𝑣))
8816ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
8988ffvelrnda 6829 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹𝑢) ∈ ℂ)
9042ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹𝑐) ∈ ℂ)
9183cnmetdval 23386 . . . . . . . . . . . . . . . 16 (((𝐹𝑢) ∈ ℂ ∧ (𝐹𝑐) ∈ ℂ) → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) = (abs‘((𝐹𝑢) − (𝐹𝑐))))
9289, 90, 91syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) = (abs‘((𝐹𝑢) − (𝐹𝑐))))
9392breq1d 5041 . . . . . . . . . . . . . 14 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤 ↔ (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))
9487, 93imbi12d 348 . . . . . . . . . . . . 13 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) ↔ ((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)))
9594ralbidva 3161 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → (∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) ↔ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)))
96 simprll 778 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}))
97 eldifsni 4683 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧𝑐)
9896, 97syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧𝑐)
9919ssdifssd 4070 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℝ)
10099sselda 3915 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → 𝑧 ∈ ℝ)
101100ad2ant2r 746 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))) → 𝑧 ∈ ℝ)
102101ad2ant2r 746 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧 ∈ ℝ)
103 elioore 12759 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℝ)
104103ad3antlr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑐 ∈ ℝ)
105102, 104lttri2d 10771 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (𝑧𝑐 ↔ (𝑧 < 𝑐𝑐 < 𝑧)))
106105biimpa 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧𝑐) → (𝑧 < 𝑐𝑐 < 𝑧))
107 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑧 → (𝐺𝑠) = (𝐺𝑧))
108107oveq1d 7151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑧 → ((𝐺𝑠) − (𝐺𝑐)) = ((𝐺𝑧) − (𝐺𝑐)))
109 oveq1 7143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑧 → (𝑠𝑐) = (𝑧𝑐))
110108, 109oveq12d 7154 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = 𝑧 → (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
111 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) = (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))
112 ovex 7169 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) ∈ V
113110, 111, 112fvmpt 6746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
114113ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
115114ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
11617ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝐺:(𝐴[,]𝐵)⟶ℂ)
117 eldifi 4054 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ∈ (𝐴[,]𝐵))
118117ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣) → 𝑧 ∈ (𝐴[,]𝐵))
119118ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ (𝐴[,]𝐵))
120116, 119ffvelrnd 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺𝑧) ∈ ℂ)
12133sseli 3911 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ (𝐴[,]𝐵))
12217ffvelrnda 6829 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ (𝐴[,]𝐵)) → (𝐺𝑐) ∈ ℂ)
123121, 122sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐺𝑐) ∈ ℂ)
124123ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺𝑐) ∈ ℂ)
125102adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℝ)
126125recnd 10661 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℂ)
12781ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑐 ∈ ℂ)
128 ltne 10729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑐𝑧)
129128necomd 3042 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑧𝑐)
130102, 129sylan 583 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧𝑐)
131120, 124, 126, 127, 130div2subd 11458 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) = (((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)))
132115, 131eqtrd 2833 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)))
133132fvoveq1d 7158 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)) − (𝐹𝑐))))
1347ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐴 ∈ ℝ)
1358ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐵 ∈ ℝ)
1369ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐴𝐵)
13714ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
13813ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐹 ∈ 𝐿1)
139 simpllr 775 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴(,)𝐵))
140 simplrl 776 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑤 ∈ ℝ+)
141 simplrr 777 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑣 ∈ ℝ+)
142 simprlr 779 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))
143 fvoveq1 7159 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = 𝑦 → (abs‘(𝑢𝑐)) = (abs‘(𝑦𝑐)))
144143breq1d 5041 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑦 → ((abs‘(𝑢𝑐)) < 𝑣 ↔ (abs‘(𝑦𝑐)) < 𝑣))
145144imbrov2fvoveq 7161 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑦 → (((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) ↔ ((abs‘(𝑦𝑐)) < 𝑣 → (abs‘((𝐹𝑦) − (𝐹𝑐))) < 𝑤)))
146145rspccva 3570 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦𝑐)) < 𝑣 → (abs‘((𝐹𝑦) − (𝐹𝑐))) < 𝑤))
147142, 146sylan 583 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦𝑐)) < 𝑣 → (abs‘((𝐹𝑦) − (𝐹𝑐))) < 𝑤))
14896, 117syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧 ∈ (𝐴[,]𝐵))
149 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(𝑧𝑐)) < 𝑣)
150121ad3antlr 730 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴[,]𝐵))
151103recnd 10661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ)
152151subidd 10977 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ (𝐴(,)𝐵) → (𝑐𝑐) = 0)
153152abs00bd 14646 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 ∈ (𝐴(,)𝐵) → (abs‘(𝑐𝑐)) = 0)
154153ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(𝑐𝑐)) = 0)
155141rpgt0d 12425 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 0 < 𝑣)
156154, 155eqbrtrd 5053 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(𝑐𝑐)) < 𝑣)
1576, 134, 135, 136, 137, 138, 139, 111, 140, 141, 147, 148, 149, 150, 156ftc1cnnclem 35147 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘((((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)) − (𝐹𝑐))) < 𝑤)
158133, 157eqbrtrd 5053 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
159113fvoveq1d 7158 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))))
160159ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))))
161160ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))))
1626, 134, 135, 136, 137, 138, 139, 111, 140, 141, 147, 150, 156, 148, 149ftc1cnnclem 35147 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))) < 𝑤)
163161, 162eqbrtrd 5053 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
164158, 163jaodan 955 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ (𝑧 < 𝑐𝑐 < 𝑧)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
165106, 164syldan 594 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
16698, 165mpdan 686 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
167166expr 460 . . . . . . . . . . . . . . 15 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))) → ((abs‘(𝑧𝑐)) < 𝑣 → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
168167adantld 494 . . . . . . . . . . . . . 14 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))) → ((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
169168expr 460 . . . . . . . . . . . . 13 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) → ((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
170169ralrimdva 3154 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → (∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
17195, 170sylbid 243 . . . . . . . . . . 11 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → (∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
172171anassrs 471 . . . . . . . . . 10 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) ∧ 𝑣 ∈ ℝ+) → (∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
173172reximdva 3233 . . . . . . . . 9 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → (∃𝑣 ∈ ℝ+𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) → ∃𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
17475, 173mpd 15 . . . . . . . 8 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
175174ralrimiva 3149 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ∀𝑤 ∈ ℝ+𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
17617adantr 484 . . . . . . . . . 10 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝐺:(𝐴[,]𝐵)⟶ℂ)
17719, 4sstrdi 3927 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
178177adantr 484 . . . . . . . . . 10 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℂ)
179121adantl 485 . . . . . . . . . 10 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴[,]𝐵))
180176, 178, 179dvlem 24509 . . . . . . . . 9 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)) ∈ ℂ)
181180fmpttd 6857 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))):((𝐴[,]𝐵) ∖ {𝑐})⟶ℂ)
182177ssdifssd 4070 . . . . . . . . 9 (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ)
183182adantr 484 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ)
18481adantl 485 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ)
185181, 183, 184ellimc3 24492 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐) ↔ ((𝐹𝑐) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))))
18642, 175, 185mpbir2and 712 . . . . . 6 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐))
187 eqid 2798 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t ℝ)
188187, 20, 111, 5, 17, 19eldv 24511 . . . . . . 7 (𝜑 → (𝑐(ℝ D 𝐺)(𝐹𝑐) ↔ (𝑐 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐))))
189188adantr 484 . . . . . 6 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝑐(ℝ D 𝐺)(𝐹𝑐) ↔ (𝑐 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐))))
19041, 186, 189mpbir2and 712 . . . . 5 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐(ℝ D 𝐺)(𝐹𝑐))
191 vex 3444 . . . . . 6 𝑐 ∈ V
192 fvex 6659 . . . . . 6 (𝐹𝑐) ∈ V
193191, 192breldm 5742 . . . . 5 (𝑐(ℝ D 𝐺)(𝐹𝑐) → 𝑐 ∈ dom (ℝ D 𝐺))
194190, 193syl 17 . . . 4 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ dom (ℝ D 𝐺))
19525, 194eqelssd 3936 . . 3 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
196 df-fn 6328 . . 3 ((ℝ D 𝐺) Fn (𝐴(,)𝐵) ↔ (Fun (ℝ D 𝐺) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)))
1973, 195, 196sylanbrc 586 . 2 (𝜑 → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
19816ffnd 6489 . 2 (𝜑𝐹 Fn (𝐴(,)𝐵))
1993adantr 484 . . 3 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → Fun (ℝ D 𝐺))
200 funbrfv 6692 . . 3 (Fun (ℝ D 𝐺) → (𝑐(ℝ D 𝐺)(𝐹𝑐) → ((ℝ D 𝐺)‘𝑐) = (𝐹𝑐)))
201199, 190, 200sylc 65 . 2 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑐) = (𝐹𝑐))
202197, 198, 201eqfnfvd 6783 1 (𝜑 → (ℝ D 𝐺) = 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ∖ cdif 3878   ⊆ wss 3881  {csn 4525  ∪ cuni 4801   class class class wbr 5031   ↦ cmpt 5111   × cxp 5518  dom cdm 5520  ran crn 5521   ↾ cres 5522   ∘ ccom 5524  Fun wfun 6319   Fn wfn 6320  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136  ℂcc 10527  ℝcr 10528  0cc0 10529   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℝ+crp 12380  (,)cioo 12729  [,]cicc 12732  abscabs 14588   ↾t crest 16689  TopOpenctopn 16690  topGenctg 16706  ∞Metcxmet 20080  MetOpencmopn 20085  ℂfldccnfld 20095  Topctop 21508  TopOnctopon 21525  intcnt 21632   Cn ccn 21839   CnP ccnp 21840  –cn→ccncf 23491  𝐿1cibl 24231  ∫citg 24232   limℂ climc 24475   D cdv 24476 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-symdif 4169  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-of 7391  df-ofr 7392  df-om 7564  df-1st 7674  df-2nd 7675  df-supp 7817  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-omul 8093  df-er 8275  df-map 8394  df-pm 8395  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8821  df-fi 8862  df-sup 8893  df-inf 8894  df-oi 8961  df-dju 9317  df-card 9355  df-acn 9358  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-4 11693  df-5 11694  df-6 11695  df-7 11696  df-8 11697  df-9 11698  df-n0 11889  df-z 11973  df-dec 12090  df-uz 12235  df-q 12340  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-ioo 12733  df-ico 12735  df-icc 12736  df-fz 12889  df-fzo 13032  df-fl 13160  df-mod 13236  df-seq 13368  df-exp 13429  df-hash 13690  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-rlim 14841  df-sum 15038  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21509  df-topon 21526  df-topsp 21548  df-bases 21561  df-cld 21634  df-ntr 21635  df-cls 21636  df-nei 21713  df-lp 21751  df-perf 21752  df-cn 21842  df-cnp 21843  df-haus 21930  df-cmp 22002  df-tx 22177  df-hmeo 22370  df-fil 22461  df-fm 22553  df-flim 22554  df-flf 22555  df-xms 22937  df-ms 22938  df-tms 22939  df-cncf 23493  df-ovol 24078  df-vol 24079  df-mbf 24233  df-itg1 24234  df-itg2 24235  df-ibl 24236  df-itg 24237  df-0p 24284  df-limc 24479  df-dv 24480 This theorem is referenced by:  ftc2nc  35158
 Copyright terms: Public domain W3C validator