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

Theorem caucvgsrlemoffgt1 6911
 Description: Lemma for caucvgsr 6914. 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
caucvgsrlemoffgt1 (𝜑 → ∀𝑚N 1R <R (𝐺𝑚))
Distinct variable groups:   𝐴,𝑎,𝑚   𝐹,𝑎   𝜑,𝑎,𝑚
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑛,𝑙)   𝐴(𝑢,𝑘,𝑛,𝑙)   𝐹(𝑢,𝑘,𝑚,𝑛,𝑙)   𝐺(𝑢,𝑘,𝑚,𝑛,𝑎,𝑙)

Proof of Theorem caucvgsrlemoffgt1
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caucvgsrlembnd.bnd . . . . . . 7 (𝜑 → ∀𝑚N 𝐴 <R (𝐹𝑚))
21r19.21bi 2422 . . . . . 6 ((𝜑𝑚N) → 𝐴 <R (𝐹𝑚))
3 ltasrg 6883 . . . . . . . 8 ((𝑓R𝑔RR) → (𝑓 <R 𝑔 ↔ ( +R 𝑓) <R ( +R 𝑔)))
43adantl 266 . . . . . . 7 (((𝜑𝑚N) ∧ (𝑓R𝑔RR)) → (𝑓 <R 𝑔 ↔ ( +R 𝑓) <R ( +R 𝑔)))
51caucvgsrlemasr 6902 . . . . . . . 8 (𝜑𝐴R)
65adantr 265 . . . . . . 7 ((𝜑𝑚N) → 𝐴R)
7 caucvgsr.f . . . . . . . 8 (𝜑𝐹:NR)
87ffvelrnda 5327 . . . . . . 7 ((𝜑𝑚N) → (𝐹𝑚) ∈ R)
9 1sr 6864 . . . . . . . 8 1RR
109a1i 9 . . . . . . 7 ((𝜑𝑚N) → 1RR)
11 addcomsrg 6868 . . . . . . . 8 ((𝑓R𝑔R) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
1211adantl 266 . . . . . . 7 (((𝜑𝑚N) ∧ (𝑓R𝑔R)) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
134, 6, 8, 10, 12caovord2d 5695 . . . . . 6 ((𝜑𝑚N) → (𝐴 <R (𝐹𝑚) ↔ (𝐴 +R 1R) <R ((𝐹𝑚) +R 1R)))
142, 13mpbid 139 . . . . 5 ((𝜑𝑚N) → (𝐴 +R 1R) <R ((𝐹𝑚) +R 1R))
15 caucvgsr.cau . . . . . 6 (𝜑 → ∀𝑛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 ))))
16 caucvgsrlembnd.offset . . . . . 6 𝐺 = (𝑎N ↦ (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)))
177, 15, 1, 16caucvgsrlemoffval 6908 . . . . 5 ((𝜑𝑚N) → ((𝐺𝑚) +R 𝐴) = ((𝐹𝑚) +R 1R))
1814, 17breqtrrd 3815 . . . 4 ((𝜑𝑚N) → (𝐴 +R 1R) <R ((𝐺𝑚) +R 𝐴))
197, 15, 1, 16caucvgsrlemofff 6909 . . . . . 6 (𝜑𝐺:NR)
2019ffvelrnda 5327 . . . . 5 ((𝜑𝑚N) → (𝐺𝑚) ∈ R)
21 addcomsrg 6868 . . . . 5 (((𝐺𝑚) ∈ R𝐴R) → ((𝐺𝑚) +R 𝐴) = (𝐴 +R (𝐺𝑚)))
2220, 6, 21syl2anc 397 . . . 4 ((𝜑𝑚N) → ((𝐺𝑚) +R 𝐴) = (𝐴 +R (𝐺𝑚)))
2318, 22breqtrd 3813 . . 3 ((𝜑𝑚N) → (𝐴 +R 1R) <R (𝐴 +R (𝐺𝑚)))
24 ltasrg 6883 . . . 4 ((1RR ∧ (𝐺𝑚) ∈ R𝐴R) → (1R <R (𝐺𝑚) ↔ (𝐴 +R 1R) <R (𝐴 +R (𝐺𝑚))))
2510, 20, 6, 24syl3anc 1144 . . 3 ((𝜑𝑚N) → (1R <R (𝐺𝑚) ↔ (𝐴 +R 1R) <R (𝐴 +R (𝐺𝑚))))
2623, 25mpbird 160 . 2 ((𝜑𝑚N) → 1R <R (𝐺𝑚))
2726ralrimiva 2407 1 (𝜑 → ∀𝑚N 1R <R (𝐺𝑚))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∧ w3a 894   = wceq 1257   ∈ wcel 1407  {cab 2040  ∀wral 2321  ⟨cop 3403   class class class wbr 3789   ↦ cmpt 3843  ⟶wf 4923  ‘cfv 4927  (class class class)co 5537  1𝑜c1o 6022  [cec 6132  Ncnpi 6398
 Copyright terms: Public domain W3C validator