Metamath Proof Explorer


Theorem prub

Description: A positive fraction not in a positive real is an upper bound. Remark (1) of Gleason p. 122. (Contributed by NM, 25-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion prub
|- ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( -. C e. A -> B 

Proof

Step Hyp Ref Expression
1 eleq1
 |-  ( B = C -> ( B e. A <-> C e. A ) )
2 1 biimpcd
 |-  ( B e. A -> ( B = C -> C e. A ) )
3 2 adantl
 |-  ( ( A e. P. /\ B e. A ) -> ( B = C -> C e. A ) )
4 prcdnq
 |-  ( ( A e. P. /\ B e. A ) -> ( C  C e. A ) )
5 3 4 jaod
 |-  ( ( A e. P. /\ B e. A ) -> ( ( B = C \/ C  C e. A ) )
6 5 con3d
 |-  ( ( A e. P. /\ B e. A ) -> ( -. C e. A -> -. ( B = C \/ C 
7 6 adantr
 |-  ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( -. C e. A -> -. ( B = C \/ C 
8 elprnq
 |-  ( ( A e. P. /\ B e. A ) -> B e. Q. )
9 ltsonq
 |-  
10 sotric
 |-  ( (  ( B  -. ( B = C \/ C 
11 9 10 mpan
 |-  ( ( B e. Q. /\ C e. Q. ) -> ( B  -. ( B = C \/ C 
12 8 11 sylan
 |-  ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( B  -. ( B = C \/ C 
13 7 12 sylibrd
 |-  ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( -. C e. A -> B