---

Step * of Lemma square-between

∀a:{a:ℚ| 0 ≤ a} . ∀b:{b:ℚ| a < b} .  (∃r:ℚ [(a < r * r < b ∧ 0 < r)])
BY
{ (Auto
   THEN ((InstLemma `equals-qrep` [⌜a⌝]⋅ THENA Auto) THEN (RevHypSubst (-1) 0 THENA Auto))
   THEN (InstLemma `equals-qrep` [⌜b⌝]⋅ THENA Auto)
   THEN (RevHypSubst (-1) 0 THENA Auto)
   THEN (InstLemma `qrep-denom` [⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `qrep-denom` [⌜b⌝]⋅ THENA Auto)
   THEN (GenConclAtAddr [2;1;1] THEN RenameVar `c' (-2) THEN D -2)
   THEN GenConclAtAddr [2;1; 3]
   THEN RenameVar `d' (-2)
   THEN D -2) }

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> ∈ (ℤ × ℕ+)
⊢ ∃r:ℚ [(<c1, c2> < r * r < <d1, d2> ∧ 0 < r)]

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbQ{}|  0  \mleq{}  a\}  .  \mforall{}b:\{b:\mBbbQ{}|  a  <  b\}  .    (\mexists{}r:\mBbbQ{}  [(a  <  r  *  r  <  b  \mwedge{}  0  <  r)])


By

---

Latex:
(Auto
  THEN  ((InstLemma  `equals-qrep`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RevHypSubst  (-1)  0  THENA  Auto))
  THEN  (InstLemma  `equals-qrep`  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RevHypSubst  (-1)  0  THENA  Auto)
  THEN  (InstLemma  `qrep-denom`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `qrep-denom`  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddr  [2;1;1]  THEN  RenameVar  `c'  (-2)  THEN  D  -2)
  THEN  GenConclAtAddr  [2;1;  3]
  THEN  RenameVar  `d'  (-2)
  THEN  D  -2)

---

Home Index