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

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