Metamath Proof Explorer

Theorem rpltrp

Description: For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion rpltrp 
|- A. x e. RR+ E. y e. RR+ y < x

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = ( x / 2 ) -> ( y < x <-> ( x / 2 ) < x ) )
2 rphalfcl 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR+ )
3 rphalflt 
 |-  ( x e. RR+ -> ( x / 2 ) < x )
4 1 2 3 rspcedvdw 
 |-  ( x e. RR+ -> E. y e. RR+ y < x )
5 4 rgen 
 |-  A. x e. RR+ E. y e. RR+ y < x