Step
*
1
1
of Lemma
isqrt-of-square
1. z : ℕ
2. ((isqrt(z * z) * isqrt(z * z)) ≤ (z * z)) ∧ z * z < (isqrt(z * z) + 1) * (isqrt(z * z) + 1)
⊢ isqrt(z * z) = z ∈ ℤ
BY
{ ((MoveToConcl (-1) THEN (GenConclTerm ⌜isqrt(z * z)⌝⋅ THENA Auto)) THEN Thin (-1) THEN Auto) }
1
1. z : ℕ
2. v : ℕ
3. (v * v) ≤ (z * z)
4. z * z < (v + 1) * (v + 1)
⊢ v = z ∈ ℤ
Latex:
Latex:
1. z : \mBbbN{}
2. ((isqrt(z * z) * isqrt(z * z)) \mleq{} (z * z)) \mwedge{} z * z < (isqrt(z * z) + 1) * (isqrt(z * z) + 1)
\mvdash{} isqrt(z * z) = z
By
Latex:
((MoveToConcl (-1) THEN (GenConclTerm \mkleeneopen{}isqrt(z * z)\mkleeneclose{}\mcdot{} THENA Auto)) THEN Thin (-1) THEN Auto)
Home
Index