unbdqndv1 - Mathbox for Asger C. Ipsen

	Mathbox for Asger C. Ipsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > unbdqndv1		Structured version Visualization version GIF version

Theorem unbdqndv1 36954

Description: If the difference quotient (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) is unbounded near 𝐴 then 𝐹 is not differentiable at 𝐴. (Contributed by Asger C. Ipsen, 12-May-2021.)

**Hypotheses**
Ref	Expression
unbdqndv1.g	⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))
unbdqndv1.1	⊢ (𝜑 → 𝑆 ⊆ ℂ)
unbdqndv1.2	⊢ (𝜑 → 𝑋 ⊆ 𝑆)
unbdqndv1.3	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
unbdqndv1.4	⊢ (𝜑 → ∀𝑏 ∈ ℝ⁺ ∀𝑑 ∈ ℝ⁺ ∃𝑥 ∈ (𝑋 ∖ {𝐴})((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐺‘𝑥))))

**Assertion**
Ref	Expression
unbdqndv1	⊢ (𝜑 → ¬ 𝐴 ∈ dom (𝑆 D 𝐹))

Distinct variable groups: 𝐴,𝑏,𝑑,𝑥 𝑧,𝐴 𝐹,𝑏,𝑑,𝑥 𝑧,𝐹 𝐺,𝑏,𝑑,𝑥 𝑆,𝑏,𝑑,𝑥 𝑧,𝑆 𝑋,𝑏,𝑑,𝑥 𝑧,𝑋 𝜑,𝑏,𝑑,𝑥 𝜑,𝑧 Allowed substitution hint: 𝐺(𝑧)

Proof of Theorem unbdqndv1 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4293	. . . . . . . 8 ⊢ ¬ 𝑦 ∈ ∅
2	1	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → ¬ 𝑦 ∈ ∅)
3		unbdqndv1.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
4		unbdqndv1.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
5	3, 4	sstrd 3949	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
6	5	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → 𝑋 ⊆ ℂ)
7	6	ssdifssd 4103	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (𝑋 ∖ {𝐴}) ⊆ ℂ)
8		unbdqndv1.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
9	8	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → 𝐹:𝑋⟶ℂ)
10	4, 8, 3	dvbss 26017	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
11	10	sselda 3939	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → 𝐴 ∈ 𝑋)
12	9, 6, 11	dvlem 26012	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) ∧ 𝑧 ∈ (𝑋 ∖ {𝐴})) → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) ∈ ℂ)
13		unbdqndv1.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))
14	12, 13	fmptd 7099	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → 𝐺:(𝑋 ∖ {𝐴})⟶ℂ)
15	6, 11	sseldd 3940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → 𝐴 ∈ ℂ)
16		unbdqndv1.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑏 ∈ ℝ⁺ ∀𝑑 ∈ ℝ⁺ ∃𝑥 ∈ (𝑋 ∖ {𝐴})((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐺‘𝑥))))
17	16	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → ∀𝑏 ∈ ℝ⁺ ∀𝑑 ∈ ℝ⁺ ∃𝑥 ∈ (𝑋 ∖ {𝐴})((abs‘(𝑥 − 𝐴)) < 𝑑 ∧ 𝑏 ≤ (abs‘(𝐺‘𝑥))))
18	7, 14, 15, 17	unblimceq0 36953	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (𝐺 lim_ℂ 𝐴) = ∅)
19	2, 18	neleqtrrd 2888	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → ¬ 𝑦 ∈ (𝐺 lim_ℂ 𝐴))
20	19	intnand 493	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → ¬ (𝐴 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝑋) ∧ 𝑦 ∈ (𝐺 lim_ℂ 𝐴)))
21		eqid 2765	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ((TopOpen‘ℂ_fld) ↾_t 𝑆)
22		eqid 2765	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
23	21, 22, 13, 4, 8, 3	eldv 26014	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝑆 D 𝐹)𝑦 ↔ (𝐴 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝑋) ∧ 𝑦 ∈ (𝐺 lim_ℂ 𝐴))))
24	23	notbid 321	. . . . . 6 ⊢ (𝜑 → (¬ 𝐴(𝑆 D 𝐹)𝑦 ↔ ¬ (𝐴 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝑋) ∧ 𝑦 ∈ (𝐺 lim_ℂ 𝐴))))
25	24	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (¬ 𝐴(𝑆 D 𝐹)𝑦 ↔ ¬ (𝐴 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝑋) ∧ 𝑦 ∈ (𝐺 lim_ℂ 𝐴))))
26	20, 25	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → ¬ 𝐴(𝑆 D 𝐹)𝑦)
27	26	alrimiv 1950	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → ∀𝑦 ¬ 𝐴(𝑆 D 𝐹)𝑦)
28		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → 𝐴 ∈ dom (𝑆 D 𝐹))
29		eldmg 5878	. . . . . 6 ⊢ (𝐴 ∈ dom (𝑆 D 𝐹) → (𝐴 ∈ dom (𝑆 D 𝐹) ↔ ∃𝑦 𝐴(𝑆 D 𝐹)𝑦))
30	28, 29	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (𝐴 ∈ dom (𝑆 D 𝐹) ↔ ∃𝑦 𝐴(𝑆 D 𝐹)𝑦))
31	30	notbid 321	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (¬ 𝐴 ∈ dom (𝑆 D 𝐹) ↔ ¬ ∃𝑦 𝐴(𝑆 D 𝐹)𝑦))
32		alnex 1804	. . . . . 6 ⊢ (∀𝑦 ¬ 𝐴(𝑆 D 𝐹)𝑦 ↔ ¬ ∃𝑦 𝐴(𝑆 D 𝐹)𝑦)
33	32	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (∀𝑦 ¬ 𝐴(𝑆 D 𝐹)𝑦 ↔ ¬ ∃𝑦 𝐴(𝑆 D 𝐹)𝑦))
34	33	bicomd 226	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (¬ ∃𝑦 𝐴(𝑆 D 𝐹)𝑦 ↔ ∀𝑦 ¬ 𝐴(𝑆 D 𝐹)𝑦))
35	31, 34	bitrd 282	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → (¬ 𝐴 ∈ dom (𝑆 D 𝐹) ↔ ∀𝑦 ¬ 𝐴(𝑆 D 𝐹)𝑦))
36	27, 35	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑆 D 𝐹)) → ¬ 𝐴 ∈ dom (𝑆 D 𝐹))
37	36	pm2.01da 810	1 ⊢ (𝜑 → ¬ 𝐴 ∈ dom (𝑆 D 𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∀wal 1561 = wceq 1563 ∃wex 1802 ∈ wcel 2145 ∀wral 3079 ∃wrex 3089 ∖ cdif 3904 ⊆ wss 3907 ∅c0 4288 {csn 4585 class class class wbr 5104 ↦ cmpt 5185 dom cdm 5651 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ℂcc 11086 < clt 11231 ≤ cle 11232 − cmin 11429 / cdiv 11859 ℝ⁺crp 13004 abscabs 15273 ↾_t crest 17461 TopOpenctopn 17462 ℂ_fldccnfld 21479 intcnt 23131 lim_ℂ climc 25978 D cdv 25979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-map 8814 df-pm 8815 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fi 9359 df-sup 9390 df-inf 9391 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-7 12296 df-8 12297 df-9 12298 df-n0 12493 df-z 12580 df-dec 12700 df-uz 12851 df-q 12961 df-rp 13005 df-xneg 13125 df-xadd 13126 df-xmul 13127 df-fz 13524 df-seq 14026 df-exp 14086 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-struct 17195 df-slot 17230 df-ndx 17242 df-base 17258 df-plusg 17311 df-mulr 17312 df-starv 17313 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-rest 17463 df-topn 17464 df-topgen 17484 df-psmet 21471 df-xmet 21472 df-met 21473 df-bl 21474 df-mopn 21475 df-cnfld 21480 df-top 23008 df-topon 23025 df-topsp 23047 df-bases 23060 df-ntr 23134 df-cnp 23342 df-xms 24434 df-ms 24435 df-limc 25982 df-dv 25983

This theorem is referenced by: unbdqndv2 36957

W3C validator