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

Theorem prarloc2 6660
 Description: A Dedekind cut is arithmetically located. This is a variation of prarloc 6659 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
Assertion
Ref Expression
prarloc2 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝐿 (𝑎 +Q 𝑃) ∈ 𝑈)
Distinct variable groups:   𝐿,𝑎   𝑃,𝑎   𝑈,𝑎

Proof of Theorem prarloc2
Dummy variable 𝑏 is distinct from all other variables.
StepHypRef Expression
1 prarloc 6659 . 2 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃))
2 prcunqu 6641 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝑏𝑈) → (𝑏 <Q (𝑎 +Q 𝑃) → (𝑎 +Q 𝑃) ∈ 𝑈))
32rexlimdva 2450 . . . 4 (⟨𝐿, 𝑈⟩ ∈ P → (∃𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) → (𝑎 +Q 𝑃) ∈ 𝑈))
43reximdv 2437 . . 3 (⟨𝐿, 𝑈⟩ ∈ P → (∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) → ∃𝑎𝐿 (𝑎 +Q 𝑃) ∈ 𝑈))
54adantr 265 . 2 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → (∃𝑎𝐿𝑏𝑈 𝑏 <Q (𝑎 +Q 𝑃) → ∃𝑎𝐿 (𝑎 +Q 𝑃) ∈ 𝑈))
61, 5mpd 13 1 ((⟨𝐿, 𝑈⟩ ∈ P𝑃Q) → ∃𝑎𝐿 (𝑎 +Q 𝑃) ∈ 𝑈)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∈ wcel 1409  ∃wrex 2324  ⟨cop 3406   class class class wbr 3792  (class class class)co 5540  Qcnq 6436   +Q cplq 6438
 Copyright terms: Public domain W3C validator