unbdqndv2

Description: Variant of unbdqndv1 with the hypothesis that ( ( ( Fy ) - ( Fx ) ) / ( y - x ) ) is unbounded where x <_ A and A <_ y . (Contributed by Asger C. Ipsen, 12-May-2021)

	Ref	Expression
Hypotheses	unbdqndv2.x	$⊢ φ \to X \subseteq ℝ$
	unbdqndv2.f	$⊢ φ \to F : X ⟶ ℂ$
	unbdqndv2.1	$⊢ φ \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land b \leq \frac{\|F (y) - F (x)\|}{y - x})$
Assertion	unbdqndv2	$⊢ φ \to \neg A \in dom F_{ℝ}^{'}$

Proof

Step	Hyp	Ref	Expression
1		unbdqndv2.x	$⊢ φ \to X \subseteq ℝ$
2		unbdqndv2.f	$⊢ φ \to F : X ⟶ ℂ$
3		unbdqndv2.1	$⊢ φ \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land b \leq \frac{\|F (y) - F (x)\|}{y - x})$
4		eqid	$⊢ (z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) = (z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A})$
5		ax-resscn	$⊢ ℝ \subseteq ℂ$
6	5	a1i	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to ℝ \subseteq ℂ$
7	1	adantr	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to X \subseteq ℝ$
8	2	adantr	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to F : X ⟶ ℂ$
9		breq1	$⊢ b = 2 c \to (b \leq \frac{\|F (y) - F (x)\|}{y - x} \leftrightarrow 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})$
10	9	3anbi3d	$⊢ b = 2 c \to (((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land b \leq \frac{\|F (y) - F (x)\|}{y - x}) \leftrightarrow ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}))$
11	10	rexbidv	$⊢ b = 2 c \to (\exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land b \leq \frac{\|F (y) - F (x)\|}{y - x}) \leftrightarrow \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}))$
12	11	rexbidv	$⊢ b = 2 c \to (\exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land b \leq \frac{\|F (y) - F (x)\|}{y - x}) \leftrightarrow \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}))$
13	12	ralbidv	$⊢ b = 2 c \to (\forall d \in ℝ^{+} \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land b \leq \frac{\|F (y) - F (x)\|}{y - x}) \leftrightarrow \forall d \in ℝ^{+} \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}))$
14	3	ad2antrr	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land b \leq \frac{\|F (y) - F (x)\|}{y - x})$
15		2rp	$⊢ 2 \in ℝ^{+}$
16	15	a1i	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to 2 \in ℝ^{+}$
17		simprl	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to c \in ℝ^{+}$
18	16 17	rpmulcld	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to 2 c \in ℝ^{+}$
19	13 14 18	rspcdva	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \forall d \in ℝ^{+} \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})$
20		simprr	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to d \in ℝ^{+}$
21		rsp	$⊢ \forall d \in ℝ^{+} \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}) \to (d \in ℝ^{+} \to \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}))$
22	19 20 21	sylc	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})$
23		eqid	$⊢ if (c (y - x) \leq \|F (x) - F (A)\|, x, y) = if (c (y - x) \leq \|F (x) - F (A)\|, x, y)$
24	7	ad3antrrr	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to X \subseteq ℝ$
25	8	ad3antrrr	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to F : X ⟶ ℂ$
26	6 8 7	dvbss	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to dom F_{ℝ}^{'} \subseteq X$
27		simpr	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to A \in dom F_{ℝ}^{'}$
28	26 27	sseldd	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to A \in X$
29	28	adantr	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to A \in X$
30	29	adantr	$⊢ (((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \to A \in X$
31	30	adantr	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to A \in X$
32	17	ad2antrr	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to c \in ℝ^{+}$
33	20	ad2antrr	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to d \in ℝ^{+}$
34		simplrl	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to x \in X$
35		simplrr	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to y \in X$
36		simpr2r	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to x \neq y$
37		simpr1l	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to x \leq A$
38		simpr1r	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to A \leq y$
39		simpr2l	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to y - x < d$
40		simpr3	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}$
41	4 23 24 25 31 32 33 34 35 36 37 38 39 40	unbdqndv2lem2	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to (if (c (y - x) \leq \|F (x) - F (A)\|, x, y) \in (X ∖ \{A\}) \land (\|if (c (y - x) \leq \|F (x) - F (A)\|, x, y) - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (if (c (y - x) \leq \|F (x) - F (A)\|, x, y))\|))$
42	41	simpld	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to if (c (y - x) \leq \|F (x) - F (A)\|, x, y) \in (X ∖ \{A\})$
43		fvoveq1	$⊢ w = if (c (y - x) \leq \|F (x) - F (A)\|, x, y) \to \|w - A\| = \|if (c (y - x) \leq \|F (x) - F (A)\|, x, y) - A\|$
44	43	breq1d	$⊢ w = if (c (y - x) \leq \|F (x) - F (A)\|, x, y) \to (\|w - A\| < d \leftrightarrow \|if (c (y - x) \leq \|F (x) - F (A)\|, x, y) - A\| < d)$
45		2fveq3	$⊢ w = if (c (y - x) \leq \|F (x) - F (A)\|, x, y) \to \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\| = \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (if (c (y - x) \leq \|F (x) - F (A)\|, x, y))\|$
46	45	breq2d	$⊢ w = if (c (y - x) \leq \|F (x) - F (A)\|, x, y) \to (c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\| \leftrightarrow c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (if (c (y - x) \leq \|F (x) - F (A)\|, x, y))\|)$
47	44 46	anbi12d	$⊢ w = if (c (y - x) \leq \|F (x) - F (A)\|, x, y) \to ((\|w - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\|) \leftrightarrow (\|if (c (y - x) \leq \|F (x) - F (A)\|, x, y) - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (if (c (y - x) \leq \|F (x) - F (A)\|, x, y))\|))$
48	47	adantl	$⊢ (((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \land w = if (c (y - x) \leq \|F (x) - F (A)\|, x, y)) \to ((\|w - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\|) \leftrightarrow (\|if (c (y - x) \leq \|F (x) - F (A)\|, x, y) - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (if (c (y - x) \leq \|F (x) - F (A)\|, x, y))\|))$
49	41	simprd	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to (\|if (c (y - x) \leq \|F (x) - F (A)\|, x, y) - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (if (c (y - x) \leq \|F (x) - F (A)\|, x, y))\|)$
50	42 48 49	rspcedvd	$⊢ ((((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \land ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x})) \to \exists w \in (X ∖ \{A\}) (\|w - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\|)$
51	50	ex	$⊢ (((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in X \land y \in X)) \to (((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}) \to \exists w \in (X ∖ \{A\}) (\|w - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\|))$
52	51	rexlimdvva	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to (\exists x \in X \exists y \in X ((x \leq A \land A \leq y) \land (y - x < d \land x \neq y) \land 2 c \leq \frac{\|F (y) - F (x)\|}{y - x}) \to \exists w \in (X ∖ \{A\}) (\|w - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\|))$
53	22 52	mpd	$⊢ ((φ \land A \in dom F_{ℝ}^{'}) \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \exists w \in (X ∖ \{A\}) (\|w - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\|)$
54	53	ralrimivva	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to \forall c \in ℝ^{+} \forall d \in ℝ^{+} \exists w \in (X ∖ \{A\}) (\|w - A\| < d \land c \leq \|(z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A}) (w)\|)$
55	4 6 7 8 54	unbdqndv1	$⊢ (φ \land A \in dom F_{ℝ}^{'}) \to \neg A \in dom F_{ℝ}^{'}$
56	55	pm2.01da	$⊢ φ \to \neg A \in dom F_{ℝ}^{'}$

Metamath Proof Explorer

Theorem unbdqndv2

Proof