---

Step * 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> ∈ (ℤ × ℕ+)
⊢ ∃r:ℚ [(<c1, c2> < r * r < <d1, d2> ∧ 0 < r)]
BY
{ (Assert 0 ≤ c1 BY
         ((Assert 0 ≤ <c1, c2> BY
                 (RevHypSubst' (-4) 0 THEN HypSubst' 3 0 THEN Auto THEN D 1 THEN Unhide THEN Auto))
          THEN (RepeatFor 2 (UnfoldTopAb (-1))
                THEN RepUR ``grp_le qadd_grp q_le`` -1
                THEN (CallByValueReduce (-1) THENA Auto)
                THEN RepUR ``qpositive qmul qsub qadd qeq`` -1
                THEN ((CallByValueReduceOn ⌜<c1, c2>⌝ (-1)⋅ THENA Auto) THEN Reduce (-1))
                THEN (CallByValueReduce (-1) THENA Auto)
                THEN Reduce (-1)
                THEN (SimplifyAssert (-1) THENA Auto)
                THEN (D -1 THEN Auto')⋅)⋅
          ))⋅ }

1
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)]

---

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>
\mvdash{}  \mexists{}r:\mBbbQ{}  [(<c1,  c2>  <  r  *  r  <  <d1,  d2>  \mwedge{}  0  <  r)]


By

---

Latex:
(Assert  0  \mleq{}  c1  BY
              ((Assert  0  \mleq{}  <c1,  c2>  BY
                              (RevHypSubst'  (-4)  0  THEN  HypSubst'  3  0  THEN  Auto  THEN  D  1  THEN  Unhide  THEN  Auto))
                THEN  (RepeatFor  2  (UnfoldTopAb  (-1))
                            THEN  RepUR  ``grp\_le  qadd\_grp  q\_le``  -1
                            THEN  (CallByValueReduce  (-1)  THENA  Auto)
                            THEN  RepUR  ``qpositive  qmul  qsub  qadd  qeq``  -1
                            THEN  ((CallByValueReduceOn  \mkleeneopen{}<c1,  c2>\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))
                            THEN  (CallByValueReduce  (-1)  THENA  Auto)
                            THEN  Reduce  (-1)
                            THEN  (SimplifyAssert  (-1)  THENA  Auto)
                            THEN  (D  -1  THEN  Auto')\mcdot{})\mcdot{}
                ))\mcdot{}

---

Home Index