---

Step * 1 1 of Lemma square-between


1. a : {a:ℚ| 0 ≤ a} 
2. b : {b:ℚ| a < b} 
3. qrep(a) = a ∈ ℚ
4. qrep(b) = b ∈ ℚ
5. qrep(a) ∈ ℤ × ℕ+
6. qrep(b) ∈ ℤ × ℕ+
7. c1 : ℤ
8. c2 : ℕ+
9. qrep(a) = <c1, c2> ∈ (ℤ × ℕ+)
10. d1 : ℤ
11. d2 : ℕ+
12. qrep(b) = <d1, d2> ∈ (ℤ × ℕ+)
13. 0 ≤ c1
⊢ ∃r:ℚ [(<c1, c2> < r * r < <d1, d2> ∧ 0 < r)]
BY
{ ((Assert c1 * d2 < d1 * c2 BY
          ((Assert <c1, c2> < <d1, d2> BY
                  (RevHypSubst' (-5) 0
                   THEN RevHypSubst' (-2) 0
                   THEN ((HypSubst 3 0 THENM HypSubst 4 0) THEN Auto THEN D 2 THEN Unhide THEN Auto)⋅))
           THEN ((RW assert_pushupC (-1)⋅ THENA Auto)
                 THEN RepUR ``q_less`` (-1)
                 THEN (Assert 0 < c2 * d2 BY
                             Auto)
                 THEN (SplitOnHypITE -2  THENM RW assert_pushdownC (-3))
                 THEN Auto)⋅
           ))⋅
   THEN ThinVar `b'
   THEN ThinVar `a'
   THEN RenameVar `a' 1
   THEN RenameVar `b' 2
   THEN RenameVar `c' 3
   THEN RenameVar `d' 4)⋅ }

1
1. a : ℤ
2. b : ℕ+
3. c : ℤ
4. d : ℕ+
5. 0 ≤ a
6. a * d < c * b
⊢ ∃r:ℚ [(<a, b> < r * r < <c, d> ∧ 0 < r)]

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbQ{}|  0  \mleq{}  a\} 
2.  b  :  \{b:\mBbbQ{}|  a  <  b\} 
3.  qrep(a)  =  a
4.  qrep(b)  =  b
5.  qrep(a)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
6.  qrep(b)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
7.  c1  :  \mBbbZ{}
8.  c2  :  \mBbbN{}\msupplus{}
9.  qrep(a)  =  <c1,  c2>
10.  d1  :  \mBbbZ{}
11.  d2  :  \mBbbN{}\msupplus{}
12.  qrep(b)  =  <d1,  d2>
13.  0  \mleq{}  c1
\mvdash{}  \mexists{}r:\mBbbQ{}  [(<c1,  c2>  <  r  *  r  <  <d1,  d2>  \mwedge{}  0  <  r)]


By

---

Latex:
((Assert  c1  *  d2  <  d1  *  c2  BY
                ((Assert  <c1,  c2>  <  <d1,  d2>  BY
                                (RevHypSubst'  (-5)  0
                                  THEN  RevHypSubst'  (-2)  0
                                  THEN  ((HypSubst  3  0  THENM  HypSubst  4  0)  THEN  Auto  THEN  D  2  THEN  Unhide  THEN  Auto)
                                  \mcdot{}))
                  THEN  ((RW  assert\_pushupC  (-1)\mcdot{}  THENA  Auto)
                              THEN  RepUR  ``q\_less``  (-1)
                              THEN  (Assert  0  <  c2  *  d2  BY
                                                      Auto)
                              THEN  (SplitOnHypITE  -2    THENM  RW  assert\_pushdownC  (-3))
                              THEN  Auto)\mcdot{}
                  ))\mcdot{}
  THEN  ThinVar  `b'
  THEN  ThinVar  `a'
  THEN  RenameVar  `a'  1
  THEN  RenameVar  `b'  2
  THEN  RenameVar  `c'  3
  THEN  RenameVar  `d'  4)\mcdot{}

---

Home Index