Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rlimi Structured version   Visualization version   GIF version

Theorem rlimi 14414
 Description: Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015.)
Hypotheses
Ref Expression
rlimi.1 (𝜑 → ∀𝑧𝐴 𝐵𝑉)
rlimi.2 (𝜑𝑅 ∈ ℝ+)
rlimi.3 (𝜑 → (𝑧𝐴𝐵) ⇝𝑟 𝐶)
Assertion
Ref Expression
rlimi (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑅))
Distinct variable groups:   𝑦,𝑧,𝐴   𝑦,𝐵   𝑦,𝐶,𝑧   𝜑,𝑦   𝑦,𝑅,𝑧   𝑧,𝑉
Allowed substitution hints:   𝜑(𝑧)   𝐵(𝑧)   𝑉(𝑦)

Proof of Theorem rlimi
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 rlimi.2 . 2 (𝜑𝑅 ∈ ℝ+)
2 rlimi.3 . . 3 (𝜑 → (𝑧𝐴𝐵) ⇝𝑟 𝐶)
3 rlimf 14402 . . . . . . 7 ((𝑧𝐴𝐵) ⇝𝑟 𝐶 → (𝑧𝐴𝐵):dom (𝑧𝐴𝐵)⟶ℂ)
42, 3syl 17 . . . . . 6 (𝜑 → (𝑧𝐴𝐵):dom (𝑧𝐴𝐵)⟶ℂ)
5 rlimi.1 . . . . . . . . 9 (𝜑 → ∀𝑧𝐴 𝐵𝑉)
6 eqid 2748 . . . . . . . . . 10 (𝑧𝐴𝐵) = (𝑧𝐴𝐵)
76fmpt 6532 . . . . . . . . 9 (∀𝑧𝐴 𝐵𝑉 ↔ (𝑧𝐴𝐵):𝐴𝑉)
85, 7sylib 208 . . . . . . . 8 (𝜑 → (𝑧𝐴𝐵):𝐴𝑉)
9 fdm 6200 . . . . . . . 8 ((𝑧𝐴𝐵):𝐴𝑉 → dom (𝑧𝐴𝐵) = 𝐴)
108, 9syl 17 . . . . . . 7 (𝜑 → dom (𝑧𝐴𝐵) = 𝐴)
1110feq2d 6180 . . . . . 6 (𝜑 → ((𝑧𝐴𝐵):dom (𝑧𝐴𝐵)⟶ℂ ↔ (𝑧𝐴𝐵):𝐴⟶ℂ))
124, 11mpbid 222 . . . . 5 (𝜑 → (𝑧𝐴𝐵):𝐴⟶ℂ)
136fmpt 6532 . . . . 5 (∀𝑧𝐴 𝐵 ∈ ℂ ↔ (𝑧𝐴𝐵):𝐴⟶ℂ)
1412, 13sylibr 224 . . . 4 (𝜑 → ∀𝑧𝐴 𝐵 ∈ ℂ)
15 rlimss 14403 . . . . . 6 ((𝑧𝐴𝐵) ⇝𝑟 𝐶 → dom (𝑧𝐴𝐵) ⊆ ℝ)
162, 15syl 17 . . . . 5 (𝜑 → dom (𝑧𝐴𝐵) ⊆ ℝ)
1710, 16eqsstr3d 3769 . . . 4 (𝜑𝐴 ⊆ ℝ)
18 rlimcl 14404 . . . . 5 ((𝑧𝐴𝐵) ⇝𝑟 𝐶𝐶 ∈ ℂ)
192, 18syl 17 . . . 4 (𝜑𝐶 ∈ ℂ)
2014, 17, 19rlim2 14397 . . 3 (𝜑 → ((𝑧𝐴𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑥)))
212, 20mpbid 222 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑥))
22 breq2 4796 . . . . 5 (𝑥 = 𝑅 → ((abs‘(𝐵𝐶)) < 𝑥 ↔ (abs‘(𝐵𝐶)) < 𝑅))
2322imbi2d 329 . . . 4 (𝑥 = 𝑅 → ((𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑥) ↔ (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑅)))
2423rexralbidv 3184 . . 3 (𝑥 = 𝑅 → (∃𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑥) ↔ ∃𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑅)))
2524rspcv 3433 . 2 (𝑅 ∈ ℝ+ → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑅)))
261, 21, 25sylc 65 1 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧𝐴 (𝑦𝑧 → (abs‘(𝐵𝐶)) < 𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1620   ∈ wcel 2127  ∀wral 3038  ∃wrex 3039   ⊆ wss 3703   class class class wbr 4792   ↦ cmpt 4869  dom cdm 5254  ⟶wf 6033  ‘cfv 6037  (class class class)co 6801  ℂcc 10097  ℝcr 10098   < clt 10237   ≤ cle 10238   − cmin 10429  ℝ+crp 11996  abscabs 14144   ⇝𝑟 crli 14386 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-cnex 10155  ax-resscn 10156 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-fv 6045  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-pm 8014  df-rlim 14390 This theorem is referenced by:  rlimi2  14415  rlimclim1  14446  rlimuni  14451  rlimcld2  14479  rlimcn1  14489  rlimcn2  14491  rlimo1  14517  o1rlimmul  14519  rlimno1  14554  xrlimcnp  24865  rlimcxp  24870  chtppilimlem2  25333  dchrisumlem3  25350
 Copyright terms: Public domain W3C validator