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

Theorem caucvgsrlemofff 7625
 Description: Lemma for caucvgsr 7630. 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‘[⟨𝑛, 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 (𝐹𝑚))
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 5559 . . . 4 ((𝜑𝑎N) → (𝐹𝑎) ∈ R)
3 1sr 7579 . . . 4 1RR
4 addclsr 7581 . . . 4 (((𝐹𝑎) ∈ R ∧ 1RR) → ((𝐹𝑎) +R 1R) ∈ R)
52, 3, 4sylancl 410 . . 3 ((𝜑𝑎N) → ((𝐹𝑎) +R 1R) ∈ R)
6 caucvgsrlembnd.bnd . . . . . 6 (𝜑 → ∀𝑚N 𝐴 <R (𝐹𝑚))
76caucvgsrlemasr 7618 . . . . 5 (𝜑𝐴R)
87adantr 274 . . . 4 ((𝜑𝑎N) → 𝐴R)
9 m1r 7580 . . . 4 -1RR
10 mulclsr 7582 . . . 4 ((𝐴R ∧ -1RR) → (𝐴 ·R -1R) ∈ R)
118, 9, 10sylancl 410 . . 3 ((𝜑𝑎N) → (𝐴 ·R -1R) ∈ R)
12 addclsr 7581 . . 3 ((((𝐹𝑎) +R 1R) ∈ R ∧ (𝐴 ·R -1R) ∈ R) → (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)) ∈ R)
135, 11, 12syl2anc 409 . 2 ((𝜑𝑎N) → (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)) ∈ R)
14 caucvgsrlembnd.offset . 2 𝐺 = (𝑎N ↦ (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)))
1513, 14fmptd 5578 1 (𝜑𝐺:NR)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332   ∈ wcel 1481  {cab 2126  ∀wral 2417  ⟨cop 3531   class class class wbr 3933   ↦ cmpt 3993  ⟶wf 5123  ‘cfv 5127  (class class class)co 5778  1oc1o 6310  [cec 6431  Ncnpi 7100
 Copyright terms: Public domain W3C validator