---

Step * 1 of Lemma full-arctan_wf

.....assertion..... 
1. (8 ∈ (r(-1))/2 < r0) ∧ (16 ∈ (r1)/3 < (r1)/2) ∧ (4 ∈ r(2) < r(3))
⊢ ∀x:ℝ
    (((r(-1))/2 < x)
    ⇒ (case rless-case((r1)/3;(r1)/2;16;x)
         of inl(_) =>
         case rless-case(r(2);r(3);4;x)
          of inl(_) =>
          2 * MachinPi4() - atan-small((r1/x))
          | inr(_) =>
          MachinPi4() + atan-small((x - r1/r1 + x))
         | inr(_) =>
         atan-small(x) ∈ {y:ℝ| y = arctangent(x)} ))
BY
{ (Intros THEN GenConclTerms Auto [⌜rless-case((r1)/3;(r1)/2;16;x)⌝]⋅ THEN Thin (-1) THEN D -1 THEN Reduce 0) }

1
1. (8 ∈ (r(-1))/2 < r0) ∧ (16 ∈ (r1)/3 < (r1)/2) ∧ (4 ∈ r(2) < r(3))
2. x : ℝ
3. (r(-1))/2 < x
4. x1 : (r1)/3 < x
⊢ case rless-case(r(2);r(3);4;x)
   of inl(_) =>
   2 * MachinPi4() - atan-small((r1/x))
   | inr(_) =>
   MachinPi4() + atan-small((x - r1/r1 + x)) ∈ {y:ℝ| y = arctangent(x)} 

2
1. (8 ∈ (r(-1))/2 < r0) ∧ (16 ∈ (r1)/3 < (r1)/2) ∧ (4 ∈ r(2) < r(3))
2. x : ℝ
3. (r(-1))/2 < x
4. y : x < (r1)/2
⊢ atan-small(x) ∈ {y:ℝ| y = arctangent(x)} 

---

Latex:

---

Latex:
.....assertion..... 
1.  (8  \mmember{}  (r(-1))/2  <  r0)  \mwedge{}  (16  \mmember{}  (r1)/3  <  (r1)/2)  \mwedge{}  (4  \mmember{}  r(2)  <  r(3))
\mvdash{}  \mforall{}x:\mBbbR{}
        (((r(-1))/2  <  x)
        {}\mRightarrow{}  (case  rless-case((r1)/3;(r1)/2;16;x)
                  of  inl($_{}$)  =>
                  case  rless-case(r(2);r(3);4;x)
                    of  inl($_{}$)  =>
                    2  *  MachinPi4()  -  atan-small((r1/x))
                    |  inr($_{}$)  =>
                    MachinPi4()  +  atan-small((x  -  r1/r1  +  x))
                  |  inr($_{}$)  =>
                  atan-small(x)  \mmember{}  \{y:\mBbbR{}|  y  =  arctangent(x)\}  ))


By

---

Latex:
(Intros
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rless-case((r1)/3;(r1)/2;16;x)\mkleeneclose{}]\mcdot{}
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index