---

Step * 1 1 2 1 1 1 1 1 1 of Lemma rsqrt-irrational


1. v : ℝ
2. v1 : ℝ
3. v2 : ℝ
4. r0 < v
5. r0 ≤ v2
6. r0 ≤ v1
7. v3 : ℝ
8. (v1/v) = v3 ∈ ℝ
9. (v2 * v * v) < (v1 * v1)
10. r0 ≤ v3
11. v2 < (v3 * v3)
⊢ rsqrt(v2) < v3
BY
{ ((Lemmaize [-1;-2;5] THEN Auto) THEN RenameVar `a' 1 THEN RenameVar `b' 2) }

1
1. a : ℝ
2. b : ℝ
3. r0 ≤ a
4. r0 ≤ b
5. a < (b * b)
⊢ rsqrt(a) < b

---

Latex:

---

Latex:

1.  v  :  \mBbbR{}
2.  v1  :  \mBbbR{}
3.  v2  :  \mBbbR{}
4.  r0  <  v
5.  r0  \mleq{}  v2
6.  r0  \mleq{}  v1
7.  v3  :  \mBbbR{}
8.  (v1/v)  =  v3
9.  (v2  *  v  *  v)  <  (v1  *  v1)
10.  r0  \mleq{}  v3
11.  v2  <  (v3  *  v3)
\mvdash{}  rsqrt(v2)  <  v3


By

---

Latex:
((Lemmaize  [-1;-2;5]  THEN  Auto)  THEN  RenameVar  `a'  1  THEN  RenameVar  `b'  2)

---

Home Index