---

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


1. a : ℝ
2. b : ℝ
3. r0 ≤ a
4. r0 ≤ b
5. (b * b) < a
⊢ b < rsqrt(a)
BY
{ (((InstLemma `rsqrt_squared` [⌜a⌝]⋅ THENA Auto) THEN (InstLemma `rsqrt_nonneg` [⌜a⌝]⋅ THENA Auto))
   THEN (RepeatFor 2 (MoveToConcl (-1)) THEN (GenConcl ⌜rsqrt(a) = c ∈ ℝ⌝⋅ THENA Auto) THEN Thin (-1) THEN Auto)
   THEN (Assert (b * b) < (c * c) BY
               Auto)
   THEN ThinVar `a') }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  r0  \mleq{}  a
4.  r0  \mleq{}  b
5.  (b  *  b)  <  a
\mvdash{}  b  <  rsqrt(a)


By

---

Latex:
(((InstLemma  `rsqrt\_squared`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (InstLemma  `rsqrt\_nonneg`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (RepeatFor  2  (MoveToConcl  (-1))
              THEN  (GenConcl  \mkleeneopen{}rsqrt(a)  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-1)
              THEN  Auto)
  THEN  (Assert  (b  *  b)  <  (c  *  c)  BY
                          Auto)
  THEN  ThinVar  `a')

---

Home Index