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

Theorem ltbtwnnq 9679
 Description: There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 17-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ltbtwnnq (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ltbtwnnq
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 9627 . . . . 5 <Q ⊆ (Q × Q)
21brel 5090 . . . 4 (𝐴 <Q 𝐵 → (𝐴Q𝐵Q))
32simprd 478 . . 3 (𝐴 <Q 𝐵𝐵Q)
4 ltexnq 9676 . . . 4 (𝐵Q → (𝐴 <Q 𝐵 ↔ ∃𝑦(𝐴 +Q 𝑦) = 𝐵))
5 eleq1 2676 . . . . . . . . . 10 ((𝐴 +Q 𝑦) = 𝐵 → ((𝐴 +Q 𝑦) ∈ Q𝐵Q))
65biimparc 503 . . . . . . . . 9 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝐴 +Q 𝑦) ∈ Q)
7 addnqf 9649 . . . . . . . . . . 11 +Q :(Q × Q)⟶Q
87fdmi 5965 . . . . . . . . . 10 dom +Q = (Q × Q)
9 0nnq 9625 . . . . . . . . . 10 ¬ ∅ ∈ Q
108, 9ndmovrcl 6718 . . . . . . . . 9 ((𝐴 +Q 𝑦) ∈ Q → (𝐴Q𝑦Q))
116, 10syl 17 . . . . . . . 8 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝐴Q𝑦Q))
1211simprd 478 . . . . . . 7 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → 𝑦Q)
13 nsmallnq 9678 . . . . . . . 8 (𝑦Q → ∃𝑧 𝑧 <Q 𝑦)
1411simpld 474 . . . . . . . . . . . 12 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → 𝐴Q)
151brel 5090 . . . . . . . . . . . . 13 (𝑧 <Q 𝑦 → (𝑧Q𝑦Q))
1615simpld 474 . . . . . . . . . . . 12 (𝑧 <Q 𝑦𝑧Q)
17 ltaddnq 9675 . . . . . . . . . . . 12 ((𝐴Q𝑧Q) → 𝐴 <Q (𝐴 +Q 𝑧))
1814, 16, 17syl2an 493 . . . . . . . . . . 11 (((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) ∧ 𝑧 <Q 𝑦) → 𝐴 <Q (𝐴 +Q 𝑧))
19 ltanq 9672 . . . . . . . . . . . . . 14 (𝐴Q → (𝑧 <Q 𝑦 ↔ (𝐴 +Q 𝑧) <Q (𝐴 +Q 𝑦)))
2019biimpa 500 . . . . . . . . . . . . 13 ((𝐴Q𝑧 <Q 𝑦) → (𝐴 +Q 𝑧) <Q (𝐴 +Q 𝑦))
2114, 20sylan 487 . . . . . . . . . . . 12 (((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) ∧ 𝑧 <Q 𝑦) → (𝐴 +Q 𝑧) <Q (𝐴 +Q 𝑦))
22 simplr 788 . . . . . . . . . . . 12 (((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) ∧ 𝑧 <Q 𝑦) → (𝐴 +Q 𝑦) = 𝐵)
2321, 22breqtrd 4609 . . . . . . . . . . 11 (((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) ∧ 𝑧 <Q 𝑦) → (𝐴 +Q 𝑧) <Q 𝐵)
24 ovex 6577 . . . . . . . . . . . 12 (𝐴 +Q 𝑧) ∈ V
25 breq2 4587 . . . . . . . . . . . . 13 (𝑥 = (𝐴 +Q 𝑧) → (𝐴 <Q 𝑥𝐴 <Q (𝐴 +Q 𝑧)))
26 breq1 4586 . . . . . . . . . . . . 13 (𝑥 = (𝐴 +Q 𝑧) → (𝑥 <Q 𝐵 ↔ (𝐴 +Q 𝑧) <Q 𝐵))
2725, 26anbi12d 743 . . . . . . . . . . . 12 (𝑥 = (𝐴 +Q 𝑧) → ((𝐴 <Q 𝑥𝑥 <Q 𝐵) ↔ (𝐴 <Q (𝐴 +Q 𝑧) ∧ (𝐴 +Q 𝑧) <Q 𝐵)))
2824, 27spcev 3273 . . . . . . . . . . 11 ((𝐴 <Q (𝐴 +Q 𝑧) ∧ (𝐴 +Q 𝑧) <Q 𝐵) → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
2918, 23, 28syl2anc 691 . . . . . . . . . 10 (((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) ∧ 𝑧 <Q 𝑦) → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
3029ex 449 . . . . . . . . 9 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝑧 <Q 𝑦 → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵)))
3130exlimdv 1848 . . . . . . . 8 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (∃𝑧 𝑧 <Q 𝑦 → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵)))
3213, 31syl5 33 . . . . . . 7 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝑦Q → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵)))
3312, 32mpd 15 . . . . . 6 ((𝐵Q ∧ (𝐴 +Q 𝑦) = 𝐵) → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
3433ex 449 . . . . 5 (𝐵Q → ((𝐴 +Q 𝑦) = 𝐵 → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵)))
3534exlimdv 1848 . . . 4 (𝐵Q → (∃𝑦(𝐴 +Q 𝑦) = 𝐵 → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵)))
364, 35sylbid 229 . . 3 (𝐵Q → (𝐴 <Q 𝐵 → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵)))
373, 36mpcom 37 . 2 (𝐴 <Q 𝐵 → ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
38 ltsonq 9670 . . . 4 <Q Or Q
3938, 1sotri 5442 . . 3 ((𝐴 <Q 𝑥𝑥 <Q 𝐵) → 𝐴 <Q 𝐵)
4039exlimiv 1845 . 2 (∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵) → 𝐴 <Q 𝐵)
4137, 40impbii 198 1 (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ 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