unbdqndv1

Description: If the difference quotient ( ( ( Fz ) - ( FA ) ) / ( z - A ) ) is unbounded near A then F is not differentiable at A . (Contributed by Asger C. Ipsen, 12-May-2021)

	Ref	Expression
Hypotheses	unbdqndv1.g	$⊢ G = (z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A})$
	unbdqndv1.1	$⊢ φ \to S \subseteq ℂ$
	unbdqndv1.2	$⊢ φ \to X \subseteq S$
	unbdqndv1.3	$⊢ φ \to F : X ⟶ ℂ$
	unbdqndv1.4	$⊢ φ \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in (X ∖ \{A\}) (\|x - A\| < d \land b \leq \|G (x)\|)$
Assertion	unbdqndv1	$⊢ φ \to \neg A \in dom F_{S}^{'}$

Proof

Step	Hyp	Ref	Expression
1		unbdqndv1.g	$⊢ G = (z \in (X ∖ \{A\}) ⟼ \frac{F (z) - F (A)}{z - A})$
2		unbdqndv1.1	$⊢ φ \to S \subseteq ℂ$
3		unbdqndv1.2	$⊢ φ \to X \subseteq S$
4		unbdqndv1.3	$⊢ φ \to F : X ⟶ ℂ$
5		unbdqndv1.4	$⊢ φ \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in (X ∖ \{A\}) (\|x - A\| < d \land b \leq \|G (x)\|)$
6		noel	$⊢ \neg y \in \emptyset$
7	6	a1i	$⊢ (φ \land A \in dom F_{S}^{'}) \to \neg y \in \emptyset$
8	3 2	sstrd	$⊢ φ \to X \subseteq ℂ$
9	8	adantr	$⊢ (φ \land A \in dom F_{S}^{'}) \to X \subseteq ℂ$
10	9	ssdifssd	$⊢ (φ \land A \in dom F_{S}^{'}) \to X ∖ \{A\} \subseteq ℂ$
11	4	adantr	$⊢ (φ \land A \in dom F_{S}^{'}) \to F : X ⟶ ℂ$
12	2 4 3	dvbss	$⊢ φ \to dom F_{S}^{'} \subseteq X$
13	12	sselda	$⊢ (φ \land A \in dom F_{S}^{'}) \to A \in X$
14	11 9 13	dvlem	$⊢ ((φ \land A \in dom F_{S}^{'}) \land z \in (X ∖ \{A\})) \to \frac{F (z) - F (A)}{z - A} \in ℂ$
15	14 1	fmptd	$⊢ (φ \land A \in dom F_{S}^{'}) \to G : X ∖ \{A\} ⟶ ℂ$
16	9 13	sseldd	$⊢ (φ \land A \in dom F_{S}^{'}) \to A \in ℂ$
17	5	adantr	$⊢ (φ \land A \in dom F_{S}^{'}) \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in (X ∖ \{A\}) (\|x - A\| < d \land b \leq \|G (x)\|)$
18	10 15 16 17	unblimceq0	$⊢ (φ \land A \in dom F_{S}^{'}) \to G {lim}_{ℂ} A = \emptyset$
19	7 18	neleqtrrd	$⊢ (φ \land A \in dom F_{S}^{'}) \to \neg y \in (G {lim}_{ℂ} A)$
20	19	intnand	$⊢ (φ \land A \in dom F_{S}^{'}) \to \neg (A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \land y \in (G {lim}_{ℂ} A))$
21		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
22		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
23	21 22 1 2 4 3	eldv	$⊢ φ \to (A F_{S}^{'} y \leftrightarrow (A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \land y \in (G {lim}_{ℂ} A)))$
24	23	notbid	$⊢ φ \to (\neg A F_{S}^{'} y \leftrightarrow \neg (A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \land y \in (G {lim}_{ℂ} A)))$
25	24	adantr	$⊢ (φ \land A \in dom F_{S}^{'}) \to (\neg A F_{S}^{'} y \leftrightarrow \neg (A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \land y \in (G {lim}_{ℂ} A)))$
26	20 25	mpbird	$⊢ (φ \land A \in dom F_{S}^{'}) \to \neg A F_{S}^{'} y$
27	26	alrimiv	$⊢ (φ \land A \in dom F_{S}^{'}) \to \forall y \neg A F_{S}^{'} y$
28		simpr	$⊢ (φ \land A \in dom F_{S}^{'}) \to A \in dom F_{S}^{'}$
29		eldmg	$⊢ A \in dom F_{S}^{'} \to (A \in dom F_{S}^{'} \leftrightarrow \exists y A F_{S}^{'} y)$
30	28 29	syl	$⊢ (φ \land A \in dom F_{S}^{'}) \to (A \in dom F_{S}^{'} \leftrightarrow \exists y A F_{S}^{'} y)$
31	30	notbid	$⊢ (φ \land A \in dom F_{S}^{'}) \to (\neg A \in dom F_{S}^{'} \leftrightarrow \neg \exists y A F_{S}^{'} y)$
32		alnex	$⊢ \forall y \neg A F_{S}^{'} y \leftrightarrow \neg \exists y A F_{S}^{'} y$
33	32	a1i	$⊢ (φ \land A \in dom F_{S}^{'}) \to (\forall y \neg A F_{S}^{'} y \leftrightarrow \neg \exists y A F_{S}^{'} y)$
34	33	bicomd	$⊢ (φ \land A \in dom F_{S}^{'}) \to (\neg \exists y A F_{S}^{'} y \leftrightarrow \forall y \neg A F_{S}^{'} y)$
35	31 34	bitrd	$⊢ (φ \land A \in dom F_{S}^{'}) \to (\neg A \in dom F_{S}^{'} \leftrightarrow \forall y \neg A F_{S}^{'} y)$
36	27 35	mpbird	$⊢ (φ \land A \in dom F_{S}^{'}) \to \neg A \in dom F_{S}^{'}$
37	36	pm2.01da	$⊢ φ \to \neg A \in dom F_{S}^{'}$

Metamath Proof Explorer

Theorem unbdqndv1

Proof