---

Step * 1 1 of Lemma isqrt-convex


1. a : ℕ
2. b : ℕa
3. isqrt(b) ≤ isqrt(a)
4. (isqrt(b) + 2) ≤ isqrt(a)
⊢ (isqrt(a) - isqrt(b)) ≤ isqrt(a - b)
BY
{ xxx((InstLemma `isqrt-property` [⌜a - b⌝]⋅ THENA Auto)
      THEN MoveToConcl (-1)
      THEN GenConclTerm ⌜isqrt(a - b)⌝⋅
      THEN Auto
      THEN Assert ⌜((isqrt(a) - isqrt(b)) * (isqrt(a) - isqrt(b))) ≤ (a - b)⌝⋅)xxx }

1
.....assertion..... 
1. a : ℕ
2. b : ℕa
3. isqrt(b) ≤ isqrt(a)
4. (isqrt(b) + 2) ≤ isqrt(a)
5. v : ℕ
6. isqrt(a - b) = v ∈ ℕ
7. (v * v) ≤ (a - b)
8. a - b < (v + 1) * (v + 1)
⊢ ((isqrt(a) - isqrt(b)) * (isqrt(a) - isqrt(b))) ≤ (a - b)

2
1. a : ℕ
2. b : ℕa
3. isqrt(b) ≤ isqrt(a)
4. (isqrt(b) + 2) ≤ isqrt(a)
5. v : ℕ
6. isqrt(a - b) = v ∈ ℕ
7. (v * v) ≤ (a - b)
8. a - b < (v + 1) * (v + 1)
9. ((isqrt(a) - isqrt(b)) * (isqrt(a) - isqrt(b))) ≤ (a - b)
⊢ (isqrt(a) - isqrt(b)) ≤ v

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}a
3.  isqrt(b)  \mleq{}  isqrt(a)
4.  (isqrt(b)  +  2)  \mleq{}  isqrt(a)
\mvdash{}  (isqrt(a)  -  isqrt(b))  \mleq{}  isqrt(a  -  b)


By

---

Latex:
xxx((InstLemma  `isqrt-property`  [\mkleeneopen{}a  -  b\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  MoveToConcl  (-1)
        THEN  GenConclTerm  \mkleeneopen{}isqrt(a  -  b)\mkleeneclose{}\mcdot{}
        THEN  Auto
        THEN  Assert  \mkleeneopen{}((isqrt(a)  -  isqrt(b))  *  (isqrt(a)  -  isqrt(b)))  \mleq{}  (a  -  b)\mkleeneclose{}\mcdot{})xxx

---

Home Index