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

Metamath Proof Explorer

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 )