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

Theorem ftc1cnnc 33814
Description: Choice-free proof of ftc1cn 24042. (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 23907 . . . . 5 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
21a1i 11 . . . 4 (𝜑 → (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ)
32ffund 6269 . . 3 (𝜑 → Fun (ℝ D 𝐺))
4 ax-resscn 10287 . . . . . . 7 ℝ ⊆ ℂ
54a1i 11 . . . . . 6 (𝜑 → ℝ ⊆ ℂ)
6 ftc1cnnc.g . . . . . . 7 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
7 ftc1cnnc.a . . . . . . 7 (𝜑𝐴 ∈ ℝ)
8 ftc1cnnc.b . . . . . . 7 (𝜑𝐵 ∈ ℝ)
9 ftc1cnnc.le . . . . . . 7 (𝜑𝐴𝐵)
10 ssidd 3832 . . . . . . 7 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
11 ioossre 12472 . . . . . . . 8 (𝐴(,)𝐵) ⊆ ℝ
1211a1i 11 . . . . . . 7 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
13 ftc1cnnc.i . . . . . . 7 (𝜑𝐹 ∈ 𝐿1)
14 ftc1cnnc.f . . . . . . . 8 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
15 cncff 22929 . . . . . . . 8 (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
1614, 15syl 17 . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
176, 7, 8, 9, 10, 12, 13, 16ftc1lem2 24035 . . . . . 6 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
18 iccssre 12492 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
197, 8, 18syl2anc 575 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
20 eqid 2817 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
2120tgioo2 22839 . . . . . 6 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
225, 17, 19, 21, 20dvbssntr 23900 . . . . 5 (𝜑 → dom (ℝ D 𝐺) ⊆ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)))
23 iccntr 22857 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
247, 8, 23syl2anc 575 . . . . 5 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
2522, 24sseqtrd 3849 . . . 4 (𝜑 → dom (ℝ D 𝐺) ⊆ (𝐴(,)𝐵))
26 retop 22798 . . . . . . . . . 10 (topGen‘ran (,)) ∈ Top
2721, 26eqeltrri 2893 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t ℝ) ∈ Top
2827a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((TopOpen‘ℂfld) ↾t ℝ) ∈ Top)
2919adantr 468 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ)
30 iooretop 22802 . . . . . . . . . 10 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
3130, 21eleqtri 2894 . . . . . . . . 9 (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ)
3231a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ))
33 ioossicc 12496 . . . . . . . . 9 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
3433a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
35 uniretop 22799 . . . . . . . . . 10 ℝ = (topGen‘ran (,))
3621unieqi 4650 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
3735, 36eqtri 2839 . . . . . . . . 9 ℝ = ((TopOpen‘ℂfld) ↾t ℝ)
3837ssntr 21096 . . . . . . . 8 (((((TopOpen‘ℂfld) ↾t ℝ) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) ∧ ((𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ) ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)))
3928, 29, 32, 34, 38syl22anc 858 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)))
40 simpr 473 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵))
4139, 40sseldd 3810 . . . . . 6 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)))
4216ffvelrnda 6590 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐹𝑐) ∈ ℂ)
43 cnxmet 22809 . . . . . . . . . . . 12 (abs ∘ − ) ∈ (∞Met‘ℂ)
4411, 4sstri 3818 . . . . . . . . . . . 12 (𝐴(,)𝐵) ⊆ ℂ
45 xmetres2 22399 . . . . . . . . . . . 12 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)))
4643, 44, 45mp2an 675 . . . . . . . . . . 11 ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵))
4746a1i 11 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)))
4843a1i 11 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → (abs ∘ − ) ∈ (∞Met‘ℂ))
49 ssid 3831 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
50 eqid 2817 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
5120cnfldtopon 22819 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
5251toponrestid 20959 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
5320, 50, 52cncfcn 22945 . . . . . . . . . . . . . . 15 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
5444, 49, 53mp2an 675 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
5514, 54syl6eleq 2906 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
56 resttopon 21199 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
5751, 44, 56mp2an 675 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))
5857toponunii 20954 . . . . . . . . . . . . . . 15 (𝐴(,)𝐵) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
5958eleq2i 2888 . . . . . . . . . . . . . 14 (𝑐 ∈ (𝐴(,)𝐵) ↔ 𝑐 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
6059biimpi 207 . . . . . . . . . . . . 13 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
61 eqid 2817 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
6261cncnpi 21316 . . . . . . . . . . . . 13 ((𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ∧ 𝑐 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑐))
6355, 60, 62syl2an 585 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑐))
64 eqid 2817 . . . . . . . . . . . . . . . 16 ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) = ((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))
6520cnfldtopn 22818 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
66 eqid 2817 . . . . . . . . . . . . . . . 16 (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) = (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))))
6764, 65, 66metrest 22562 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))))
6843, 44, 67mp2an 675 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))))
6968oveq1i 6893 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = ((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))
7069fveq1i 6418 . . . . . . . . . . . 12 ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑐) = (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐)
7163, 70syl6eleq 2906 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝐹 ∈ (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐))
7271adantr 468 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝐹 ∈ (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐))
73 simpr 473 . . . . . . . . . 10 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
7466, 65metcnpi2 22583 . . . . . . . . . 10 (((((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵))) ∈ (∞Met‘(𝐴(,)𝐵)) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ)) ∧ (𝐹 ∈ (((MetOpen‘((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))) CnP (TopOpen‘ℂfld))‘𝑐) ∧ 𝑤 ∈ ℝ+)) → ∃𝑣 ∈ ℝ+𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤))
7547, 48, 72, 73, 74syl22anc 858 . . . . . . . . 9 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤))
76 simpr 473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑢 ∈ (𝐴(,)𝐵))
77 simpllr 784 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴(,)𝐵))
7876, 77ovresd 7040 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (𝑢(abs ∘ − )𝑐))
79 elioore 12442 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℝ)
8079recnd 10362 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ ℂ)
8144sseli 3805 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ)
8281ad3antlr 713 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ)
83 eqid 2817 . . . . . . . . . . . . . . . . . 18 (abs ∘ − ) = (abs ∘ − )
8483cnmetdval 22807 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢𝑐)))
8580, 82, 84syl2an2 669 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢(abs ∘ − )𝑐) = (abs‘(𝑢𝑐)))
8678, 85eqtrd 2851 . . . . . . . . . . . . . . 15 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) = (abs‘(𝑢𝑐)))
8786breq1d 4865 . . . . . . . . . . . . . 14 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 ↔ (abs‘(𝑢𝑐)) < 𝑣))
8816ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
8988ffvelrnda 6590 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹𝑢) ∈ ℂ)
9042ad2antrr 708 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹𝑐) ∈ ℂ)
9183cnmetdval 22807 . . . . . . . . . . . . . . . 16 (((𝐹𝑢) ∈ ℂ ∧ (𝐹𝑐) ∈ ℂ) → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) = (abs‘((𝐹𝑢) − (𝐹𝑐))))
9289, 90, 91syl2anc 575 . . . . . . . . . . . . . . 15 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) = (abs‘((𝐹𝑢) − (𝐹𝑐))))
9392breq1d 4865 . . . . . . . . . . . . . 14 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤 ↔ (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))
9487, 93imbi12d 335 . . . . . . . . . . . . 13 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) ↔ ((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)))
9594ralbidva 3184 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → (∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) ↔ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)))
96 simprll 788 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}))
97 eldifsni 4523 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧𝑐)
9896, 97syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧𝑐)
9919ssdifssd 3958 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℝ)
10099sselda 3809 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → 𝑧 ∈ ℝ)
101100ad2ant2r 744 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))) → 𝑧 ∈ ℝ)
102101ad2ant2r 744 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧 ∈ ℝ)
103 elioore 12442 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℝ)
104103ad3antlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑐 ∈ ℝ)
105102, 104lttri2d 10470 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (𝑧𝑐 ↔ (𝑧 < 𝑐𝑐 < 𝑧)))
106105biimpa 464 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧𝑐) → (𝑧 < 𝑐𝑐 < 𝑧))
107 fveq2 6417 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑧 → (𝐺𝑠) = (𝐺𝑧))
108107oveq1d 6898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑧 → ((𝐺𝑠) − (𝐺𝑐)) = ((𝐺𝑧) − (𝐺𝑐)))
109 oveq1 6890 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑧 → (𝑠𝑐) = (𝑧𝑐))
110108, 109oveq12d 6901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = 𝑧 → (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
111 eqid 2817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) = (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))
112 ovex 6915 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) ∈ V
113110, 111, 112fvmpt 6512 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
114113ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
115114ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)))
11617ad4antr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝐺:(𝐴[,]𝐵)⟶ℂ)
117 eldifi 3942 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → 𝑧 ∈ (𝐴[,]𝐵))
118117ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣) → 𝑧 ∈ (𝐴[,]𝐵))
119118ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ (𝐴[,]𝐵))
120116, 119ffvelrnd 6591 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺𝑧) ∈ ℂ)
12133sseli 3805 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ (𝐴[,]𝐵))
12217ffvelrnda 6590 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ (𝐴[,]𝐵)) → (𝐺𝑐) ∈ ℂ)
123121, 122sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐺𝑐) ∈ ℂ)
124123ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (𝐺𝑐) ∈ ℂ)
125102adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℝ)
126125recnd 10362 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧 ∈ ℂ)
12781ad4antlr 717 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑐 ∈ ℂ)
128 ltne 10428 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑐𝑧)
129128necomd 3044 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℝ ∧ 𝑧 < 𝑐) → 𝑧𝑐)
130102, 129sylan 571 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → 𝑧𝑐)
131120, 124, 126, 127, 130div2subd 11145 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) = (((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)))
132115, 131eqtrd 2851 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) = (((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)))
133132fvoveq1d 6905 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)) − (𝐹𝑐))))
1347ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐴 ∈ ℝ)
1358ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐵 ∈ ℝ)
1369ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐴𝐵)
13714ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
13813ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝐹 ∈ 𝐿1)
139 simpllr 784 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴(,)𝐵))
140 simplrl 786 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑤 ∈ ℝ+)
141 simplrr 787 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑣 ∈ ℝ+)
142 simprlr 789 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))
143 fvoveq1 6906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = 𝑦 → (abs‘(𝑢𝑐)) = (abs‘(𝑦𝑐)))
144143breq1d 4865 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑦 → ((abs‘(𝑢𝑐)) < 𝑣 ↔ (abs‘(𝑦𝑐)) < 𝑣))
145144imbrov2fvoveq 6908 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑦 → (((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) ↔ ((abs‘(𝑦𝑐)) < 𝑣 → (abs‘((𝐹𝑦) − (𝐹𝑐))) < 𝑤)))
146145rspccva 3512 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦𝑐)) < 𝑣 → (abs‘((𝐹𝑦) − (𝐹𝑐))) < 𝑤))
147142, 146sylan 571 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦𝑐)) < 𝑣 → (abs‘((𝐹𝑦) − (𝐹𝑐))) < 𝑤))
14896, 117syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑧 ∈ (𝐴[,]𝐵))
149 simprr 780 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(𝑧𝑐)) < 𝑣)
150121ad3antlr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 𝑐 ∈ (𝐴[,]𝐵))
151103recnd 10362 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 ∈ (𝐴(,)𝐵) → 𝑐 ∈ ℂ)
152151subidd 10674 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ (𝐴(,)𝐵) → (𝑐𝑐) = 0)
153152abs00bd 14273 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 ∈ (𝐴(,)𝐵) → (abs‘(𝑐𝑐)) = 0)
154153ad3antlr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(𝑐𝑐)) = 0)
155141rpgt0d 12108 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → 0 < 𝑣)
156154, 155eqbrtrd 4877 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(𝑐𝑐)) < 𝑣)
1576, 134, 135, 136, 137, 138, 139, 111, 140, 141, 147, 148, 149, 150, 156ftc1cnnclem 33813 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘((((𝐺𝑐) − (𝐺𝑧)) / (𝑐𝑧)) − (𝐹𝑐))) < 𝑤)
158133, 157eqbrtrd 4877 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧 < 𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
159113fvoveq1d 6905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))))
160159ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))))
161160ad2antlr 709 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) = (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))))
1626, 134, 135, 136, 137, 138, 139, 111, 140, 141, 147, 150, 156, 148, 149ftc1cnnclem 33813 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘((((𝐺𝑧) − (𝐺𝑐)) / (𝑧𝑐)) − (𝐹𝑐))) < 𝑤)
163161, 162eqbrtrd 4877 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑐 < 𝑧) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
164158, 163jaodan 971 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ (𝑧 < 𝑐𝑐 < 𝑧)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
165106, 164syldan 581 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) ∧ 𝑧𝑐) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
16698, 165mpdan 670 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ ((𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤)) ∧ (abs‘(𝑧𝑐)) < 𝑣)) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)
167166expr 446 . . . . . . . . . . . . . . 15 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))) → ((abs‘(𝑧𝑐)) < 𝑣 → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
168167adantld 480 . . . . . . . . . . . . . 14 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ∧ ∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤))) → ((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
169168expr 446 . . . . . . . . . . . . 13 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) ∧ 𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) → ((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
170169ralrimdva 3168 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → (∀𝑢 ∈ (𝐴(,)𝐵)((abs‘(𝑢𝑐)) < 𝑣 → (abs‘((𝐹𝑢) − (𝐹𝑐))) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
17195, 170sylbid 231 . . . . . . . . . . 11 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ (𝑤 ∈ ℝ+𝑣 ∈ ℝ+)) → (∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
172171anassrs 455 . . . . . . . . . 10 ((((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) ∧ 𝑣 ∈ ℝ+) → (∀𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) → ∀𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
173172reximdva 3215 . . . . . . . . 9 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → (∃𝑣 ∈ ℝ+𝑢 ∈ (𝐴(,)𝐵)((𝑢((abs ∘ − ) ↾ ((𝐴(,)𝐵) × (𝐴(,)𝐵)))𝑐) < 𝑣 → ((𝐹𝑢)(abs ∘ − )(𝐹𝑐)) < 𝑤) → ∃𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤)))
17475, 173mpd 15 . . . . . . . 8 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑤 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
175174ralrimiva 3165 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ∀𝑤 ∈ ℝ+𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))
17617adantr 468 . . . . . . . . . 10 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝐺:(𝐴[,]𝐵)⟶ℂ)
17719, 4syl6ss 3821 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
178177adantr 468 . . . . . . . . . 10 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℂ)
179121adantl 469 . . . . . . . . . 10 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ (𝐴[,]𝐵))
180176, 178, 179dvlem 23896 . . . . . . . . 9 (((𝜑𝑐 ∈ (𝐴(,)𝐵)) ∧ 𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐})) → (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)) ∈ ℂ)
181180fmpttd 6616 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))):((𝐴[,]𝐵) ∖ {𝑐})⟶ℂ)
182177ssdifssd 3958 . . . . . . . . 9 (𝜑 → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ)
183182adantr 468 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((𝐴[,]𝐵) ∖ {𝑐}) ⊆ ℂ)
18481adantl 469 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ ℂ)
185181, 183, 184ellimc3 23879 . . . . . . 7 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐) ↔ ((𝐹𝑐) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑣 ∈ ℝ+𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐})((𝑧𝑐 ∧ (abs‘(𝑧𝑐)) < 𝑣) → (abs‘(((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐)))‘𝑧) − (𝐹𝑐))) < 𝑤))))
18642, 175, 185mpbir2and 695 . . . . . 6 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐))
187 eqid 2817 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t ℝ)
188187, 20, 111, 5, 17, 19eldv 23898 . . . . . . 7 (𝜑 → (𝑐(ℝ D 𝐺)(𝐹𝑐) ↔ (𝑐 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐))))
189188adantr 468 . . . . . 6 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → (𝑐(ℝ D 𝐺)(𝐹𝑐) ↔ (𝑐 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘(𝐴[,]𝐵)) ∧ (𝐹𝑐) ∈ ((𝑠 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺𝑠) − (𝐺𝑐)) / (𝑠𝑐))) lim 𝑐))))
19041, 186, 189mpbir2and 695 . . . . 5 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐(ℝ D 𝐺)(𝐹𝑐))
191 vex 3405 . . . . . 6 𝑐 ∈ V
192 fvex 6430 . . . . . 6 (𝐹𝑐) ∈ V
193191, 192breldm 5543 . . . . 5 (𝑐(ℝ D 𝐺)(𝐹𝑐) → 𝑐 ∈ dom (ℝ D 𝐺))
194190, 193syl 17 . . . 4 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ dom (ℝ D 𝐺))
19525, 194eqelssd 3830 . . 3 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
196 df-fn 6113 . . 3 ((ℝ D 𝐺) Fn (𝐴(,)𝐵) ↔ (Fun (ℝ D 𝐺) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)))
1973, 195, 196sylanbrc 574 . 2 (𝜑 → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
19816ffnd 6266 . 2 (𝜑𝐹 Fn (𝐴(,)𝐵))
1993adantr 468 . . 3 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → Fun (ℝ D 𝐺))
200 funbrfv 6463 . . 3 (Fun (ℝ D 𝐺) → (𝑐(ℝ D 𝐺)(𝐹𝑐) → ((ℝ D 𝐺)‘𝑐) = (𝐹𝑐)))
201199, 190, 200sylc 65 . 2 ((𝜑𝑐 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑐) = (𝐹𝑐))
202197, 198, 201eqfnfvd 6545 1 (𝜑 → (ℝ D 𝐺) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2157  wne 2989  wral 3107  wrex 3108  cdif 3777  wss 3780  {csn 4381   cuni 4641   class class class wbr 4855  cmpt 4934   × cxp 5322  dom cdm 5324  ran crn 5325  cres 5326  ccom 5328  Fun wfun 6104   Fn wfn 6105  wf 6106  cfv 6110  (class class class)co 6883  cc 10228  cr 10229  0cc0 10230   < clt 10368  cle 10369  cmin 10560   / cdiv 10978  +crp 12065  (,)cioo 12412  [,]cicc 12415  abscabs 14216  t crest 16305  TopOpenctopn 16306  topGenctg 16322  ∞Metcxmt 19958  MetOpencmopn 19963  fldccnfld 19973  Topctop 20931  TopOnctopon 20948  intcnt 21055   Cn ccn 21262   CnP ccnp 21263  cnccncf 22912  𝐿1cibl 23620  citg 23621   lim climc 23862   D cdv 23863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188  ax-inf2 8794  ax-cnex 10286  ax-resscn 10287  ax-1cn 10288  ax-icn 10289  ax-addcl 10290  ax-addrcl 10291  ax-mulcl 10292  ax-mulrcl 10293  ax-mulcom 10294  ax-addass 10295  ax-mulass 10296  ax-distr 10297  ax-i2m1 10298  ax-1ne0 10299  ax-1rid 10300  ax-rnegex 10301  ax-rrecex 10302  ax-cnre 10303  ax-pre-lttri 10304  ax-pre-lttrn 10305  ax-pre-ltadd 10306  ax-pre-mulgt0 10307  ax-pre-sup 10308  ax-addf 10309  ax-mulf 10310
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-symdif 4053  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-disj 4824  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5906  df-ord 5952  df-on 5953  df-lim 5954  df-suc 5955  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-isom 6119  df-riota 6844  df-ov 6886  df-oprab 6887  df-mpt2 6888  df-of 7136  df-ofr 7137  df-om 7305  df-1st 7407  df-2nd 7408  df-supp 7539  df-wrecs 7651  df-recs 7713  df-rdg 7751  df-1o 7805  df-2o 7806  df-oadd 7809  df-omul 7810  df-er 7988  df-map 8103  df-pm 8104  df-ixp 8155  df-en 8202  df-dom 8203  df-sdom 8204  df-fin 8205  df-fsupp 8524  df-fi 8565  df-sup 8596  df-inf 8597  df-oi 8663  df-card 9057  df-acn 9060  df-cda 9284  df-pnf 10370  df-mnf 10371  df-xr 10372  df-ltxr 10373  df-le 10374  df-sub 10562  df-neg 10563  df-div 10979  df-nn 11315  df-2 11375  df-3 11376  df-4 11377  df-5 11378  df-6 11379  df-7 11380  df-8 11381  df-9 11382  df-n0 11579  df-z 11663  df-dec 11779  df-uz 11924  df-q 12027  df-rp 12066  df-xneg 12181  df-xadd 12182  df-xmul 12183  df-ioo 12416  df-ico 12418  df-icc 12419  df-fz 12569  df-fzo 12709  df-fl 12836  df-mod 12912  df-seq 13044  df-exp 13103  df-hash 13357  df-cj 14081  df-re 14082  df-im 14083  df-sqrt 14217  df-abs 14218  df-clim 14461  df-rlim 14462  df-sum 14659  df-struct 16089  df-ndx 16090  df-slot 16091  df-base 16093  df-sets 16094  df-ress 16095  df-plusg 16185  df-mulr 16186  df-starv 16187  df-sca 16188  df-vsca 16189  df-ip 16190  df-tset 16191  df-ple 16192  df-ds 16194  df-unif 16195  df-hom 16196  df-cco 16197  df-rest 16307  df-topn 16308  df-0g 16326  df-gsum 16327  df-topgen 16328  df-pt 16329  df-prds 16332  df-xrs 16386  df-qtop 16391  df-imas 16392  df-xps 16394  df-mre 16470  df-mrc 16471  df-acs 16473  df-mgm 17466  df-sgrp 17508  df-mnd 17519  df-submnd 17560  df-mulg 17765  df-cntz 17970  df-cmn 18415  df-psmet 19965  df-xmet 19966  df-met 19967  df-bl 19968  df-mopn 19969  df-fbas 19970  df-fg 19971  df-cnfld 19974  df-top 20932  df-topon 20949  df-topsp 20971  df-bases 20984  df-cld 21057  df-ntr 21058  df-cls 21059  df-nei 21136  df-lp 21174  df-perf 21175  df-cn 21265  df-cnp 21266  df-haus 21353  df-cmp 21424  df-tx 21599  df-hmeo 21792  df-fil 21883  df-fm 21975  df-flim 21976  df-flf 21977  df-xms 22358  df-ms 22359  df-tms 22360  df-cncf 22914  df-ovol 23467  df-vol 23468  df-mbf 23622  df-itg1 23623  df-itg2 23624  df-ibl 23625  df-itg 23626  df-0p 23673  df-limc 23866  df-dv 23867
This theorem is referenced by:  ftc2nc  33824
  Copyright terms: Public domain W3C validator