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

Theorem climcn1 10023
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 265 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → 𝑀 ∈ ℤ)
5 simpr 107 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
6 eqidd 2055 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑘𝑍) → (𝐺𝑘) = (𝐺𝑘))
7 climcn1.5 . . . . . . . . 9 (𝜑𝐺𝐴)
87adantr 265 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ+) → 𝐺𝐴)
92, 4, 5, 6, 8climi2 10003 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦)
102uztrn2 8556 . . . . . . . . . . . 12 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
11 climcn1.8 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)
1211adantlr 454 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑘𝑍) → (𝐺𝑘) ∈ 𝐵)
13 oveq1 5544 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝐺𝑘) → (𝑧𝐴) = ((𝐺𝑘) − 𝐴))
1413fveq2d 5207 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐺𝑘) → (abs‘(𝑧𝐴)) = (abs‘((𝐺𝑘) − 𝐴)))
1514breq1d 3799 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐺𝑘) → ((abs‘(𝑧𝐴)) < 𝑦 ↔ (abs‘((𝐺𝑘) − 𝐴)) < 𝑦))
16 fveq2 5203 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐺𝑘) → (𝐹𝑧) = (𝐹‘(𝐺𝑘)))
1716oveq1d 5552 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝐺𝑘) → ((𝐹𝑧) − (𝐹𝐴)) = ((𝐹‘(𝐺𝑘)) − (𝐹𝐴)))
1817fveq2d 5207 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐺𝑘) → (abs‘((𝐹𝑧) − (𝐹𝐴))) = (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))))
1918breq1d 3799 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐺𝑘) → ((abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥 ↔ (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2015, 19imbi12d 227 . . . . . . . . . . . . . . 15 (𝑧 = (𝐺𝑘) → (((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) ↔ ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)))
2120rspcva 2669 . . . . . . . . . . . . . 14 (((𝐺𝑘) ∈ 𝐵 ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2212, 21sylan 271 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑘𝑍) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2322an32s 510 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ 𝑘𝑍) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2410, 23sylan2 274 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2524anassrs 386 . . . . . . . . . 10 (((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2625ralimdva 2402 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2726reximdva 2436 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ ∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
2827ex 112 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → (∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐺𝑘) − 𝐴)) < 𝑦 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)))
299, 28mpid 41 . . . . . 6 ((𝜑𝑦 ∈ ℝ+) → (∀𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
3029rexlimdva 2448 . . . . 5 (𝜑 → (∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
3130adantr 265 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℝ+𝑧𝐵 ((abs‘(𝑧𝐴)) < 𝑦 → (abs‘((𝐹𝑧) − (𝐹𝐴))) < 𝑥) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
321, 31mpd 13 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)
3332ralrimiva 2407 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥)
34 climcn1.6 . . 3 (𝜑𝐻𝑊)
35 climcn1.9 . . 3 ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
36 climcn1.3 . . . 4 (𝜑𝐴𝐵)
37 climcn1.4 . . . . 5 ((𝜑𝑧𝐵) → (𝐹𝑧) ∈ ℂ)
3837ralrimiva 2407 . . . 4 (𝜑 → ∀𝑧𝐵 (𝐹𝑧) ∈ ℂ)
39 fveq2 5203 . . . . . 6 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
4039eleq1d 2120 . . . . 5 (𝑧 = 𝐴 → ((𝐹𝑧) ∈ ℂ ↔ (𝐹𝐴) ∈ ℂ))
4140rspcv 2667 . . . 4 (𝐴𝐵 → (∀𝑧𝐵 (𝐹𝑧) ∈ ℂ → (𝐹𝐴) ∈ ℂ))
4236, 38, 41sylc 60 . . 3 (𝜑 → (𝐹𝐴) ∈ ℂ)
4338adantr 265 . . . 4 ((𝜑𝑘𝑍) → ∀𝑧𝐵 (𝐹𝑧) ∈ ℂ)
4416eleq1d 2120 . . . . 5 (𝑧 = (𝐺𝑘) → ((𝐹𝑧) ∈ ℂ ↔ (𝐹‘(𝐺𝑘)) ∈ ℂ))
4544rspcv 2667 . . . 4 ((𝐺𝑘) ∈ 𝐵 → (∀𝑧𝐵 (𝐹𝑧) ∈ ℂ → (𝐹‘(𝐺𝑘)) ∈ ℂ))
4611, 43, 45sylc 60 . . 3 ((𝜑𝑘𝑍) → (𝐹‘(𝐺𝑘)) ∈ ℂ)
472, 3, 34, 35, 42, 46clim2c 9999 . 2 (𝜑 → (𝐻 ⇝ (𝐹𝐴) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹‘(𝐺𝑘)) − (𝐹𝐴))) < 𝑥))
4833, 47mpbird 160 1 (𝜑𝐻 ⇝ (𝐹𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101   = wceq 1257  wcel 1407  wral 2321  wrex 2322   class class class wbr 3789  cfv 4927  (class class class)co 5537  cc 6915   < clt 7089  cmin 7215  cz 8272  cuz 8539  +crp 8651  abscabs 9787  cli 9993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-13 1418  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-coll 3897  ax-sep 3900  ax-nul 3908  ax-pow 3952  ax-pr 3969  ax-un 4195  ax-setind 4287  ax-iinf 4336  ax-cnex 7003  ax-resscn 7004  ax-1cn 7005  ax-1re 7006  ax-icn 7007  ax-addcl 7008  ax-addrcl 7009  ax-mulcl 7010  ax-addcom 7012  ax-addass 7014  ax-distr 7016  ax-i2m1 7017  ax-0id 7020  ax-rnegex 7021  ax-cnre 7023  ax-pre-ltirr 7024  ax-pre-ltwlin 7025  ax-pre-lttrn 7026  ax-pre-apti 7027  ax-pre-ltadd 7028
This theorem depends on definitions:  df-bi 114  df-dc 752  df-3or 895  df-3an 896  df-tru 1260  df-fal 1263  df-nf 1364  df-sb 1660  df-eu 1917  df-mo 1918  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ne 2219  df-nel 2313  df-ral 2326  df-rex 2327  df-reu 2328  df-rab 2330  df-v 2574  df-sbc 2785  df-csb 2878  df-dif 2945  df-un 2947  df-in 2949  df-ss 2956  df-nul 3250  df-if 3357  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-int 3641  df-iun 3684  df-br 3790  df-opab 3844  df-mpt 3845  df-tr 3880  df-eprel 4051  df-id 4055  df-po 4058  df-iso 4059  df-iord 4128  df-on 4130  df-suc 4133  df-iom 4339  df-xp 4376  df-rel 4377  df-cnv 4378  df-co 4379  df-dm 4380  df-rn 4381  df-res 4382  df-ima 4383  df-iota 4892  df-fun 4929  df-fn 4930  df-f 4931  df-f1 4932  df-fo 4933  df-f1o 4934  df-fv 4935  df-riota 5493  df-ov 5540  df-oprab 5541  df-mpt2 5542  df-1st 5792  df-2nd 5793  df-recs 5948  df-irdg 5985  df-1o 6029  df-2o 6030  df-oadd 6033  df-omul 6034  df-er 6134  df-ec 6136  df-qs 6140  df-ni 6430  df-pli 6431  df-mi 6432  df-lti 6433  df-plpq 6470  df-mpq 6471  df-enq 6473  df-nqqs 6474  df-plqqs 6475  df-mqqs 6476  df-1nqqs 6477  df-rq 6478  df-ltnqqs 6479  df-enq0 6550  df-nq0 6551  df-0nq0 6552  df-plq0 6553  df-mq0 6554  df-inp 6592  df-i1p 6593  df-iplp 6594  df-iltp 6596  df-enr 6839  df-nr 6840  df-ltr 6843  df-0r 6844  df-1r 6845  df-0 6924  df-1 6925  df-r 6927  df-lt 6930  df-pnf 7091  df-mnf 7092  df-xr 7093  df-ltxr 7094  df-le 7095  df-sub 7217  df-neg 7218  df-inn 7961  df-n0 8210  df-z 8273  df-uz 8540  df-clim 9994
This theorem is referenced by:  climcn1lem  10033
  Copyright terms: Public domain W3C validator