Metamath Proof Explorer


Theorem nsmallnq

Description: The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion nsmallnq
|- ( A e. Q. -> E. x x 

Proof

Step Hyp Ref Expression
1 halfnq
 |-  ( A e. Q. -> E. x ( x +Q x ) = A )
2 eleq1a
 |-  ( A e. Q. -> ( ( x +Q x ) = A -> ( x +Q x ) e. Q. ) )
3 addnqf
 |-  +Q : ( Q. X. Q. ) --> Q.
4 3 fdmi
 |-  dom +Q = ( Q. X. Q. )
5 0nnq
 |-  -. (/) e. Q.
6 4 5 ndmovrcl
 |-  ( ( x +Q x ) e. Q. -> ( x e. Q. /\ x e. Q. ) )
7 ltaddnq
 |-  ( ( x e. Q. /\ x e. Q. ) -> x 
8 6 7 syl
 |-  ( ( x +Q x ) e. Q. -> x 
9 2 8 syl6
 |-  ( A e. Q. -> ( ( x +Q x ) = A -> x 
10 breq2
 |-  ( ( x +Q x ) = A -> ( x  x 
11 9 10 mpbidi
 |-  ( A e. Q. -> ( ( x +Q x ) = A -> x 
12 11 eximdv
 |-  ( A e. Q. -> ( E. x ( x +Q x ) = A -> E. x x 
13 1 12 mpd
 |-  ( A e. Q. -> E. x x