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

Theorem caucvgsrlemoffgt1 7494
 Description: Lemma for caucvgsr 7497. 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
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 2479 . . . . . 6 ((𝜑𝑚N) → 𝐴 <R (𝐹𝑚))
3 ltasrg 7466 . . . . . . . 8 ((𝑓R𝑔RR) → (𝑓 <R 𝑔 ↔ ( +R 𝑓) <R ( +R 𝑔)))
43adantl 273 . . . . . . 7 (((𝜑𝑚N) ∧ (𝑓R𝑔RR)) → (𝑓 <R 𝑔 ↔ ( +R 𝑓) <R ( +R 𝑔)))
51caucvgsrlemasr 7485 . . . . . . . 8 (𝜑𝐴R)
65adantr 272 . . . . . . 7 ((𝜑𝑚N) → 𝐴R)
7 caucvgsr.f . . . . . . . 8 (𝜑𝐹:NR)
87ffvelrnda 5487 . . . . . . 7 ((𝜑𝑚N) → (𝐹𝑚) ∈ R)
9 1sr 7447 . . . . . . . 8 1RR
109a1i 9 . . . . . . 7 ((𝜑𝑚N) → 1RR)
11 addcomsrg 7451 . . . . . . . 8 ((𝑓R𝑔R) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
1211adantl 273 . . . . . . 7 (((𝜑𝑚N) ∧ (𝑓R𝑔R)) → (𝑓 +R 𝑔) = (𝑔 +R 𝑓))
134, 6, 8, 10, 12caovord2d 5872 . . . . . 6 ((𝜑𝑚N) → (𝐴 <R (𝐹𝑚) ↔ (𝐴 +R 1R) <R ((𝐹𝑚) +R 1R)))
142, 13mpbid 146 . . . . 5 ((𝜑𝑚N) → (𝐴 +R 1R) <R ((𝐹𝑚) +R 1R))
15 caucvgsr.cau . . . . . 6 (𝜑 → ∀𝑛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 ))))
16 caucvgsrlembnd.offset . . . . . 6 𝐺 = (𝑎N ↦ (((𝐹𝑎) +R 1R) +R (𝐴 ·R -1R)))
177, 15, 1, 16caucvgsrlemoffval 7491 . . . . 5 ((𝜑𝑚N) → ((𝐺𝑚) +R 𝐴) = ((𝐹𝑚) +R 1R))
1814, 17breqtrrd 3901 . . . 4 ((𝜑𝑚N) → (𝐴 +R 1R) <R ((𝐺𝑚) +R 𝐴))
197, 15, 1, 16caucvgsrlemofff 7492 . . . . . 6 (𝜑𝐺:NR)
2019ffvelrnda 5487 . . . . 5 ((𝜑𝑚N) → (𝐺𝑚) ∈ R)
21 addcomsrg 7451 . . . . 5 (((𝐺𝑚) ∈ R𝐴R) → ((𝐺𝑚) +R 𝐴) = (𝐴 +R (𝐺𝑚)))
2220, 6, 21syl2anc 406 . . . 4 ((𝜑𝑚N) → ((𝐺𝑚) +R 𝐴) = (𝐴 +R (𝐺𝑚)))
2318, 22breqtrd 3899 . . 3 ((𝜑𝑚N) → (𝐴 +R 1R) <R (𝐴 +R (𝐺𝑚)))
24 ltasrg 7466 . . . 4 ((1RR ∧ (𝐺𝑚) ∈ R𝐴R) → (1R <R (𝐺𝑚) ↔ (𝐴 +R 1R) <R (𝐴 +R (𝐺𝑚))))
2510, 20, 6, 24syl3anc 1184 . . 3 ((𝜑𝑚N) → (1R <R (𝐺𝑚) ↔ (𝐴 +R 1R) <R (𝐴 +R (𝐺𝑚))))
2623, 25mpbird 166 . 2 ((𝜑𝑚N) → 1R <R (𝐺𝑚))
2726ralrimiva 2464 1 (𝜑 → ∀𝑚N 1R <R (𝐺𝑚))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 930   = wceq 1299   ∈ wcel 1448  {cab 2086  ∀wral 2375  ⟨cop 3477   class class class wbr 3875   ↦ cmpt 3929  ⟶wf 5055  ‘cfv 5059  (class class class)co 5706  1oc1o 6236  [cec 6357  Ncnpi 6981
 Copyright terms: Public domain W3C validator