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

Theorem caucvgprprlemdisj 7322
 Description: Lemma for caucvgprpr 7332. The putative limit is disjoint. (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
caucvgprprlemdisj (𝜑 → ∀𝑠Q ¬ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿)))
Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝑘,𝐹,𝑛,𝑙   𝐹,𝑟,𝑙   𝑢,𝐹,𝑟   𝑘,𝐿   𝑘,𝑝,𝑟,𝑠   𝜑,𝑟,𝑠   𝑘,𝑞,𝑟,𝑠   𝑝,𝑙,𝑠,𝑞   𝑢,𝑝,𝑠,𝑞   𝑢,𝑛   𝑛,𝑙,𝑘   𝑢,𝑘
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙)   𝐴(𝑢,𝑘,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑠,𝑞,𝑝)   𝐿(𝑢,𝑚,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemdisj
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caucvgprpr.lim . . . . . . . . 9 𝐿 = ⟨{𝑙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 𝑞}⟩}⟩
21caucvgprprlemell 7305 . . . . . . . 8 (𝑠 ∈ (1st𝐿) ↔ (𝑠Q ∧ ∃𝑎N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎)))
32simprbi 270 . . . . . . 7 (𝑠 ∈ (1st𝐿) → ∃𝑎N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎))
41caucvgprprlemelu 7306 . . . . . . . 8 (𝑠 ∈ (2nd𝐿) ↔ (𝑠Q ∧ ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
54simprbi 270 . . . . . . 7 (𝑠 ∈ (2nd𝐿) → ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩)
63, 5anim12i 332 . . . . . 6 ((𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿)) → (∃𝑎N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
7 reeanv 2537 . . . . . 6 (∃𝑎N𝑏N (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩) ↔ (∃𝑎N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
86, 7sylibr 133 . . . . 5 ((𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿)) → ∃𝑎N𝑏N (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
98adantl 272 . . . 4 ((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) → ∃𝑎N𝑏N (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
10 caucvgprpr.f . . . . . . . 8 (𝜑𝐹:NP)
1110ad2antrr 473 . . . . . . 7 (((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) ∧ (𝑎N𝑏N)) → 𝐹:NP)
12 caucvgprpr.cau . . . . . . . 8 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
1312ad2antrr 473 . . . . . . 7 (((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) ∧ (𝑎N𝑏N)) → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
14 simprl 499 . . . . . . 7 (((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) ∧ (𝑎N𝑏N)) → 𝑎N)
15 simprr 500 . . . . . . 7 (((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) ∧ (𝑎N𝑏N)) → 𝑏N)
161caucvgprprlemell 7305 . . . . . . . . . 10 (𝑠 ∈ (1st𝐿) ↔ (𝑠Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
1716simplbi 269 . . . . . . . . 9 (𝑠 ∈ (1st𝐿) → 𝑠Q)
1817ad2antrl 475 . . . . . . . 8 ((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) → 𝑠Q)
1918adantr 271 . . . . . . 7 (((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) ∧ (𝑎N𝑏N)) → 𝑠Q)
2011, 13, 14, 15, 19caucvgprprlemnkj 7312 . . . . . 6 (((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) ∧ (𝑎N𝑏N)) → ¬ (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
2120pm2.21d 585 . . . . 5 (((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) ∧ (𝑎N𝑏N)) → ((⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩) → ⊥))
2221rexlimdvva 2497 . . . 4 ((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) → (∃𝑎N𝑏N (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑎, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑎) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩) → ⊥))
239, 22mpd 13 . . 3 ((𝜑 ∧ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿))) → ⊥)
2423inegd 1309 . 2 (𝜑 → ¬ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿)))
2524ralrimivw 2448 1 (𝜑 → ∀𝑠Q ¬ (𝑠 ∈ (1st𝐿) ∧ 𝑠 ∈ (2nd𝐿)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   = wceq 1290  ⊥wfal 1295   ∈ wcel 1439  {cab 2075  ∀wral 2360  ∃wrex 2361  {crab 2364  ⟨cop 3453   class class class wbr 3851  ⟶wf 5024  ‘cfv 5028  (class class class)co 5666  1st c1st 5923  2nd c2nd 5924  1oc1o 6188  [cec 6304  Ncnpi 6892
 Copyright terms: Public domain W3C validator