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

Theorem subhalfnqq 6271
 Description: There is a number which is less than half of any positive fraction. The case where A 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 6267). (Contributed by Jim Kingdon, 25-Nov-2019.)
Assertion
Ref Expression
subhalfnqq (A Qx Q (x +Q x) <Q A)
Distinct variable group:   x,A

Proof of Theorem subhalfnqq
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 halfnqq 6267 . . . . . 6 (A Qy Q (y +Q y) = A)
2 df-rex 2290 . . . . . . 7 (y Q (y +Q y) = Ay(y Q (y +Q y) = A))
3 halfnqq 6267 . . . . . . . . . 10 (y Qx Q (x +Q x) = y)
43adantr 261 . . . . . . . . 9 ((y Q (y +Q y) = A) → x Q (x +Q x) = y)
54ancli 306 . . . . . . . 8 ((y Q (y +Q y) = A) → ((y Q (y +Q y) = A) x Q (x +Q x) = y))
65eximi 1473 . . . . . . 7 (y(y Q (y +Q y) = A) → y((y Q (y +Q y) = A) x Q (x +Q x) = y))
72, 6sylbi 114 . . . . . 6 (y Q (y +Q y) = Ay((y Q (y +Q y) = A) x Q (x +Q x) = y))
81, 7syl 14 . . . . 5 (A Qy((y Q (y +Q y) = A) x Q (x +Q x) = y))
9 df-rex 2290 . . . . . . 7 (x Q (x +Q x) = yx(x Q (x +Q x) = y))
109anbi2i 433 . . . . . 6 (((y Q (y +Q y) = A) x Q (x +Q x) = y) ↔ ((y Q (y +Q y) = A) x(x Q (x +Q x) = y)))
1110exbii 1478 . . . . 5 (y((y Q (y +Q y) = A) x Q (x +Q x) = y) ↔ y((y Q (y +Q y) = A) x(x Q (x +Q x) = y)))
128, 11sylib 127 . . . 4 (A Qy((y Q (y +Q y) = A) x(x Q (x +Q x) = y)))
13 exdistr 1769 . . . 4 (yx((y Q (y +Q y) = A) (x Q (x +Q x) = y)) ↔ y((y Q (y +Q y) = A) x(x Q (x +Q x) = y)))
1412, 13sylibr 137 . . 3 (A Qyx((y Q (y +Q y) = A) (x Q (x +Q x) = y)))
15 simprl 471 . . . . . 6 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → x Q)
16 simpll 469 . . . . . . . . 9 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → y Q)
17 ltaddnq 6265 . . . . . . . . 9 ((y Q y Q) → y <Q (y +Q y))
1816, 16, 17syl2anc 393 . . . . . . . 8 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → y <Q (y +Q y))
19 breq2 3742 . . . . . . . . 9 ((y +Q y) = A → (y <Q (y +Q y) ↔ y <Q A))
2019ad2antlr 462 . . . . . . . 8 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → (y <Q (y +Q y) ↔ y <Q A))
2118, 20mpbid 135 . . . . . . 7 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → y <Q A)
22 breq1 3741 . . . . . . . 8 ((x +Q x) = y → ((x +Q x) <Q Ay <Q A))
2322ad2antll 464 . . . . . . 7 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → ((x +Q x) <Q Ay <Q A))
2421, 23mpbird 156 . . . . . 6 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → (x +Q x) <Q A)
2515, 24jca 290 . . . . 5 (((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → (x Q (x +Q x) <Q A))
2625eximi 1473 . . . 4 (x((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → x(x Q (x +Q x) <Q A))
2726exlimiv 1471 . . 3 (yx((y Q (y +Q y) = A) (x Q (x +Q x) = y)) → x(x Q (x +Q x) <Q A))
2814, 27syl 14 . 2 (A Qx(x Q (x +Q x) <Q A))
29 df-rex 2290 . 2 (x Q (x +Q x) <Q Ax(x Q (x +Q x) <Q A))
3028, 29sylibr 137 1 (A Qx Q (x +Q x) <Q A)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1228  ∃wex 1362   ∈ wcel 1374  ∃wrex 2285   class class class wbr 3738  (class class class)co 5436  Qcnq 6138   +Q cplq 6140
 Copyright terms: Public domain W3C validator