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

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

Proof of Theorem nqprm
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 nsmallnqq 6395 . . 3 (A Q𝑞 Q 𝑞 <Q A)
2 vex 2554 . . . . 5 𝑞 V
3 breq1 3758 . . . . 5 (x = 𝑞 → (x <Q A𝑞 <Q A))
42, 3elab 2681 . . . 4 (𝑞 {xx <Q A} ↔ 𝑞 <Q A)
54rexbii 2325 . . 3 (𝑞 Q 𝑞 {xx <Q A} ↔ 𝑞 Q 𝑞 <Q A)
61, 5sylibr 137 . 2 (A Q𝑞 Q 𝑞 {xx <Q A})
7 archnqq 6400 . . . . 5 (A Q𝑛 N A <Q [⟨𝑛, 1𝑜⟩] ~Q )
8 df-rex 2306 . . . . 5 (𝑛 N A <Q [⟨𝑛, 1𝑜⟩] ~Q𝑛(𝑛 N A <Q [⟨𝑛, 1𝑜⟩] ~Q ))
97, 8sylib 127 . . . 4 (A Q𝑛(𝑛 N A <Q [⟨𝑛, 1𝑜⟩] ~Q ))
10 1pi 6299 . . . . . . . 8 1𝑜 N
11 opelxpi 4319 . . . . . . . . 9 ((𝑛 N 1𝑜 N) → ⟨𝑛, 1𝑜 (N × N))
12 enqex 6344 . . . . . . . . . 10 ~Q V
1312ecelqsi 6096 . . . . . . . . 9 (⟨𝑛, 1𝑜 (N × N) → [⟨𝑛, 1𝑜⟩] ~Q ((N × N) / ~Q ))
1411, 13syl 14 . . . . . . . 8 ((𝑛 N 1𝑜 N) → [⟨𝑛, 1𝑜⟩] ~Q ((N × N) / ~Q ))
1510, 14mpan2 401 . . . . . . 7 (𝑛 N → [⟨𝑛, 1𝑜⟩] ~Q ((N × N) / ~Q ))
16 df-nqqs 6332 . . . . . . 7 Q = ((N × N) / ~Q )
1715, 16syl6eleqr 2128 . . . . . 6 (𝑛 N → [⟨𝑛, 1𝑜⟩] ~Q Q)
18 breq2 3759 . . . . . . 7 (𝑟 = [⟨𝑛, 1𝑜⟩] ~Q → (A <Q 𝑟A <Q [⟨𝑛, 1𝑜⟩] ~Q ))
1918rspcev 2650 . . . . . 6 (([⟨𝑛, 1𝑜⟩] ~Q Q A <Q [⟨𝑛, 1𝑜⟩] ~Q ) → 𝑟 Q A <Q 𝑟)
2017, 19sylan 267 . . . . 5 ((𝑛 N A <Q [⟨𝑛, 1𝑜⟩] ~Q ) → 𝑟 Q A <Q 𝑟)
2120exlimiv 1486 . . . 4 (𝑛(𝑛 N A <Q [⟨𝑛, 1𝑜⟩] ~Q ) → 𝑟 Q A <Q 𝑟)
229, 21syl 14 . . 3 (A Q𝑟 Q A <Q 𝑟)
23 vex 2554 . . . . 5 𝑟 V
24 breq2 3759 . . . . 5 (x = 𝑟 → (A <Q xA <Q 𝑟))
2523, 24elab 2681 . . . 4 (𝑟 {xA <Q x} ↔ A <Q 𝑟)
2625rexbii 2325 . . 3 (𝑟 Q 𝑟 {xA <Q x} ↔ 𝑟 Q A <Q 𝑟)
2722, 26sylibr 137 . 2 (A Q𝑟 Q 𝑟 {xA <Q x})
286, 27jca 290 1 (A Q → (𝑞 Q 𝑞 {xx <Q A} 𝑟 Q 𝑟 {xA <Q x}))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97  ∃wex 1378   ∈ wcel 1390  {cab 2023  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755   × cxp 4286  1𝑜c1o 5933  [cec 6040   / cqs 6041  Ncnpi 6256   ~Q ceq 6263  Qcnq 6264
 Copyright terms: Public domain W3C validator