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

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

Proof of Theorem nqprrnd
StepHypRef Expression
1 ltbtwnnqq 6398 . . . . . 6 (A <Q 𝑟𝑞 Q (A <Q 𝑞 𝑞 <Q 𝑟))
2 ancom 253 . . . . . . 7 ((A <Q 𝑞 𝑞 <Q 𝑟) ↔ (𝑞 <Q 𝑟 A <Q 𝑞))
32rexbii 2325 . . . . . 6 (𝑞 Q (A <Q 𝑞 𝑞 <Q 𝑟) ↔ 𝑞 Q (𝑞 <Q 𝑟 A <Q 𝑞))
41, 3bitri 173 . . . . 5 (A <Q 𝑟𝑞 Q (𝑞 <Q 𝑟 A <Q 𝑞))
5 vex 2554 . . . . . 6 𝑟 V
6 breq2 3759 . . . . . 6 (x = 𝑟 → (A <Q xA <Q 𝑟))
75, 6elab 2681 . . . . 5 (𝑟 {xA <Q x} ↔ A <Q 𝑟)
8 vex 2554 . . . . . . . 8 𝑞 V
9 breq2 3759 . . . . . . . 8 (x = 𝑞 → (A <Q xA <Q 𝑞))
108, 9elab 2681 . . . . . . 7 (𝑞 {xA <Q x} ↔ A <Q 𝑞)
1110anbi2i 430 . . . . . 6 ((𝑞 <Q 𝑟 𝑞 {xA <Q x}) ↔ (𝑞 <Q 𝑟 A <Q 𝑞))
1211rexbii 2325 . . . . 5 (𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}) ↔ 𝑞 Q (𝑞 <Q 𝑟 A <Q 𝑞))
134, 7, 123bitr4i 201 . . . 4 (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))
1413rgenw 2370 . . 3 𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))
1514a1i 9 . 2 (A Q𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x})))
16 ltbtwnnqq 6398 . . . 4 (𝑞 <Q A𝑟 Q (𝑞 <Q 𝑟 𝑟 <Q A))
17 breq1 3758 . . . . 5 (x = 𝑞 → (x <Q A𝑞 <Q A))
188, 17elab 2681 . . . 4 (𝑞 {xx <Q A} ↔ 𝑞 <Q A)
19 breq1 3758 . . . . . . 7 (x = 𝑟 → (x <Q A𝑟 <Q A))
205, 19elab 2681 . . . . . 6 (𝑟 {xx <Q A} ↔ 𝑟 <Q A)
2120anbi2i 430 . . . . 5 ((𝑞 <Q 𝑟 𝑟 {xx <Q A}) ↔ (𝑞 <Q 𝑟 𝑟 <Q A))
2221rexbii 2325 . . . 4 (𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A}) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 <Q A))
2316, 18, 223bitr4i 201 . . 3 (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A}))
2423rgenw 2370 . 2 𝑞 Q (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A}))
2515, 24jctil 295 1 (A Q → (𝑞 Q (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A})) 𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301   class class class wbr 3755  Qcnq 6264
 Copyright terms: Public domain W3C validator