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