---

Step * 1 1 of Lemma isqrt-non-decreasing


1. x : ℕ
2. y : ℕ
3. x ≤ y
4. (isqrt(y) + 1) ≤ isqrt(x)
5. ((isqrt(y) + 1) * (isqrt(y) + 1)) ≤ (isqrt(x) * isqrt(x))
6. y < (isqrt(y) + 1) * (isqrt(y) + 1)
7. (isqrt(x) * isqrt(x)) ≤ x
⊢ isqrt(x) ≤ isqrt(y)
BY
{ TACTIC:Auto' }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
2.  y  :  \mBbbN{}
3.  x  \mleq{}  y
4.  (isqrt(y)  +  1)  \mleq{}  isqrt(x)
5.  ((isqrt(y)  +  1)  *  (isqrt(y)  +  1))  \mleq{}  (isqrt(x)  *  isqrt(x))
6.  y  <  (isqrt(y)  +  1)  *  (isqrt(y)  +  1)
7.  (isqrt(x)  *  isqrt(x))  \mleq{}  x
\mvdash{}  isqrt(x)  \mleq{}  isqrt(y)


By

---

Latex:
TACTIC:Auto'

---

Home Index