ioodvbdlimc1

Description: A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Proof shortened by AV, 3-Oct-2020)

	Ref	Expression
Hypotheses	ioodvbdlimc1.a	$⊢ φ \to A \in ℝ$
	ioodvbdlimc1.b	$⊢ φ \to B \in ℝ$
	ioodvbdlimc1.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	ioodvbdlimc1.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	ioodvbdlimc1.dvbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
Assertion	ioodvbdlimc1	$⊢ φ \to F {lim}_{ℂ} A \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ioodvbdlimc1.a	$⊢ φ \to A \in ℝ$
2		ioodvbdlimc1.b	$⊢ φ \to B \in ℝ$
3		ioodvbdlimc1.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
4		ioodvbdlimc1.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
5		ioodvbdlimc1.dvbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
6	1	adantr	$⊢ (φ \land A < B) \to A \in ℝ$
7	2	adantr	$⊢ (φ \land A < B) \to B \in ℝ$
8		simpr	$⊢ (φ \land A < B) \to A < B$
9	3	adantr	$⊢ (φ \land A < B) \to F : (A, B) ⟶ ℝ$
10	4	adantr	$⊢ (φ \land A < B) \to dom F_{ℝ}^{'} = (A, B)$
11	5	adantr	$⊢ (φ \land A < B) \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
12		2fveq3	$⊢ y = x \to \|F_{ℝ}^{'} (y)\| = \|F_{ℝ}^{'} (x)\|$
13	12	cbvmptv	$⊢ (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) = (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|)$
14	13	rneqi	$⊢ ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) = ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|)$
15	14	supeq1i	$⊢ sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <) = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
16		eqid	$⊢ ⌊\frac{1}{B - A}⌋ + 1 = ⌊\frac{1}{B - A}⌋ + 1$
17		oveq2	$⊢ j = k \to \frac{1}{j} = \frac{1}{k}$
18	17	oveq2d	$⊢ j = k \to A + (\frac{1}{j}) = A + (\frac{1}{k})$
19	18	fveq2d	$⊢ j = k \to F (A + (\frac{1}{j})) = F (A + (\frac{1}{k}))$
20	19	cbvmptv	$⊢ (j \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ F (A + (\frac{1}{j}))) = (k \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ F (A + (\frac{1}{k})))$
21	18	cbvmptv	$⊢ (j \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ A + (\frac{1}{j})) = (k \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ A + (\frac{1}{k}))$
22		eqid	$⊢ if (⌊\frac{1}{B - A}⌋ + 1 \leq ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{1}{B - A}⌋ + 1) = if (⌊\frac{1}{B - A}⌋ + 1 \leq ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{1}{B - A}⌋ + 1)$
23		biid	$⊢ ((((((φ \land A < B) \land x \in ℝ^{+}) \land k \in ℤ_{\geq if (⌊\frac{1}{B - A}⌋ + 1 \leq ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{1}{B - A}⌋ + 1)}) \land \|(j \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ F (A + (\frac{1}{j}))) (k) - lim sup ((j \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ F (A + (\frac{1}{j}))))\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - A\| < \frac{1}{k}) \leftrightarrow ((((((φ \land A < B) \land x \in ℝ^{+}) \land k \in ℤ_{\geq if (⌊\frac{1}{B - A}⌋ + 1 \leq ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{sup (ran (y \in (A, B) ⟼ \|F_{ℝ}^{'} (y)\|) ℝ <)}{\frac{x}{2}}⌋ + 1, ⌊\frac{1}{B - A}⌋ + 1)}) \land \|(j \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ F (A + (\frac{1}{j}))) (k) - lim sup ((j \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ F (A + (\frac{1}{j}))))\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - A\| < \frac{1}{k})$
24	6 7 8 9 10 11 15 16 20 21 22 23	ioodvbdlimc1lem2	$⊢ (φ \land A < B) \to lim sup ((j \in ℤ_{\geq (⌊\frac{1}{B - A}⌋ + 1)} ⟼ F (A + (\frac{1}{j})))) \in (F {lim}_{ℂ} A)$
25	24	ne0d	$⊢ (φ \land A < B) \to F {lim}_{ℂ} A \neq \emptyset$
26		ax-resscn	$⊢ ℝ \subseteq ℂ$
27	26	a1i	$⊢ φ \to ℝ \subseteq ℂ$
28	3 27	fssd	$⊢ φ \to F : (A, B) ⟶ ℂ$
29	28	adantr	$⊢ (φ \land B \leq A) \to F : (A, B) ⟶ ℂ$
30		simpr	$⊢ (φ \land B \leq A) \to B \leq A$
31	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
32	31	adantr	$⊢ (φ \land B \leq A) \to A \in ℝ^{*}$
33	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
34	33	adantr	$⊢ (φ \land B \leq A) \to B \in ℝ^{*}$
35		ioo0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
36	32 34 35	syl2anc	$⊢ (φ \land B \leq A) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
37	30 36	mpbird	$⊢ (φ \land B \leq A) \to (A, B) = \emptyset$
38	37	feq2d	$⊢ (φ \land B \leq A) \to (F : (A, B) ⟶ ℂ \leftrightarrow F : \emptyset ⟶ ℂ)$
39	29 38	mpbid	$⊢ (φ \land B \leq A) \to F : \emptyset ⟶ ℂ$
40	1	recnd	$⊢ φ \to A \in ℂ$
41	40	adantr	$⊢ (φ \land B \leq A) \to A \in ℂ$
42	39 41	limcdm0	$⊢ (φ \land B \leq A) \to F {lim}_{ℂ} A = ℂ$
43		0cn	$⊢ 0 \in ℂ$
44	43	ne0ii	$⊢ ℂ \neq \emptyset$
45	44	a1i	$⊢ (φ \land B \leq A) \to ℂ \neq \emptyset$
46	42 45	eqnetrd	$⊢ (φ \land B \leq A) \to F {lim}_{ℂ} A \neq \emptyset$
47	25 46 1 2	ltlecasei	$⊢ φ \to F {lim}_{ℂ} A \neq \emptyset$

Metamath Proof Explorer

Theorem ioodvbdlimc1

Proof