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\in 𝑸\to \exists xx{<}_{𝑸}A$$

Proof

Step	Hyp	Ref	Expression
1		halfnq	$$⊢A\in 𝑸\to \exists xx{+}_{𝑸}x=A$$
2		eleq1a	$$⊢A\in 𝑸\to \left(x{+}_{𝑸}x=A\to x{+}_{𝑸}x\in 𝑸\right)$$
3		addnqf	$$⊢{+}_{𝑸}:𝑸\times 𝑸⟶𝑸$$
4	3	fdmi	$$⊢\mathrm{dom}{+}_{𝑸}=𝑸\times 𝑸$$
5		0nnq	$$⊢\neg \varnothing \in 𝑸$$
6	4 5	ndmovrcl	$$⊢x{+}_{𝑸}x\in 𝑸\to \left(x\in 𝑸\wedge x\in 𝑸\right)$$
7		ltaddnq	$$⊢\left(x\in 𝑸\wedge x\in 𝑸\right)\to x{<}_{𝑸}\left(x{+}_{𝑸}x\right)$$
8	6 7	syl	$$⊢x{+}_{𝑸}x\in 𝑸\to x{<}_{𝑸}\left(x{+}_{𝑸}x\right)$$
9	2 8	syl6	$$⊢A\in 𝑸\to \left(x{+}_{𝑸}x=A\to x{<}_{𝑸}\left(x{+}_{𝑸}x\right)\right)$$
10		breq2	$$⊢x{+}_{𝑸}x=A\to \left(x{<}_{𝑸}\left(x{+}_{𝑸}x\right)\leftrightarrow x{<}_{𝑸}A\right)$$
11	9 10	mpbidi	$$⊢A\in 𝑸\to \left(x{+}_{𝑸}x=A\to x{<}_{𝑸}A\right)$$
12	11	eximdv	$$⊢A\in 𝑸\to \left(\exists xx{+}_{𝑸}x=A\to \exists xx{<}_{𝑸}A\right)$$
13	1 12	mpd	$$⊢A\in 𝑸\to \exists xx{<}_{𝑸}A$$