Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltbtwnnqq GIF version

Theorem ltbtwnnqq 7230
 Description: There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by Jim Kingdon, 24-Sep-2019.)
Assertion
Ref Expression
ltbtwnnqq (𝐴 <Q 𝐵 ↔ ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ltbtwnnqq
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 7180 . . . . 5 <Q ⊆ (Q × Q)
21brel 4591 . . . 4 (𝐴 <Q 𝐵 → (𝐴Q𝐵Q))
32simpld 111 . . 3 (𝐴 <Q 𝐵𝐴Q)
4 ltexnqi 7224 . . 3 (𝐴 <Q 𝐵 → ∃𝑦Q (𝐴 +Q 𝑦) = 𝐵)
5 nsmallnq 7228 . . . . . 6 (𝑦Q → ∃𝑧 𝑧 <Q 𝑦)
61brel 4591 . . . . . . . . . . . . . . 15 (𝑧 <Q 𝑦 → (𝑧Q𝑦Q))
76simpld 111 . . . . . . . . . . . . . 14 (𝑧 <Q 𝑦𝑧Q)
8 ltaddnq 7222 . . . . . . . . . . . . . 14 ((𝐴Q𝑧Q) → 𝐴 <Q (𝐴 +Q 𝑧))
97, 8sylan2 284 . . . . . . . . . . . . 13 ((𝐴Q𝑧 <Q 𝑦) → 𝐴 <Q (𝐴 +Q 𝑧))
109ancoms 266 . . . . . . . . . . . 12 ((𝑧 <Q 𝑦𝐴Q) → 𝐴 <Q (𝐴 +Q 𝑧))
1110adantr 274 . . . . . . . . . . 11 (((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) → 𝐴 <Q (𝐴 +Q 𝑧))
12 ltanqi 7217 . . . . . . . . . . . . 13 ((𝑧 <Q 𝑦𝐴Q) → (𝐴 +Q 𝑧) <Q (𝐴 +Q 𝑦))
1312adantr 274 . . . . . . . . . . . 12 (((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝐴 +Q 𝑧) <Q (𝐴 +Q 𝑦))
14 breq2 3933 . . . . . . . . . . . . 13 ((𝐴 +Q 𝑦) = 𝐵 → ((𝐴 +Q 𝑧) <Q (𝐴 +Q 𝑦) ↔ (𝐴 +Q 𝑧) <Q 𝐵))
1514adantl 275 . . . . . . . . . . . 12 (((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) → ((𝐴 +Q 𝑧) <Q (𝐴 +Q 𝑦) ↔ (𝐴 +Q 𝑧) <Q 𝐵))
1613, 15mpbid 146 . . . . . . . . . . 11 (((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝐴 +Q 𝑧) <Q 𝐵)
17 addclnq 7190 . . . . . . . . . . . . . . 15 ((𝐴Q𝑧Q) → (𝐴 +Q 𝑧) ∈ Q)
187, 17sylan2 284 . . . . . . . . . . . . . 14 ((𝐴Q𝑧 <Q 𝑦) → (𝐴 +Q 𝑧) ∈ Q)
1918ancoms 266 . . . . . . . . . . . . 13 ((𝑧 <Q 𝑦𝐴Q) → (𝐴 +Q 𝑧) ∈ Q)
2019adantr 274 . . . . . . . . . . . 12 (((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝐴 +Q 𝑧) ∈ Q)
21 breq2 3933 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 +Q 𝑧) → (𝐴 <Q 𝑥𝐴 <Q (𝐴 +Q 𝑧)))
22 breq1 3932 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 +Q 𝑧) → (𝑥 <Q 𝐵 ↔ (𝐴 +Q 𝑧) <Q 𝐵))
2321, 22anbi12d 464 . . . . . . . . . . . . 13 (𝑥 = (𝐴 +Q 𝑧) → ((𝐴 <Q 𝑥𝑥 <Q 𝐵) ↔ (𝐴 <Q (𝐴 +Q 𝑧) ∧ (𝐴 +Q 𝑧) <Q 𝐵)))
2423adantl 275 . . . . . . . . . . . 12 ((((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) ∧ 𝑥 = (𝐴 +Q 𝑧)) → ((𝐴 <Q 𝑥𝑥 <Q 𝐵) ↔ (𝐴 <Q (𝐴 +Q 𝑧) ∧ (𝐴 +Q 𝑧) <Q 𝐵)))
2520, 24rspcedv 2793 . . . . . . . . . . 11 (((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) → ((𝐴 <Q (𝐴 +Q 𝑧) ∧ (𝐴 +Q 𝑧) <Q 𝐵) → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
2611, 16, 25mp2and 429 . . . . . . . . . 10 (((𝑧 <Q 𝑦𝐴Q) ∧ (𝐴 +Q 𝑦) = 𝐵) → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵))
27263impa 1176 . . . . . . . . 9 ((𝑧 <Q 𝑦𝐴Q ∧ (𝐴 +Q 𝑦) = 𝐵) → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵))
28273coml 1188 . . . . . . . 8 ((𝐴Q ∧ (𝐴 +Q 𝑦) = 𝐵𝑧 <Q 𝑦) → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵))
29283expia 1183 . . . . . . 7 ((𝐴Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝑧 <Q 𝑦 → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
3029exlimdv 1791 . . . . . 6 ((𝐴Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (∃𝑧 𝑧 <Q 𝑦 → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
315, 30syl5 32 . . . . 5 ((𝐴Q ∧ (𝐴 +Q 𝑦) = 𝐵) → (𝑦Q → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
3231impancom 258 . . . 4 ((𝐴Q𝑦Q) → ((𝐴 +Q 𝑦) = 𝐵 → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
3332rexlimdva 2549 . . 3 (𝐴Q → (∃𝑦Q (𝐴 +Q 𝑦) = 𝐵 → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
343, 4, 33sylc 62 . 2 (𝐴 <Q 𝐵 → ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵))
35 ltsonq 7213 . . . 4 <Q Or Q
3635, 1sotri 4934 . . 3 ((𝐴 <Q 𝑥𝑥 <Q 𝐵) → 𝐴 <Q 𝐵)
3736rexlimivw 2545 . 2 (∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵) → 𝐴 <Q 𝐵)
3834, 37impbii 125 1 (𝐴 <Q 𝐵 ↔ ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∃wrex 2417   class class class wbr 3929  (class class class)co 5774  Qcnq 7095   +Q cplq 7097
 Copyright terms: Public domain W3C validator