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

Metamath Proof Explorer

Theorem infmrp1

Description: The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion infmrp1 
|- inf ( RR+ , RR , < ) = 0

Proof

Step Hyp Ref Expression
1 rpltrp 
 |-  A. x e. RR+ E. y e. RR+ y < x
2 ltso 
 |-  < Or RR
3 2 a1i 
 |-  ( A. x e. RR+ E. y e. RR+ y < x -> < Or RR )
4 0red 
 |-  ( A. x e. RR+ E. y e. RR+ y < x -> 0 e. RR )
5 0red 
 |-  ( z e. RR+ -> 0 e. RR )
6 rpre 
 |-  ( z e. RR+ -> z e. RR )
7 rpge0 
 |-  ( z e. RR+ -> 0 <_ z )
8 5 6 7 lensymd 
 |-  ( z e. RR+ -> -. z < 0 )
9 8 adantl 
 |-  ( ( A. x e. RR+ E. y e. RR+ y < x /\ z e. RR+ ) -> -. z < 0 )
10 elrp 
 |-  ( z e. RR+ <-> ( z e. RR /\ 0 < z ) )
11 breq2 
 |-  ( x = z -> ( y < x <-> y < z ) )
12 11 rexbidv 
 |-  ( x = z -> ( E. y e. RR+ y < x <-> E. y e. RR+ y < z ) )
13 12 rspcv 
 |-  ( z e. RR+ -> ( A. x e. RR+ E. y e. RR+ y < x -> E. y e. RR+ y < z ) )
14 10 13 sylbir 
 |-  ( ( z e. RR /\ 0 < z ) -> ( A. x e. RR+ E. y e. RR+ y < x -> E. y e. RR+ y < z ) )
15 14 impcom 
 |-  ( ( A. x e. RR+ E. y e. RR+ y < x /\ ( z e. RR /\ 0 < z ) ) -> E. y e. RR+ y < z )
16 3 4 9 15 eqinfd 
 |-  ( A. x e. RR+ E. y e. RR+ y < x -> inf ( RR+ , RR , < ) = 0 )
17 1 16 ax-mp 
 |-  inf ( RR+ , RR , < ) = 0