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