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 ∈ 𝑸 → ∃ x x < 𝑸 A

Proof

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