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

Metamath Proof Explorer

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 imbitrdi 
 |-  ( 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 )