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