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

Theorem nqprloc 6394
 Description: A cut produced from a rational is located. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.)
Assertion
Ref Expression
nqprloc (A Q𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
Distinct variable group:   x,A,𝑟,𝑞

Proof of Theorem nqprloc
StepHypRef Expression
1 nqtri3or 6249 . . . . . . 7 ((𝑞 Q A Q) → (𝑞 <Q A 𝑞 = A A <Q 𝑞))
21ancoms 255 . . . . . 6 ((A Q 𝑞 Q) → (𝑞 <Q A 𝑞 = A A <Q 𝑞))
32ad2antrr 460 . . . . 5 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → (𝑞 <Q A 𝑞 = A A <Q 𝑞))
4 vex 2534 . . . . . . . . . 10 𝑞 V
5 breq1 3737 . . . . . . . . . 10 (x = 𝑞 → (x <Q A𝑞 <Q A))
64, 5elab 2660 . . . . . . . . 9 (𝑞 {xx <Q A} ↔ 𝑞 <Q A)
76biimpri 124 . . . . . . . 8 (𝑞 <Q A𝑞 {xx <Q A})
87orcd 639 . . . . . . 7 (𝑞 <Q A → (𝑞 {xx <Q A} 𝑟 {xA <Q x}))
98a1i 9 . . . . . 6 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → (𝑞 <Q A → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
10 simpr 103 . . . . . . . 8 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → 𝑞 <Q 𝑟)
11 breq1 3737 . . . . . . . 8 (𝑞 = A → (𝑞 <Q 𝑟A <Q 𝑟))
1210, 11syl5ibcom 144 . . . . . . 7 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → (𝑞 = AA <Q 𝑟))
13 vex 2534 . . . . . . . . 9 𝑟 V
14 breq2 3738 . . . . . . . . 9 (x = 𝑟 → (A <Q xA <Q 𝑟))
1513, 14elab 2660 . . . . . . . 8 (𝑟 {xA <Q x} ↔ A <Q 𝑟)
16 olc 619 . . . . . . . 8 (𝑟 {xA <Q x} → (𝑞 {xx <Q A} 𝑟 {xA <Q x}))
1715, 16sylbir 125 . . . . . . 7 (A <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x}))
1812, 17syl6 29 . . . . . 6 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → (𝑞 = A → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
19 ltsonq 6251 . . . . . . . . . 10 <Q Or Q
20 ltrelnq 6218 . . . . . . . . . 10 <Q ⊆ (Q × Q)
2119, 20sotri 4643 . . . . . . . . 9 ((A <Q 𝑞 𝑞 <Q 𝑟) → A <Q 𝑟)
2221, 17syl 14 . . . . . . . 8 ((A <Q 𝑞 𝑞 <Q 𝑟) → (𝑞 {xx <Q A} 𝑟 {xA <Q x}))
2322expcom 109 . . . . . . 7 (𝑞 <Q 𝑟 → (A <Q 𝑞 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
2423adantl 262 . . . . . 6 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → (A <Q 𝑞 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
259, 18, 243jaod 1183 . . . . 5 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → ((𝑞 <Q A 𝑞 = A A <Q 𝑞) → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
263, 25mpd 13 . . . 4 ((((A Q 𝑞 Q) 𝑟 Q) 𝑞 <Q 𝑟) → (𝑞 {xx <Q A} 𝑟 {xA <Q x}))
2726ex 108 . . 3 (((A Q 𝑞 Q) 𝑟 Q) → (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
2827ralrimiva 2366 . 2 ((A Q 𝑞 Q) → 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
2928ralrimiva 2366 1 (A Q𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∨ wo 616   ∨ w3o 870   = wceq 1226   ∈ wcel 1370  {cab 2004  ∀wral 2280   class class class wbr 3734  Qcnq 6134
 Copyright terms: Public domain W3C validator