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