---

Step * 1 1 1 of Lemma isqrt-convex

.....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)
BY
{ xxx((RW IntNormC 0 THENA Auto)
      THEN (Assert (isqrt(a) * isqrt(a)) ≤ a BY
                  (InstLemma `isqrt-property` [⌜a⌝]⋅ THEN Auto))
      THEN (RWO "-1" 0 THENA Auto)
      THEN (Assert (isqrt(b) * isqrt(b)) ≤ b BY
                  (InstLemma `isqrt-property` [⌜b⌝]⋅ THEN Auto))
      THEN (RWO "-1" 0 THENA Auto))xxx }

1
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(a)) ≤ a
10. (isqrt(b) * isqrt(b)) ≤ b
⊢ (a + ((-2) * isqrt(a) * isqrt(b)) + b) ≤ (a + ((-1) * b))

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}a
3.  isqrt(b)  \mleq{}  isqrt(a)
4.  (isqrt(b)  +  2)  \mleq{}  isqrt(a)
5.  v  :  \mBbbN{}
6.  isqrt(a  -  b)  =  v
7.  (v  *  v)  \mleq{}  (a  -  b)
8.  a  -  b  <  (v  +  1)  *  (v  +  1)
\mvdash{}  ((isqrt(a)  -  isqrt(b))  *  (isqrt(a)  -  isqrt(b)))  \mleq{}  (a  -  b)


By

---

Latex:
xxx((RW  IntNormC  0  THENA  Auto)
        THEN  (Assert  (isqrt(a)  *  isqrt(a))  \mleq{}  a  BY
                                (InstLemma  `isqrt-property`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto))
        THEN  (RWO  "-1"  0  THENA  Auto)
        THEN  (Assert  (isqrt(b)  *  isqrt(b))  \mleq{}  b  BY
                                (InstLemma  `isqrt-property`  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto))
        THEN  (RWO  "-1"  0  THENA  Auto))xxx

---

Home Index