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

Theorem caucvgsrlemofff 7087
 Description: Lemma for caucvgsr 7092. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-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 (𝐹𝑚))
caucvgsrlembnd.offset 𝐺 = (𝑎N ↦ (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)))
Assertion
Ref Expression
caucvgsrlemofff (𝜑𝐺:NR)
Distinct variable groups:   𝐴,𝑚   𝜑,𝑎
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑚,𝑛,𝑙)   𝐴(𝑢,𝑘,𝑛,𝑎,𝑙)   𝐹(𝑢,𝑘,𝑚,𝑛,𝑎,𝑙)   𝐺(𝑢,𝑘,𝑚,𝑛,𝑎,𝑙)

Proof of Theorem caucvgsrlemofff
StepHypRef Expression
1 caucvgsr.f . . . . 5 (𝜑𝐹:NR)
21ffvelrnda 5354 . . . 4 ((𝜑𝑎N) → (𝐹𝑎) ∈ R)
3 1sr 7042 . . . 4 1RR
4 addclsr 7044 . . . 4 (((𝐹𝑎) ∈ R ∧ 1RR) → ((𝐹𝑎) +R 1R) ∈ R)
52, 3, 4sylancl 404 . . 3 ((𝜑𝑎N) → ((𝐹𝑎) +R 1R) ∈ R)
6 caucvgsrlembnd.bnd . . . . . 6 (𝜑 → ∀𝑚N 𝐴 <R (𝐹𝑚))
76caucvgsrlemasr 7080 . . . . 5 (𝜑𝐴R)
87adantr 270 . . . 4 ((𝜑𝑎N) → 𝐴R)
9 m1r 7043 . . . 4 -1RR
10 mulclsr 7045 . . . 4 ((𝐴R ∧ -1RR) → (𝐴 ·R -1R) ∈ R)
118, 9, 10sylancl 404 . . 3 ((𝜑𝑎N) → (𝐴 ·R -1R) ∈ R)
12 addclsr 7044 . . 3 ((((𝐹𝑎) +R 1R) ∈ R ∧ (𝐴 ·R -1R) ∈ R) → (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)) ∈ R)
135, 11, 12syl2anc 403 . 2 ((𝜑𝑎N) → (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)) ∈ R)
14 caucvgsrlembnd.offset . 2 𝐺 = (𝑎N ↦ (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)))
1513, 14fmptd 5374 1 (𝜑𝐺:NR)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   = wceq 1285   ∈ wcel 1434  {cab 2069  ∀wral 2353  ⟨cop 3419   class class class wbr 3805   ↦ cmpt 3859  ⟶wf 4948  ‘cfv 4952  (class class class)co 5563  1𝑜c1o 6078  [cec 6191  Ncnpi 6576
 Copyright terms: Public domain W3C validator