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	⊢ ( 𝐴 ∈ Q → ∃ 𝑥 𝑥 <Q 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		halfnq	⊢ ( 𝐴 ∈ Q → ∃ 𝑥 ( 𝑥 +Q 𝑥 ) = 𝐴 )
2		eleq1a	⊢ ( 𝐴 ∈ Q → ( ( 𝑥 +Q 𝑥 ) = 𝐴 → ( 𝑥 +Q 𝑥 ) ∈ Q ) )
3		addnqf	⊢ +Q : ( Q × Q ) ⟶ Q
4	3	fdmi	⊢ dom +Q = ( Q × Q )
5		0nnq	⊢ ¬ ∅ ∈ Q
6	4 5	ndmovrcl	⊢ ( ( 𝑥 +Q 𝑥 ) ∈ Q → ( 𝑥 ∈ Q ∧ 𝑥 ∈ Q ) )
7		ltaddnq	⊢ ( ( 𝑥 ∈ Q ∧ 𝑥 ∈ Q ) → 𝑥 <Q ( 𝑥 +Q 𝑥 ) )
8	6 7	syl	⊢ ( ( 𝑥 +Q 𝑥 ) ∈ Q → 𝑥 <Q ( 𝑥 +Q 𝑥 ) )
9	2 8	syl6	⊢ ( 𝐴 ∈ Q → ( ( 𝑥 +Q 𝑥 ) = 𝐴 → 𝑥 <Q ( 𝑥 +Q 𝑥 ) ) )
10		breq2	⊢ ( ( 𝑥 +Q 𝑥 ) = 𝐴 → ( 𝑥 <Q ( 𝑥 +Q 𝑥 ) ↔ 𝑥 <Q 𝐴 ) )
11	9 10	mpbidi	⊢ ( 𝐴 ∈ Q → ( ( 𝑥 +Q 𝑥 ) = 𝐴 → 𝑥 <Q 𝐴 ) )
12	11	eximdv	⊢ ( 𝐴 ∈ Q → ( ∃ 𝑥 ( 𝑥 +Q 𝑥 ) = 𝐴 → ∃ 𝑥 𝑥 <Q 𝐴 ) )
13	1 12	mpd	⊢ ( 𝐴 ∈ Q → ∃ 𝑥 𝑥 <Q 𝐴 )