Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  limcdifap GIF version

Theorem limcdifap 12862
 Description: It suffices to consider functions which are not defined at 𝐵 to define the limit of a function. In particular, the value of the original function 𝐹 at 𝐵 does not affect the limit of 𝐹. (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.)
Hypotheses
Ref Expression
limccl.f (𝜑𝐹:𝐴⟶ℂ)
limcdifap.a (𝜑𝐴 ⊆ ℂ)
Assertion
Ref Expression
limcdifap (𝜑 → (𝐹 lim 𝐵) = ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐹(𝑥)

Proof of Theorem limcdifap
Dummy variables 𝑑 𝑒 𝑢 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limcrcl 12858 . . . . 5 (𝑢 ∈ (𝐹 lim 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
21simp3d 996 . . . 4 (𝑢 ∈ (𝐹 lim 𝐵) → 𝐵 ∈ ℂ)
32a1i 9 . . 3 (𝜑 → (𝑢 ∈ (𝐹 lim 𝐵) → 𝐵 ∈ ℂ))
4 limcrcl 12858 . . . . 5 (𝑢 ∈ ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵) → ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}):dom (𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})⟶ℂ ∧ dom (𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) ⊆ ℂ ∧ 𝐵 ∈ ℂ))
54simp3d 996 . . . 4 (𝑢 ∈ ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵) → 𝐵 ∈ ℂ)
65a1i 9 . . 3 (𝜑 → (𝑢 ∈ ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵) → 𝐵 ∈ ℂ))
7 breq1 3941 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑥 # 𝐵𝑧 # 𝐵))
8 simplr 520 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) ∧ 𝑧 # 𝐵) → 𝑧𝐴)
9 simpr 109 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) ∧ 𝑧 # 𝐵) → 𝑧 # 𝐵)
107, 8, 9elrabd 2847 . . . . . . . . . . . . . . . 16 ((((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) ∧ 𝑧 # 𝐵) → 𝑧 ∈ {𝑥𝐴𝑥 # 𝐵})
11 fvres 5455 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} → ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) = (𝐹𝑧))
1211eqcomd 2146 . . . . . . . . . . . . . . . 16 (𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} → (𝐹𝑧) = ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧))
1310, 12syl 14 . . . . . . . . . . . . . . 15 ((((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) ∧ 𝑧 # 𝐵) → (𝐹𝑧) = ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧))
1413fvoveq1d 5806 . . . . . . . . . . . . . 14 ((((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) ∧ 𝑧 # 𝐵) → (abs‘((𝐹𝑧) − 𝑢)) = (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)))
1514breq1d 3948 . . . . . . . . . . . . 13 ((((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) ∧ 𝑧 # 𝐵) → ((abs‘((𝐹𝑧) − 𝑢)) < 𝑒 ↔ (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))
1615imbi2d 229 . . . . . . . . . . . 12 ((((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) ∧ 𝑧 # 𝐵) → (((abs‘(𝑧𝐵)) < 𝑑 → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒) ↔ ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
1716pm5.74da 440 . . . . . . . . . . 11 (((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) → ((𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒)) ↔ (𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))))
18 impexp 261 . . . . . . . . . . 11 (((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒) ↔ (𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒)))
19 impexp 261 . . . . . . . . . . . . 13 (((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒) ↔ (𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
2019imbi2i 225 . . . . . . . . . . . 12 ((𝑧 # 𝐵 → ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)) ↔ (𝑧 # 𝐵 → (𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))))
21 pm5.4 248 . . . . . . . . . . . 12 ((𝑧 # 𝐵 → (𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))) ↔ (𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
2220, 21bitri 183 . . . . . . . . . . 11 ((𝑧 # 𝐵 → ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)) ↔ (𝑧 # 𝐵 → ((abs‘(𝑧𝐵)) < 𝑑 → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
2317, 18, 223bitr4g 222 . . . . . . . . . 10 (((𝜑𝐵 ∈ ℂ) ∧ 𝑧𝐴) → (((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒) ↔ (𝑧 # 𝐵 → ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))))
2423ralbidva 2435 . . . . . . . . 9 ((𝜑𝐵 ∈ ℂ) → (∀𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒) ↔ ∀𝑧𝐴 (𝑧 # 𝐵 → ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))))
257ralrab 2850 . . . . . . . . 9 (∀𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒) ↔ ∀𝑧𝐴 (𝑧 # 𝐵 → ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
2624, 25bitr4di 197 . . . . . . . 8 ((𝜑𝐵 ∈ ℂ) → (∀𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒) ↔ ∀𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
2726rexbidv 2440 . . . . . . 7 ((𝜑𝐵 ∈ ℂ) → (∃𝑑 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
2827ralbidv 2439 . . . . . 6 ((𝜑𝐵 ∈ ℂ) → (∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒) ↔ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒)))
2928anbi2d 460 . . . . 5 ((𝜑𝐵 ∈ ℂ) → ((𝑢 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒)) ↔ (𝑢 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))))
30 limccl.f . . . . . . 7 (𝜑𝐹:𝐴⟶ℂ)
3130adantr 274 . . . . . 6 ((𝜑𝐵 ∈ ℂ) → 𝐹:𝐴⟶ℂ)
32 limcdifap.a . . . . . . 7 (𝜑𝐴 ⊆ ℂ)
3332adantr 274 . . . . . 6 ((𝜑𝐵 ∈ ℂ) → 𝐴 ⊆ ℂ)
34 simpr 109 . . . . . 6 ((𝜑𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
3531, 33, 34ellimc3ap 12861 . . . . 5 ((𝜑𝐵 ∈ ℂ) → (𝑢 ∈ (𝐹 lim 𝐵) ↔ (𝑢 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑒))))
36 ssrab2 3188 . . . . . . 7 {𝑥𝐴𝑥 # 𝐵} ⊆ 𝐴
37 fssres 5308 . . . . . . 7 ((𝐹:𝐴⟶ℂ ∧ {𝑥𝐴𝑥 # 𝐵} ⊆ 𝐴) → (𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}):{𝑥𝐴𝑥 # 𝐵}⟶ℂ)
3831, 36, 37sylancl 410 . . . . . 6 ((𝜑𝐵 ∈ ℂ) → (𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}):{𝑥𝐴𝑥 # 𝐵}⟶ℂ)
3936, 33sstrid 3114 . . . . . 6 ((𝜑𝐵 ∈ ℂ) → {𝑥𝐴𝑥 # 𝐵} ⊆ ℂ)
4038, 39, 34ellimc3ap 12861 . . . . 5 ((𝜑𝐵 ∈ ℂ) → (𝑢 ∈ ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵) ↔ (𝑢 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ {𝑥𝐴𝑥 # 𝐵} ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑑) → (abs‘(((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵})‘𝑧) − 𝑢)) < 𝑒))))
4129, 35, 403bitr4d 219 . . . 4 ((𝜑𝐵 ∈ ℂ) → (𝑢 ∈ (𝐹 lim 𝐵) ↔ 𝑢 ∈ ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵)))
4241ex 114 . . 3 (𝜑 → (𝐵 ∈ ℂ → (𝑢 ∈ (𝐹 lim 𝐵) ↔ 𝑢 ∈ ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵))))
433, 6, 42pm5.21ndd 695 . 2 (𝜑 → (𝑢 ∈ (𝐹 lim 𝐵) ↔ 𝑢 ∈ ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵)))
4443eqrdv 2138 1 (𝜑 → (𝐹 lim 𝐵) = ((𝐹 ↾ {𝑥𝐴𝑥 # 𝐵}) lim 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  {crab 2421   ⊆ wss 3077   class class class wbr 3938  dom cdm 4549   ↾ cres 4551  ⟶wf 5129  ‘cfv 5133  (class class class)co 5784  ℂcc 7665   < clt 7847   − cmin 7980   # cap 8390  ℝ+crp 9493  abscabs 10824   limℂ climc 12854 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461  ax-cnex 7758 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-id 4224  df-xp 4555  df-rel 4556  df-cnv 4557  df-co 4558  df-dm 4559  df-rn 4560  df-res 4561  df-iota 5098  df-fun 5135  df-fn 5136  df-f 5137  df-fv 5141  df-ov 5787  df-oprab 5788  df-mpo 5789  df-pm 6555  df-limced 12856 This theorem is referenced by:  dvcnp2cntop  12894  dvmulxxbr  12897  dvrecap  12908
 Copyright terms: Public domain W3C validator