Metamath Proof Explorer

Theorem nominpos

Description: There is no smallest positive real number. (Contributed by NM, 28-Oct-2004)

Ref Expression
Assertion nominpos 
|- -. E. x e. RR ( 0 < x /\ -. E. y e. RR ( 0 < y /\ y < x ) )

Proof

Step Hyp Ref Expression
1 rehalfcl 
 |-  ( x e. RR -> ( x / 2 ) e. RR )
2 2re 
 |-  2 e. RR
3 2pos 
 |-  0 < 2
4 divgt0 
 |-  ( ( ( x e. RR /\ 0 < x ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( x / 2 ) )
5 2 3 4 mpanr12 
 |-  ( ( x e. RR /\ 0 < x ) -> 0 < ( x / 2 ) )
6 5 ex 
 |-  ( x e. RR -> ( 0 < x -> 0 < ( x / 2 ) ) )
7 halfpos 
 |-  ( x e. RR -> ( 0 < x <-> ( x / 2 ) < x ) )
8 7 biimpd 
 |-  ( x e. RR -> ( 0 < x -> ( x / 2 ) < x ) )
9 6 8 jcad 
 |-  ( x e. RR -> ( 0 < x -> ( 0 < ( x / 2 ) /\ ( x / 2 ) < x ) ) )
10 breq2 
 |-  ( y = ( x / 2 ) -> ( 0 < y <-> 0 < ( x / 2 ) ) )
11 breq1 
 |-  ( y = ( x / 2 ) -> ( y < x <-> ( x / 2 ) < x ) )
12 10 11 anbi12d 
 |-  ( y = ( x / 2 ) -> ( ( 0 < y /\ y < x ) <-> ( 0 < ( x / 2 ) /\ ( x / 2 ) < x ) ) )
13 12 rspcev 
 |-  ( ( ( x / 2 ) e. RR /\ ( 0 < ( x / 2 ) /\ ( x / 2 ) < x ) ) -> E. y e. RR ( 0 < y /\ y < x ) )
14 1 9 13 syl6an 
 |-  ( x e. RR -> ( 0 < x -> E. y e. RR ( 0 < y /\ y < x ) ) )
15 iman 
 |-  ( ( 0 < x -> E. y e. RR ( 0 < y /\ y < x ) ) <-> -. ( 0 < x /\ -. E. y e. RR ( 0 < y /\ y < x ) ) )
16 14 15 sylib 
 |-  ( x e. RR -> -. ( 0 < x /\ -. E. y e. RR ( 0 < y /\ y < x ) ) )
17 16 nrex 
 |-  -. E. x e. RR ( 0 < x /\ -. E. y e. RR ( 0 < y /\ y < x ) )