Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsmallnq Structured version   Visualization version   GIF version

Theorem nsmallnq 9678
 Description: The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
nsmallnq (𝐴Q → ∃𝑥 𝑥 <Q 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem nsmallnq
StepHypRef Expression
1 halfnq 9677 . 2 (𝐴Q → ∃𝑥(𝑥 +Q 𝑥) = 𝐴)
2 eleq1a 2683 . . . . 5 (𝐴Q → ((𝑥 +Q 𝑥) = 𝐴 → (𝑥 +Q 𝑥) ∈ Q))
3 addnqf 9649 . . . . . . . 8 +Q :(Q × Q)⟶Q
43fdmi 5965 . . . . . . 7 dom +Q = (Q × Q)
5 0nnq 9625 . . . . . . 7 ¬ ∅ ∈ Q
64, 5ndmovrcl 6718 . . . . . 6 ((𝑥 +Q 𝑥) ∈ Q → (𝑥Q𝑥Q))
7 ltaddnq 9675 . . . . . 6 ((𝑥Q𝑥Q) → 𝑥 <Q (𝑥 +Q 𝑥))
86, 7syl 17 . . . . 5 ((𝑥 +Q 𝑥) ∈ Q𝑥 <Q (𝑥 +Q 𝑥))
92, 8syl6 34 . . . 4 (𝐴Q → ((𝑥 +Q 𝑥) = 𝐴𝑥 <Q (𝑥 +Q 𝑥)))
10 breq2 4587 . . . 4 ((𝑥 +Q 𝑥) = 𝐴 → (𝑥 <Q (𝑥 +Q 𝑥) ↔ 𝑥 <Q 𝐴))
119, 10mpbidi 230 . . 3 (𝐴Q → ((𝑥 +Q 𝑥) = 𝐴𝑥 <Q 𝐴))
1211eximdv 1833 . 2 (𝐴Q → (∃𝑥(𝑥 +Q 𝑥) = 𝐴 → ∃𝑥 𝑥 <Q 𝐴))
131, 12mpd 15 1 (𝐴Q → ∃𝑥 𝑥 <Q 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977   class class class wbr 4583   × cxp 5036  (class class class)co 6549  Qcnq 9553   +Q cplq 9556
 Copyright terms: Public domain W3C validator