Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > limclr | Structured version Visualization version GIF version |
Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. In this case, the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
limclr.k | ⊢ 𝐾 = (TopOpen‘ℂfld) |
limclr.a | ⊢ (𝜑 → 𝐴 ⊆ ℝ) |
limclr.j | ⊢ 𝐽 = (topGen‘ran (,)) |
limclr.f | ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
limclr.lp1 | ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) |
limclr.lp2 | ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) |
limclr.l | ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) |
limclr.r | ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) |
Ref | Expression |
---|---|
limclr | ⊢ (𝜑 → (((𝐹 limℂ 𝐵) ≠ ∅ ↔ 𝐿 = 𝑅) ∧ (𝐿 = 𝑅 → 𝐿 ∈ (𝐹 limℂ 𝐵)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neqne 3019 | . . . . . 6 ⊢ (¬ 𝐿 = 𝑅 → 𝐿 ≠ 𝑅) | |
2 | limclr.k | . . . . . . . 8 ⊢ 𝐾 = (TopOpen‘ℂfld) | |
3 | limclr.a | . . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ ℝ) | |
4 | 3 | adantr 483 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → 𝐴 ⊆ ℝ) |
5 | limclr.j | . . . . . . . 8 ⊢ 𝐽 = (topGen‘ran (,)) | |
6 | limclr.f | . . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | |
7 | 6 | adantr 483 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → 𝐹:𝐴⟶ℂ) |
8 | limclr.lp1 | . . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) | |
9 | 8 | adantr 483 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) |
10 | limclr.lp2 | . . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) | |
11 | 10 | adantr 483 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) |
12 | limclr.l | . . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) | |
13 | 12 | adantr 483 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) |
14 | limclr.r | . . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) | |
15 | 14 | adantr 483 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) |
16 | simpr 487 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → 𝐿 ≠ 𝑅) | |
17 | 2, 4, 5, 7, 9, 11, 13, 15, 16 | limclner 42017 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → (𝐹 limℂ 𝐵) = ∅) |
18 | nne 3015 | . . . . . . 7 ⊢ (¬ (𝐹 limℂ 𝐵) ≠ ∅ ↔ (𝐹 limℂ 𝐵) = ∅) | |
19 | 17, 18 | sylibr 236 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐿 ≠ 𝑅) → ¬ (𝐹 limℂ 𝐵) ≠ ∅) |
20 | 1, 19 | sylan2 594 | . . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 𝑅) → ¬ (𝐹 limℂ 𝐵) ≠ ∅) |
21 | 20 | ex 415 | . . . 4 ⊢ (𝜑 → (¬ 𝐿 = 𝑅 → ¬ (𝐹 limℂ 𝐵) ≠ ∅)) |
22 | 21 | con4d 115 | . . 3 ⊢ (𝜑 → ((𝐹 limℂ 𝐵) ≠ ∅ → 𝐿 = 𝑅)) |
23 | 3 | adantr 483 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → 𝐴 ⊆ ℝ) |
24 | 6 | adantr 483 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → 𝐹:𝐴⟶ℂ) |
25 | retop 23348 | . . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ Top | |
26 | 5, 25 | eqeltri 2907 | . . . . . . . . 9 ⊢ 𝐽 ∈ Top |
27 | inss2 4189 | . . . . . . . . . 10 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵) | |
28 | ioossre 12780 | . . . . . . . . . 10 ⊢ (-∞(,)𝐵) ⊆ ℝ | |
29 | 27, 28 | sstri 3959 | . . . . . . . . 9 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ |
30 | uniretop 23349 | . . . . . . . . . . 11 ⊢ ℝ = ∪ (topGen‘ran (,)) | |
31 | 5 | eqcomi 2829 | . . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = 𝐽 |
32 | 31 | unieqi 4832 | . . . . . . . . . . 11 ⊢ ∪ (topGen‘ran (,)) = ∪ 𝐽 |
33 | 30, 32 | eqtri 2843 | . . . . . . . . . 10 ⊢ ℝ = ∪ 𝐽 |
34 | 33 | lpss 21728 | . . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ) |
35 | 26, 29, 34 | mp2an 690 | . . . . . . . 8 ⊢ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ |
36 | 35, 8 | sseldi 3948 | . . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ) |
37 | 36 | adantr 483 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → 𝐵 ∈ ℝ) |
38 | 12 | adantr 483 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) |
39 | 14 | adantr 483 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) |
40 | simpr 487 | . . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → 𝐿 = 𝑅) | |
41 | 2, 23, 5, 24, 37, 38, 39, 40 | limcleqr 42010 | . . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
42 | 41 | ne0d 4282 | . . . 4 ⊢ ((𝜑 ∧ 𝐿 = 𝑅) → (𝐹 limℂ 𝐵) ≠ ∅) |
43 | 42 | ex 415 | . . 3 ⊢ (𝜑 → (𝐿 = 𝑅 → (𝐹 limℂ 𝐵) ≠ ∅)) |
44 | 22, 43 | impbid 214 | . 2 ⊢ (𝜑 → ((𝐹 limℂ 𝐵) ≠ ∅ ↔ 𝐿 = 𝑅)) |
45 | 41 | ex 415 | . 2 ⊢ (𝜑 → (𝐿 = 𝑅 → 𝐿 ∈ (𝐹 limℂ 𝐵))) |
46 | 44, 45 | jca 514 | 1 ⊢ (𝜑 → (((𝐹 limℂ 𝐵) ≠ ∅ ↔ 𝐿 = 𝑅) ∧ (𝐿 = 𝑅 → 𝐿 ∈ (𝐹 limℂ 𝐵)))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3011 ∩ cin 3918 ⊆ wss 3919 ∅c0 4274 ∪ cuni 4819 ran crn 5537 ↾ cres 5538 ⟶wf 6332 ‘cfv 6336 (class class class)co 7137 ℂcc 10516 ℝcr 10517 +∞cpnf 10653 -∞cmnf 10654 (,)cioo 12720 TopOpenctopn 16673 topGenctg 16689 ℂfldccnfld 20523 Topctop 21479 limPtclp 21720 limℂ climc 24440 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2792 ax-rep 5171 ax-sep 5184 ax-nul 5191 ax-pow 5247 ax-pr 5311 ax-un 7442 ax-cnex 10574 ax-resscn 10575 ax-1cn 10576 ax-icn 10577 ax-addcl 10578 ax-addrcl 10579 ax-mulcl 10580 ax-mulrcl 10581 ax-mulcom 10582 ax-addass 10583 ax-mulass 10584 ax-distr 10585 ax-i2m1 10586 ax-1ne0 10587 ax-1rid 10588 ax-rnegex 10589 ax-rrecex 10590 ax-cnre 10591 ax-pre-lttri 10592 ax-pre-lttrn 10593 ax-pre-ltadd 10594 ax-pre-mulgt0 10595 ax-pre-sup 10596 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2891 df-nfc 2959 df-ne 3012 df-nel 3119 df-ral 3138 df-rex 3139 df-reu 3140 df-rmo 3141 df-rab 3142 df-v 3483 df-sbc 3759 df-csb 3867 df-dif 3922 df-un 3924 df-in 3926 df-ss 3935 df-pss 3937 df-nul 4275 df-if 4449 df-pw 4522 df-sn 4549 df-pr 4551 df-tp 4553 df-op 4555 df-uni 4820 df-int 4858 df-iun 4902 df-iin 4903 df-br 5048 df-opab 5110 df-mpt 5128 df-tr 5154 df-id 5441 df-eprel 5446 df-po 5455 df-so 5456 df-fr 5495 df-we 5497 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-riota 7095 df-ov 7140 df-oprab 7141 df-mpo 7142 df-om 7562 df-1st 7670 df-2nd 7671 df-wrecs 7928 df-recs 7989 df-rdg 8027 df-1o 8083 df-oadd 8087 df-er 8270 df-map 8389 df-pm 8390 df-en 8491 df-dom 8492 df-sdom 8493 df-fin 8494 df-fi 8856 df-sup 8887 df-inf 8888 df-pnf 10658 df-mnf 10659 df-xr 10660 df-ltxr 10661 df-le 10662 df-sub 10853 df-neg 10854 df-div 11279 df-nn 11620 df-2 11682 df-3 11683 df-4 11684 df-5 11685 df-6 11686 df-7 11687 df-8 11688 df-9 11689 df-n0 11880 df-z 11964 df-dec 12081 df-uz 12226 df-q 12331 df-rp 12372 df-xneg 12489 df-xadd 12490 df-xmul 12491 df-ioo 12724 df-fz 12878 df-seq 13355 df-exp 13415 df-cj 14438 df-re 14439 df-im 14440 df-sqrt 14574 df-abs 14575 df-struct 16463 df-ndx 16464 df-slot 16465 df-base 16467 df-plusg 16556 df-mulr 16557 df-starv 16558 df-tset 16562 df-ple 16563 df-ds 16565 df-unif 16566 df-rest 16674 df-topn 16675 df-topgen 16695 df-psmet 20515 df-xmet 20516 df-met 20517 df-bl 20518 df-mopn 20519 df-cnfld 20524 df-top 21480 df-topon 21497 df-topsp 21519 df-bases 21532 df-cld 21605 df-ntr 21606 df-cls 21607 df-nei 21684 df-lp 21722 df-cnp 21814 df-xms 22908 df-ms 22909 df-limc 24444 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |