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

Theorem climsqz2 10562
Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
Hypotheses
Ref Expression
climadd.1 𝑍 = (ℤ𝑀)
climadd.2 (𝜑𝑀 ∈ ℤ)
climadd.4 (𝜑𝐹𝐴)
climsqz.5 (𝜑𝐺𝑊)
climsqz.6 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
climsqz.7 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
climsqz2.8 ((𝜑𝑘𝑍) → (𝐺𝑘) ≤ (𝐹𝑘))
climsqz2.9 ((𝜑𝑘𝑍) → 𝐴 ≤ (𝐺𝑘))
Assertion
Ref Expression
climsqz2 (𝜑𝐺𝐴)
Distinct variable groups:   𝑘,𝐹   𝜑,𝑘   𝐴,𝑘   𝑘,𝐺   𝑘,𝑀   𝑘,𝑍
Allowed substitution hint:   𝑊(𝑘)

Proof of Theorem climsqz2
Dummy variables 𝑥 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climadd.1 . . . . 5 𝑍 = (ℤ𝑀)
2 climadd.2 . . . . . 6 (𝜑𝑀 ∈ ℤ)
32adantr 270 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
4 simpr 108 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
5 eqidd 2086 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
6 climadd.4 . . . . . 6 (𝜑𝐹𝐴)
76adantr 270 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → 𝐹𝐴)
81, 3, 4, 5, 7climi2 10515 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥)
91uztrn2 8945 . . . . . . . 8 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
10 climsqz.7 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
11 climsqz.6 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
121, 2, 6, 11climrecl 10550 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
1312adantr 270 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝐴 ∈ ℝ)
14 climsqz2.8 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐺𝑘) ≤ (𝐹𝑘))
1510, 11, 13, 14lesub1dd 7956 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝐺𝑘) − 𝐴) ≤ ((𝐹𝑘) − 𝐴))
16 climsqz2.9 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝐴 ≤ (𝐺𝑘))
1713, 10, 16abssubge0d 10450 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (abs‘((𝐺𝑘) − 𝐴)) = ((𝐺𝑘) − 𝐴))
1813, 10, 11, 16, 14letrd 7528 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → 𝐴 ≤ (𝐹𝑘))
1913, 11, 18abssubge0d 10450 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (abs‘((𝐹𝑘) − 𝐴)) = ((𝐹𝑘) − 𝐴))
2015, 17, 193brtr4d 3844 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (abs‘((𝐺𝑘) − 𝐴)) ≤ (abs‘((𝐹𝑘) − 𝐴)))
2120adantlr 461 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → (abs‘((𝐺𝑘) − 𝐴)) ≤ (abs‘((𝐹𝑘) − 𝐴)))
2210adantlr 461 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
2312ad2antrr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → 𝐴 ∈ ℝ)
2422, 23resubcld 7780 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → ((𝐺𝑘) − 𝐴) ∈ ℝ)
2524recnd 7437 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → ((𝐺𝑘) − 𝐴) ∈ ℂ)
2625abscld 10455 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → (abs‘((𝐺𝑘) − 𝐴)) ∈ ℝ)
2711adantlr 461 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
2827, 23resubcld 7780 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → ((𝐹𝑘) − 𝐴) ∈ ℝ)
2928recnd 7437 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → ((𝐹𝑘) − 𝐴) ∈ ℂ)
3029abscld 10455 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → (abs‘((𝐹𝑘) − 𝐴)) ∈ ℝ)
31 rpre 9049 . . . . . . . . . . 11 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
3231ad2antlr 473 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → 𝑥 ∈ ℝ)
33 lelttr 7494 . . . . . . . . . 10 (((abs‘((𝐺𝑘) − 𝐴)) ∈ ℝ ∧ (abs‘((𝐹𝑘) − 𝐴)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘((𝐺𝑘) − 𝐴)) ≤ (abs‘((𝐹𝑘) − 𝐴)) ∧ (abs‘((𝐹𝑘) − 𝐴)) < 𝑥) → (abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
3426, 30, 32, 33syl3anc 1172 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → (((abs‘((𝐺𝑘) − 𝐴)) ≤ (abs‘((𝐹𝑘) − 𝐴)) ∧ (abs‘((𝐹𝑘) − 𝐴)) < 𝑥) → (abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
3521, 34mpand 420 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘𝑍) → ((abs‘((𝐹𝑘) − 𝐴)) < 𝑥 → (abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
369, 35sylan2 280 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((abs‘((𝐹𝑘) − 𝐴)) < 𝑥 → (abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
3736anassrs 392 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((abs‘((𝐹𝑘) − 𝐴)) < 𝑥 → (abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
3837ralimdva 2437 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
3938reximdva 2471 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
408, 39mpd 13 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑥)
4140ralrimiva 2442 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑥)
42 climsqz.5 . . 3 (𝜑𝐺𝑊)
43 eqidd 2086 . . 3 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐺𝑘))
4412recnd 7437 . . 3 (𝜑𝐴 ∈ ℂ)
4510recnd 7437 . . 3 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℂ)
461, 2, 42, 43, 44, 45clim2c 10511 . 2 (𝜑 → (𝐺𝐴 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑥))
4741, 46mpbird 165 1 (𝜑𝐺𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1287  wcel 1436  wral 2355  wrex 2356   class class class wbr 3814  cfv 4972  (class class class)co 5594  cr 7270   < clt 7443  cle 7444  cmin 7574  cz 8660  cuz 8928  +crp 9043  abscabs 10271  cli 10505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3922  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-iinf 4369  ax-cnex 7357  ax-resscn 7358  ax-1cn 7359  ax-1re 7360  ax-icn 7361  ax-addcl 7362  ax-addrcl 7363  ax-mulcl 7364  ax-mulrcl 7365  ax-addcom 7366  ax-mulcom 7367  ax-addass 7368  ax-mulass 7369  ax-distr 7370  ax-i2m1 7371  ax-0lt1 7372  ax-1rid 7373  ax-0id 7374  ax-rnegex 7375  ax-precex 7376  ax-cnre 7377  ax-pre-ltirr 7378  ax-pre-ltwlin 7379  ax-pre-lttrn 7380  ax-pre-apti 7381  ax-pre-ltadd 7382  ax-pre-mulgt0 7383  ax-pre-mulext 7384  ax-arch 7385  ax-caucvg 7386
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-if 3377  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-id 4087  df-po 4090  df-iso 4091  df-iord 4160  df-on 4162  df-ilim 4163  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-riota 5550  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-1st 5849  df-2nd 5850  df-recs 6005  df-frec 6091  df-pnf 7445  df-mnf 7446  df-xr 7447  df-ltxr 7448  df-le 7449  df-sub 7576  df-neg 7577  df-reap 7970  df-ap 7977  df-div 8056  df-inn 8335  df-2 8393  df-3 8394  df-4 8395  df-n0 8584  df-z 8661  df-uz 8929  df-rp 9044  df-iseq 9755  df-iexp 9806  df-cj 10117  df-re 10118  df-im 10119  df-rsqrt 10272  df-abs 10273  df-clim 10506
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator