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

Theorem caucvgsrlembnd 7573
 Description: Lemma for caucvgsr 7574. 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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
3 caucvgsrlembnd.bnd . 2 (𝜑 → ∀𝑚N 𝐴 <R (𝐹𝑚))
4 fveq2 5387 . . . . 5 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
54oveq1d 5755 . . . 4 (𝑎 = 𝑏 → ((𝐹𝑎) +R 1R) = ((𝐹𝑏) +R 1R))
65oveq1d 5755 . . 3 (𝑎 = 𝑏 → (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)) = (((𝐹𝑏) +R 1R) +R (𝐴 ·R -1R)))
76cbvmptv 3992 . 2 (𝑎N ↦ (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R))) = (𝑏N ↦ (((𝐹𝑏) +R 1R) +R (𝐴 ·R -1R)))
81, 2, 3, 7caucvgsrlemoffres 7572 1 (𝜑 → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑘) +R 𝑥)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103  {cab 2101  ∀wral 2391  ∃wrex 2392  ⟨cop 3498   class class class wbr 3897   ↦ cmpt 3957  ⟶wf 5087  ‘cfv 5091  (class class class)co 5740  1oc1o 6272  [cec 6393  Ncnpi 7044
 Copyright terms: Public domain W3C validator