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

Theorem prarloc2 6352
 Description: A Dedekind cut is arithmetically located. This is a variation of prarloc 6351 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 6351 . 2 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))
2 prcunqu 6333 . . . . 5 ((⟨𝐿, 𝑈 P 𝑏 𝑈) → (𝑏 <Q (𝑎 +Q 𝑃) → (𝑎 +Q 𝑃) 𝑈))
32rexlimdva 2407 . . . 4 (⟨𝐿, 𝑈 P → (𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃) → (𝑎 +Q 𝑃) 𝑈))
43reximdv 2394 . . 3 (⟨𝐿, 𝑈 P → (𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃) → 𝑎 𝐿 (𝑎 +Q 𝑃) 𝑈))
54adantr 261 . 2 ((⟨𝐿, 𝑈 P 𝑃 Q) → (𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃) → 𝑎 𝐿 (𝑎 +Q 𝑃) 𝑈))
61, 5mpd 13 1 ((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑎 𝐿 (𝑎 +Q 𝑃) 𝑈)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1370  ∃wrex 2281  ⟨cop 3349   class class class wbr 3734  (class class class)co 5432  Qcnq 6134   +Q cplq 6136
 Copyright terms: Public domain W3C validator