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

Theorem caucvgsrlembnd 6885
 Description: Lemma for caucvgsr 6886. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.)
Hypotheses
Ref Expression
caucvgsr.f (𝜑𝐹:NR)
caucvgsr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <R ((𝐹𝑘) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
caucvgsrlembnd.bnd (𝜑 → ∀𝑚N 𝐴 <R (𝐹𝑚))
Assertion
Ref Expression
caucvgsrlembnd (𝜑 → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑘) +R 𝑥)))))
Distinct variable groups:   𝐴,𝑘,𝑛   𝐴,𝑗,𝑙,𝑢,𝑘   𝐴,𝑚,𝑘   𝑥,𝐴,𝑗,𝑘,𝑦   𝑘,𝐹,𝑛   𝑗,𝐹,𝑙,𝑢   𝑚,𝐹   𝑥,𝐹,𝑦   𝜑,𝑘,𝑛   𝜑,𝑗,𝑥   𝜑,𝑚   𝑛,𝑙,𝑢   𝑚,𝑛
Allowed substitution hints:   𝜑(𝑦,𝑢,𝑙)

Proof of Theorem caucvgsrlembnd
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caucvgsr.f . 2 (𝜑𝐹:NR)
2 caucvgsr.cau . 2 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <R ((𝐹𝑘) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
3 caucvgsrlembnd.bnd . 2 (𝜑 → ∀𝑚N 𝐴 <R (𝐹𝑚))
4 fveq2 5178 . . . . 5 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
54oveq1d 5527 . . . 4 (𝑎 = 𝑏 → ((𝐹𝑎) +R 1R) = ((𝐹𝑏) +R 1R))
65oveq1d 5527 . . 3 (𝑎 = 𝑏 → (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)) = (((𝐹𝑏) +R 1R) +R (𝐴 ·R -1R)))
76cbvmptv 3852 . 2 (𝑎N ↦ (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R))) = (𝑏N ↦ (((𝐹𝑏) +R 1R) +R (𝐴 ·R -1R)))
81, 2, 3, 7caucvgsrlemoffres 6884 1 (𝜑 → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑘) +R 𝑥)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97  {cab 2026  ∀wral 2306  ∃wrex 2307  ⟨cop 3378   class class class wbr 3764   ↦ cmpt 3818  ⟶wf 4898  ‘cfv 4902  (class class class)co 5512  1𝑜c1o 5994  [cec 6104  Ncnpi 6370
 Copyright terms: Public domain W3C validator