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 ( 𝐴 ∈ 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 𝐴 )