Theorem squeeze0

Description: If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006)

	Ref	Expression
Assertion	squeeze0	|- ( ( A e. RR /\ 0 <_ A /\ A. x e. RR ( 0 < x -> A < x ) ) -> A = 0 )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		leloe	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
3	1 2	mpan	|- ( A e. RR -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
4		breq2	|- ( x = A -> ( 0 < x <-> 0 < A ) )
5		breq2	|- ( x = A -> ( A < x <-> A < A ) )
6	4 5	imbi12d	|- ( x = A -> ( ( 0 < x -> A < x ) <-> ( 0 < A -> A < A ) ) )
7	6	rspcv	|- ( A e. RR -> ( A. x e. RR ( 0 < x -> A < x ) -> ( 0 < A -> A < A ) ) )
8		ltnr	|- ( A e. RR -> -. A < A )
9	8	pm2.21d	|- ( A e. RR -> ( A < A -> A = 0 ) )
10	9	com12	|- ( A < A -> ( A e. RR -> A = 0 ) )
11	10	imim2i	|- ( ( 0 < A -> A < A ) -> ( 0 < A -> ( A e. RR -> A = 0 ) ) )
12	11	com13	|- ( A e. RR -> ( 0 < A -> ( ( 0 < A -> A < A ) -> A = 0 ) ) )
13	7 12	syl5d	|- ( A e. RR -> ( 0 < A -> ( A. x e. RR ( 0 < x -> A < x ) -> A = 0 ) ) )
14		ax-1	|- ( A = 0 -> ( A. x e. RR ( 0 < x -> A < x ) -> A = 0 ) )
15	14	eqcoms	|- ( 0 = A -> ( A. x e. RR ( 0 < x -> A < x ) -> A = 0 ) )
16	15	a1i	|- ( A e. RR -> ( 0 = A -> ( A. x e. RR ( 0 < x -> A < x ) -> A = 0 ) ) )
17	13 16	jaod	|- ( A e. RR -> ( ( 0 < A \/ 0 = A ) -> ( A. x e. RR ( 0 < x -> A < x ) -> A = 0 ) ) )
18	3 17	sylbid	|- ( A e. RR -> ( 0 <_ A -> ( A. x e. RR ( 0 < x -> A < x ) -> A = 0 ) ) )
19	18	3imp	|- ( ( A e. RR /\ 0 <_ A /\ A. x e. RR ( 0 < x -> A < x ) ) -> A = 0 )