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

Theorem climcn1 10331
Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
Hypotheses
Ref Expression
climcn1.1 𝑍 = (ℤ𝑀)
climcn1.2 (𝜑𝑀 ∈ ℤ)
climcn1.3 (𝜑𝐴𝐵)
climcn1.4 ((𝜑𝑧𝐵) → (𝐹𝑧) ∈ ℂ)
climcn1.5 (𝜑𝐺𝐴)
climcn1.6 (𝜑𝐻𝑊)
climcn1.7 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))
climcn1.8 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)
climcn1.9 ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
Assertion
Ref Expression
climcn1 (𝜑𝐻 ⇝ (𝐹𝐴))
Distinct variable groups:   𝑥,𝑘,𝑦,𝑧,𝐴   𝐵,𝑘,𝑧   𝑘,𝐺,𝑦,𝑧   𝑘,𝐻,𝑥   𝑘,𝐹,𝑥,𝑦,𝑧   𝜑,𝑘,𝑥,𝑦,𝑧   𝑘,𝑍,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐺(𝑥)   𝐻(𝑦,𝑧)   𝑀(𝑥,𝑦,𝑧,𝑘)   𝑊(𝑥,𝑦,𝑧,𝑘)   𝑍(𝑥,𝑧)

Proof of Theorem climcn1
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 climcn1.7 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥))
2 climcn1.1 . . . . . . . 8 𝑍 = (ℤ𝑀)
3 climcn1.2 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
43adantr 270 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → 𝑀 ∈ ℤ)
5 simpr 108 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
6 eqidd 2084 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑘𝑍) → (𝐺𝑘) = (𝐺𝑘))
7 climcn1.5 . . . . . . . . 9 (𝜑𝐺𝐴)
87adantr 270 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → 𝐺𝐴)
92, 4, 5, 6, 8climi2 10311 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦)
102uztrn2 8752 . . . . . . . . . . . 12 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
11 climcn1.8 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)
1211adantlr 461 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)
13 oveq1 5570 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝐺𝑘) → (𝑧𝐴) = ((𝐺𝑘) − 𝐴))
1413fveq2d 5233 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐺𝑘) → (abs‘(𝑧𝐴)) = (abs‘((𝐺𝑘) − 𝐴)))
1514breq1d 3815 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐺𝑘) → ((abs‘(𝑧𝐴)) < 𝑦 ↔ (abs‘((𝐺𝑘) − 𝐴)) < 𝑦))
16 fveq2 5229 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐺𝑘) → (𝐹𝑧) = (𝐹‘(𝐺𝑘)))
1716oveq1d 5578 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝐺𝑘) → ((𝐹𝑧) − (𝐹𝐴)) = ((𝐹‘(𝐺𝑘)) − (𝐹𝐴)))
1817fveq2d 5233 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐺𝑘) → (abs‘((𝐹𝑧) − (𝐹𝐴))) = (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))))
1918breq1d 3815 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐺𝑘) → ((abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥 ↔ (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2015, 19imbi12d 232 . . . . . . . . . . . . . . 15 (𝑧 = (𝐺𝑘) → (((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) ↔ ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)))
2120rspcva 2707 . . . . . . . . . . . . . 14 (((𝐺𝑘) ∈ 𝐵 ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2212, 21sylan 277 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑘𝑍) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2322an32s 533 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ 𝑘𝑍) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2410, 23sylan2 280 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2524anassrs 392 . . . . . . . . . 10 (((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2625ralimdva 2434 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2726reximdva 2468 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2827ex 113 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → (∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)))
299, 28mpid 41 . . . . . 6 ((𝜑𝑦 ∈ ℝ+) → (∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
3029rexlimdva 2482 . . . . 5 (𝜑 → (∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
3130adantr 270 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
321, 31mpd 13 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)
3332ralrimiva 2439 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)
34 climcn1.6 . . 3 (𝜑𝐻𝑊)
35 climcn1.9 . . 3 ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
36 climcn1.3 . . . 4 (𝜑𝐴𝐵)
37 climcn1.4 . . . . 5 ((𝜑𝑧𝐵) → (𝐹𝑧) ∈ ℂ)
3837ralrimiva 2439 . . . 4 (𝜑 → ∀𝑧𝐵 (𝐹𝑧) ∈ ℂ)
39 fveq2 5229 . . . . . 6 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
4039eleq1d 2151 . . . . 5 (𝑧 = 𝐴 → ((𝐹𝑧) ∈ ℂ ↔ (𝐹𝐴) ∈ ℂ))
4140rspcv 2705 . . . 4 (𝐴𝐵 → (∀𝑧𝐵 (𝐹𝑧) ∈ ℂ → (𝐹𝐴) ∈ ℂ))
4236, 38, 41sylc 61 . . 3 (𝜑 → (𝐹𝐴) ∈ ℂ)
4338adantr 270 . . . 4 ((𝜑𝑘𝑍) → ∀𝑧𝐵 (𝐹𝑧) ∈ ℂ)
4416eleq1d 2151 . . . . 5 (𝑧 = (𝐺𝑘) → ((𝐹𝑧) ∈ ℂ ↔ (𝐹‘(𝐺𝑘)) ∈ ℂ))
4544rspcv 2705 . . . 4 ((𝐺𝑘) ∈ 𝐵 → (∀𝑧𝐵 (𝐹𝑧) ∈ ℂ → (𝐹‘(𝐺𝑘)) ∈ ℂ))
4611, 43, 45sylc 61 . . 3 ((𝜑𝑘𝑍) → (𝐹‘(𝐺𝑘)) ∈ ℂ)
472, 3, 34, 35, 42, 46clim2c 10307 . 2 (𝜑 → (𝐻 ⇝ (𝐹𝐴) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
4833, 47mpbird 165 1 (𝜑𝐻 ⇝ (𝐹𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1285  wcel 1434  wral 2353  wrex 2354   class class class wbr 3805  cfv 4952  (class class class)co 5563  cc 7076   < clt 7250  cmin 7381  cz 8467  cuz 8735  +crp 8850  abscabs 10067  cli 10301
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308  ax-cnex 7164  ax-resscn 7165  ax-1cn 7166  ax-1re 7167  ax-icn 7168  ax-addcl 7169  ax-addrcl 7170  ax-mulcl 7171  ax-addcom 7173  ax-addass 7175  ax-distr 7177  ax-i2m1 7178  ax-0lt1 7179  ax-0id 7181  ax-rnegex 7182  ax-cnre 7184  ax-pre-ltirr 7185  ax-pre-ltwlin 7186  ax-pre-lttrn 7187  ax-pre-apti 7188  ax-pre-ltadd 7189
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2611  df-sbc 2825  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-if 3369  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-br 3806  df-opab 3860  df-mpt 3861  df-id 4076  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-fv 4960  df-riota 5519  df-ov 5566  df-oprab 5567  df-mpt2 5568  df-pnf 7252  df-mnf 7253  df-xr 7254  df-ltxr 7255  df-le 7256  df-sub 7383  df-neg 7384  df-inn 8142  df-n0 8391  df-z 8468  df-uz 8736  df-clim 10302
This theorem is referenced by:  climcn1lem  10341
  Copyright terms: Public domain W3C validator