This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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