Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prcdnq Unicode version

Theorem prcdnq 8497
 Description: A positive real is closed downwards under the positive fractions. Definition 9-3.1 (ii) of [Gleason] p. 121. (Contributed by NM, 25-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
prcdnq

Proof of Theorem prcdnq
StepHypRef Expression
1 ltrelnq 8430 . . . . . . 7
2 relxp 4701 . . . . . . 7
3 relss 4682 . . . . . . 7
41, 2, 3mp2 19 . . . . . 6
54brrelexi 4636 . . . . 5
6 eleq1 2313 . . . . . . . . 9
76anbi2d 687 . . . . . . . 8
8 breq2 3924 . . . . . . . 8
97, 8anbi12d 694 . . . . . . 7
109imbi1d 310 . . . . . 6
11 breq1 3923 . . . . . . . 8
1211anbi2d 687 . . . . . . 7
13 eleq1 2313 . . . . . . 7
1412, 13imbi12d 313 . . . . . 6
15 elnpi 8492 . . . . . . . . . . 11
1615simprbi 452 . . . . . . . . . 10
1716r19.21bi 2603 . . . . . . . . 9
1817simpld 447 . . . . . . . 8
191819.21bi 1774 . . . . . . 7
2019imp 420 . . . . . 6
2110, 14, 20vtocl2g 2785 . . . . 5
225, 21sylan2 462 . . . 4