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

Theorem caucvgprlemlim 7482
 Description: Lemma for caucvgpr 7483. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.)
Hypotheses
Ref Expression
caucvgpr.f (𝜑𝐹:NQ)
caucvgpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )))))
caucvgpr.bnd (𝜑 → ∀𝑗N 𝐴 <Q (𝐹𝑗))
caucvgpr.lim 𝐿 = ⟨{𝑙Q ∣ ∃𝑗N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹𝑗)}, {𝑢Q ∣ ∃𝑗N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩
Assertion
Ref Expression
caucvgprlemlim (𝜑 → ∀𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
Distinct variable groups:   𝐴,𝑗   𝑗,𝐹,𝑢,𝑙,𝑘   𝑛,𝐹,𝑘   𝑗,𝑘,𝜑,𝑥   𝑘,𝑙,𝑢,𝑥,𝑗   𝑗,𝐿,𝑘
Allowed substitution hints:   𝜑(𝑢,𝑛,𝑙)   𝐴(𝑥,𝑢,𝑘,𝑛,𝑙)   𝐹(𝑥)   𝐿(𝑥,𝑢,𝑛,𝑙)

Proof of Theorem caucvgprlemlim
StepHypRef Expression
1 archrecnq 7464 . . . 4 (𝑥Q → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥)
21adantl 275 . . 3 ((𝜑𝑥Q) → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥)
3 caucvgpr.f . . . . . . . . . 10 (𝜑𝐹:NQ)
43ad5antr 487 . . . . . . . . 9 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → 𝐹:NQ)
5 caucvgpr.cau . . . . . . . . . 10 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )))))
65ad5antr 487 . . . . . . . . 9 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )))))
7 caucvgpr.bnd . . . . . . . . . 10 (𝜑 → ∀𝑗N 𝐴 <Q (𝐹𝑗))
87ad5antr 487 . . . . . . . . 9 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → ∀𝑗N 𝐴 <Q (𝐹𝑗))
9 caucvgpr.lim . . . . . . . . 9 𝐿 = ⟨{𝑙Q ∣ ∃𝑗N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹𝑗)}, {𝑢Q ∣ ∃𝑗N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩
10 simpr 109 . . . . . . . . . 10 ((𝜑𝑥Q) → 𝑥Q)
1110ad4antr 485 . . . . . . . . 9 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → 𝑥Q)
12 simpr 109 . . . . . . . . 9 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → 𝑗 <N 𝑘)
13 simpllr 523 . . . . . . . . 9 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥)
144, 6, 8, 9, 11, 12, 13caucvgprlem1 7480 . . . . . . . 8 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → ⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩))
154, 6, 8, 9, 11, 12, 13caucvgprlem2 7481 . . . . . . . 8 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)
1614, 15jca 304 . . . . . . 7 ((((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) ∧ 𝑗 <N 𝑘) → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))
1716ex 114 . . . . . 6 (((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) ∧ 𝑘N) → (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
1817ralrimiva 2503 . . . . 5 ((((𝜑𝑥Q) ∧ 𝑗N) ∧ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥) → ∀𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
1918ex 114 . . . 4 (((𝜑𝑥Q) ∧ 𝑗N) → ((*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥 → ∀𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))))
2019reximdva 2532 . . 3 ((𝜑𝑥Q) → (∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥 → ∃𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))))
212, 20mpd 13 . 2 ((𝜑𝑥Q) → ∃𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
2221ralrimiva 2503 1 (𝜑 → ∀𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331   ∈ wcel 1480  {cab 2123  ∀wral 2414  ∃wrex 2415  {crab 2418  ⟨cop 3525   class class class wbr 3924  ⟶wf 5114  ‘cfv 5118  (class class class)co 5767  1oc1o 6299  [cec 6420  Ncnpi 7073
 Copyright terms: Public domain W3C validator