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

Theorem subhalfnqq 6569
 Description: There is a number which is less than half of any positive fraction. The case where 𝐴 is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 6565). (Contributed by Jim Kingdon, 25-Nov-2019.)
Assertion
Ref Expression
subhalfnqq (𝐴Q → ∃𝑥Q (𝑥 +Q 𝑥) <Q 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem subhalfnqq
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 halfnqq 6565 . . . . . 6 (𝐴Q → ∃𝑦Q (𝑦 +Q 𝑦) = 𝐴)
2 df-rex 2329 . . . . . . 7 (∃𝑦Q (𝑦 +Q 𝑦) = 𝐴 ↔ ∃𝑦(𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴))
3 halfnqq 6565 . . . . . . . . . 10 (𝑦Q → ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦)
43adantr 265 . . . . . . . . 9 ((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) → ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦)
54ancli 310 . . . . . . . 8 ((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) → ((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦))
65eximi 1507 . . . . . . 7 (∃𝑦(𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) → ∃𝑦((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦))
72, 6sylbi 118 . . . . . 6 (∃𝑦Q (𝑦 +Q 𝑦) = 𝐴 → ∃𝑦((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦))
81, 7syl 14 . . . . 5 (𝐴Q → ∃𝑦((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦))
9 df-rex 2329 . . . . . . 7 (∃𝑥Q (𝑥 +Q 𝑥) = 𝑦 ↔ ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦))
109anbi2i 438 . . . . . 6 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦) ↔ ((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)))
1110exbii 1512 . . . . 5 (∃𝑦((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥Q (𝑥 +Q 𝑥) = 𝑦) ↔ ∃𝑦((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)))
128, 11sylib 131 . . . 4 (𝐴Q → ∃𝑦((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)))
13 exdistr 1803 . . . 4 (∃𝑦𝑥((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) ↔ ∃𝑦((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)))
1412, 13sylibr 141 . . 3 (𝐴Q → ∃𝑦𝑥((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)))
15 simprl 491 . . . . . 6 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → 𝑥Q)
16 simpll 489 . . . . . . . . 9 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → 𝑦Q)
17 ltaddnq 6562 . . . . . . . . 9 ((𝑦Q𝑦Q) → 𝑦 <Q (𝑦 +Q 𝑦))
1816, 16, 17syl2anc 397 . . . . . . . 8 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → 𝑦 <Q (𝑦 +Q 𝑦))
19 breq2 3795 . . . . . . . . 9 ((𝑦 +Q 𝑦) = 𝐴 → (𝑦 <Q (𝑦 +Q 𝑦) ↔ 𝑦 <Q 𝐴))
2019ad2antlr 466 . . . . . . . 8 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → (𝑦 <Q (𝑦 +Q 𝑦) ↔ 𝑦 <Q 𝐴))
2118, 20mpbid 139 . . . . . . 7 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → 𝑦 <Q 𝐴)
22 breq1 3794 . . . . . . . 8 ((𝑥 +Q 𝑥) = 𝑦 → ((𝑥 +Q 𝑥) <Q 𝐴𝑦 <Q 𝐴))
2322ad2antll 468 . . . . . . 7 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → ((𝑥 +Q 𝑥) <Q 𝐴𝑦 <Q 𝐴))
2421, 23mpbird 160 . . . . . 6 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → (𝑥 +Q 𝑥) <Q 𝐴)
2515, 24jca 294 . . . . 5 (((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → (𝑥Q ∧ (𝑥 +Q 𝑥) <Q 𝐴))
2625eximi 1507 . . . 4 (∃𝑥((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) <Q 𝐴))
2726exlimiv 1505 . . 3 (∃𝑦𝑥((𝑦Q ∧ (𝑦 +Q 𝑦) = 𝐴) ∧ (𝑥Q ∧ (𝑥 +Q 𝑥) = 𝑦)) → ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) <Q 𝐴))
2814, 27syl 14 . 2 (𝐴Q → ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) <Q 𝐴))
29 df-rex 2329 . 2 (∃𝑥Q (𝑥 +Q 𝑥) <Q 𝐴 ↔ ∃𝑥(𝑥Q ∧ (𝑥 +Q 𝑥) <Q 𝐴))
3028, 29sylibr 141 1 (𝐴Q → ∃𝑥Q (𝑥 +Q 𝑥) <Q 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   = wceq 1259  ∃wex 1397   ∈ wcel 1409  ∃wrex 2324   class class class wbr 3791  (class class class)co 5539  Qcnq 6435   +Q cplq 6437
 Copyright terms: Public domain W3C validator