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

Theorem caucvgsrlemf 7564
 Description: Lemma for caucvgsr 7574. Defining the sequence in terms of positive reals. (Contributed by Jim Kingdon, 23-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 ))))
caucvgsrlemgt1.gt1 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
caucvgsrlemf.xfr 𝐺 = (𝑥N ↦ (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
Assertion
Ref Expression
caucvgsrlemf (𝜑𝐺:NP)
Distinct variable groups:   𝑚,𝐹   𝑦,𝐹   𝑥,𝑚   𝜑,𝑥   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑦,𝑢,𝑘,𝑚,𝑛,𝑙)   𝐹(𝑥,𝑢,𝑘,𝑛,𝑙)   𝐺(𝑥,𝑦,𝑢,𝑘,𝑚,𝑛,𝑙)

Proof of Theorem caucvgsrlemf
StepHypRef Expression
1 caucvgsr.f . . 3 (𝜑𝐹:NR)
2 caucvgsrlemgt1.gt1 . . 3 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
31, 2caucvgsrlemcl 7561 . 2 ((𝜑𝑥N) → (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) ∈ P)
4 caucvgsrlemf.xfr . 2 𝐺 = (𝑥N ↦ (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
53, 4fmptd 5540 1 (𝜑𝐺:NP)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1314  {cab 2101  ∀wral 2391  ⟨cop 3498   class class class wbr 3897   ↦ cmpt 3957  ⟶wf 5087  ‘cfv 5091  ℩crio 5695  (class class class)co 5740  1oc1o 6272  [cec 6393  Ncnpi 7044
 Copyright terms: Public domain W3C validator