Step * of Lemma rroot_functionality

[i:{2...}]. ∀[x:{x:ℝ(↑isEven(i))  (r0 ≤ x)} ]. ∀[y:ℝ].  rroot(i;x) rroot(i;y) supposing y
BY
(Auto
   THEN (Assert (↑isEven(i))  (r0 ≤ y) BY
               (Auto THEN 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. {2...}
2. : ℝ
3. (↑isEven(i))  (r0 ≤ x)
4. : ℝ
5. y
6. (↑isEven(i))  (r0 ≤ y)
7. : ℝ@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
⊢ 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