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

Theorem caucvgprprlemrnd 7473
 Description: Lemma for caucvgprpr 7484. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
caucvgprpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprpr.bnd (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
caucvgprpr.lim 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
Assertion
Ref Expression
caucvgprprlemrnd (𝜑 → (∀𝑠Q (𝑠 ∈ (1st𝐿) ↔ ∃𝑡Q (𝑠 <Q 𝑡𝑡 ∈ (1st𝐿))) ∧ ∀𝑡Q (𝑡 ∈ (2nd𝐿) ↔ ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)))))
Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝐹,𝑙,𝑡   𝑢,𝐹,𝑡,𝑟,𝑠   𝐿,𝑠,𝑡   𝑝,𝑙,𝑞,𝑟,𝑠,𝑡   𝑢,𝑝,𝑞,𝑟,𝑠   𝜑,𝑟,𝑠,𝑡
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙)   𝐴(𝑢,𝑡,𝑘,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑘,𝑛,𝑞,𝑝)   𝐿(𝑢,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemrnd
StepHypRef Expression
1 caucvgprpr.f . . . . . 6 (𝜑𝐹:NP)
2 caucvgprpr.cau . . . . . 6 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
3 caucvgprpr.bnd . . . . . 6 (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
4 caucvgprpr.lim . . . . . 6 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
51, 2, 3, 4caucvgprprlemopl 7469 . . . . 5 ((𝜑𝑠 ∈ (1st𝐿)) → ∃𝑡Q (𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)))
65ex 114 . . . 4 (𝜑 → (𝑠 ∈ (1st𝐿) → ∃𝑡Q (𝑠 <Q 𝑡𝑡 ∈ (1st𝐿))))
71, 2, 3, 4caucvgprprlemlol 7470 . . . . . 6 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿))
873expib 1167 . . . . 5 (𝜑 → ((𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿)))
98rexlimdvw 2528 . . . 4 (𝜑 → (∃𝑡Q (𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿)))
106, 9impbid 128 . . 3 (𝜑 → (𝑠 ∈ (1st𝐿) ↔ ∃𝑡Q (𝑠 <Q 𝑡𝑡 ∈ (1st𝐿))))
1110ralrimivw 2481 . 2 (𝜑 → ∀𝑠Q (𝑠 ∈ (1st𝐿) ↔ ∃𝑡Q (𝑠 <Q 𝑡𝑡 ∈ (1st𝐿))))
121, 2, 3, 4caucvgprprlemopu 7471 . . . . 5 ((𝜑𝑡 ∈ (2nd𝐿)) → ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)))
1312ex 114 . . . 4 (𝜑 → (𝑡 ∈ (2nd𝐿) → ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿))))
141, 2, 3, 4caucvgprprlemupu 7472 . . . . . 6 ((𝜑𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)) → 𝑡 ∈ (2nd𝐿))
15143expib 1167 . . . . 5 (𝜑 → ((𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)) → 𝑡 ∈ (2nd𝐿)))
1615rexlimdvw 2528 . . . 4 (𝜑 → (∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)) → 𝑡 ∈ (2nd𝐿)))
1713, 16impbid 128 . . 3 (𝜑 → (𝑡 ∈ (2nd𝐿) ↔ ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿))))
1817ralrimivw 2481 . 2 (𝜑 → ∀𝑡Q (𝑡 ∈ (2nd𝐿) ↔ ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿))))
1911, 18jca 302 1 (𝜑 → (∀𝑠Q (𝑠 ∈ (1st𝐿) ↔ ∃𝑡Q (𝑠 <Q 𝑡𝑡 ∈ (1st𝐿))) ∧ ∀𝑡Q (𝑡 ∈ (2nd𝐿) ↔ ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1314   ∈ wcel 1463  {cab 2101  ∀wral 2391  ∃wrex 2392  {crab 2395  ⟨cop 3498   class class class wbr 3897  ⟶wf 5087  ‘cfv 5091  (class class class)co 5740  1st c1st 6002  2nd c2nd 6003  1oc1o 6272  [cec 6393  Ncnpi 7044
 Copyright terms: Public domain W3C validator