Step
*
of Lemma
rroot_functionality
∀[i:{2...}]. ∀[x:{x:ℝ| (↑isEven(i)) 
⇒ (r0 ≤ x)} ]. ∀[y:ℝ].  rroot(i;x) = rroot(i;y) supposing x = y
BY
{ (Auto
   THEN (Assert (↑isEven(i)) 
⇒ (r0 ≤ y) BY
               (Auto THEN D 2 THEN Unhide THEN Auto))
   THEN (GenConclTerm ⌜rroot(i;x)⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜rroot(i;y)⌝⋅ THENA Auto)
   THEN DSetVars
   THEN Unhide
   THEN Auto
   THEN (Assert v^i = v1^i BY
               Auto)) }
1
1. i : {2...}
2. x : ℝ
3. (↑isEven(i)) 
⇒ (r0 ≤ x)
4. y : ℝ
5. x = y
6. (↑isEven(i)) 
⇒ (r0 ≤ y)
7. v : ℝ@i
8. (↑isEven(i)) 
⇒ (r0 ≤ v)@i
9. v^i = x@i
10. rroot(i;x) = v ∈ {y:ℝ| ((↑isEven(i)) 
⇒ (r0 ≤ y)) ∧ (y^i = x)} @i
11. v1 : ℝ@i
12. (↑isEven(i)) 
⇒ (r0 ≤ v1)@i
13. v1^i = y@i
14. rroot(i;y) = v1 ∈ {y1:ℝ| ((↑isEven(i)) 
⇒ (r0 ≤ y1)) ∧ (y1^i = y)} @i
15. v^i = v1^i
⊢ v = v1
Latex:
Latex:
\mforall{}[i:\{2...\}].  \mforall{}[x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  ].  \mforall{}[y:\mBbbR{}].    rroot(i;x)  =  rroot(i;y)  supposing  x  =  y
By
Latex:
(Auto
  THEN  (Assert  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  y)  BY
                          (Auto  THEN  D  2  THEN  Unhide  THEN  Auto))
  THEN  (GenConclTerm  \mkleeneopen{}rroot(i;x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}rroot(i;y)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  DSetVars
  THEN  Unhide
  THEN  Auto
  THEN  (Assert  v\^{}i  =  v1\^{}i  BY
                          Auto))
Home
Index