Theorem qsqueeze

Description: If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		ltnle	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A <-> -. A <_ 0 ) )
3	1 2	mpan	|- ( A e. RR -> ( 0 < A <-> -. A <_ 0 ) )
4		qbtwnre	|- ( ( 0 e. RR /\ A e. RR /\ 0 < A ) -> E. x e. QQ ( 0 < x /\ x < A ) )
5	1 4	mp3an1	|- ( ( A e. RR /\ 0 < A ) -> E. x e. QQ ( 0 < x /\ x < A ) )
6	5	ex	|- ( A e. RR -> ( 0 < A -> E. x e. QQ ( 0 < x /\ x < A ) ) )
7		qre	|- ( x e. QQ -> x e. RR )
8		ltnsym	|- ( ( A e. RR /\ x e. RR ) -> ( A < x -> -. x < A ) )
9	8	con2d	|- ( ( A e. RR /\ x e. RR ) -> ( x < A -> -. A < x ) )
10	7 9	sylan2	|- ( ( A e. RR /\ x e. QQ ) -> ( x < A -> -. A < x ) )
11	10	anim2d	|- ( ( A e. RR /\ x e. QQ ) -> ( ( 0 < x /\ x < A ) -> ( 0 < x /\ -. A < x ) ) )
12	11	reximdva	|- ( A e. RR -> ( E. x e. QQ ( 0 < x /\ x < A ) -> E. x e. QQ ( 0 < x /\ -. A < x ) ) )
13	6 12	syld	|- ( A e. RR -> ( 0 < A -> E. x e. QQ ( 0 < x /\ -. A < x ) ) )
14	3 13	sylbird	|- ( A e. RR -> ( -. A <_ 0 -> E. x e. QQ ( 0 < x /\ -. A < x ) ) )
15		rexanali	|- ( E. x e. QQ ( 0 < x /\ -. A < x ) <-> -. A. x e. QQ ( 0 < x -> A < x ) )
16	14 15	syl6ib	|- ( A e. RR -> ( -. A <_ 0 -> -. A. x e. QQ ( 0 < x -> A < x ) ) )
17	16	con4d	|- ( A e. RR -> ( A. x e. QQ ( 0 < x -> A < x ) -> A <_ 0 ) )
18	17	imp	|- ( ( A e. RR /\ A. x e. QQ ( 0 < x -> A < x ) ) -> A <_ 0 )
19	18	3adant2	|- ( ( A e. RR /\ 0 <_ A /\ A. x e. QQ ( 0 < x -> A < x ) ) -> A <_ 0 )
20		letri3	|- ( ( A e. RR /\ 0 e. RR ) -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) )
21	1 20	mpan2	|- ( A e. RR -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) )
22	21	rbaibd	|- ( ( A e. RR /\ 0 <_ A ) -> ( A = 0 <-> A <_ 0 ) )
23	22	3adant3	|- ( ( A e. RR /\ 0 <_ A /\ A. x e. QQ ( 0 < x -> A < x ) ) -> ( A = 0 <-> A <_ 0 ) )
24	19 23	mpbird	|- ( ( A e. RR /\ 0 <_ A /\ A. x e. QQ ( 0 < x -> A < x ) ) -> A = 0 )