---

Step * 2 2 of Lemma full-arctan_wf


1. 8 ∈ (r(-1))/2 < r0
2. 16 ∈ (r1)/3 < (r1)/2
3. 4 ∈ r(2) < r(3)
4. ∀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)} ))
5. x : ℝ
6. y : x < r0
⊢ -(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
{ (Assert (r(-1))/2 < -(x) BY
         (RWO "-1" 0 THEN Auto THEN UseWitness ⌜8⌝⋅ THEN Auto)) }

1
1. 8 ∈ (r(-1))/2 < r0
2. 16 ∈ (r1)/3 < (r1)/2
3. 4 ∈ r(2) < r(3)
4. ∀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)} ))
5. x : ℝ
6. y : x < r0
7. (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)} 

---

Latex:

---

Latex:

1.  8  \mmember{}  (r(-1))/2  <  r0
2.  16  \mmember{}  (r1)/3  <  (r1)/2
3.  4  \mmember{}  r(2)  <  r(3)
4.  \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)\}  ))
5.  x  :  \mBbbR{}
6.  y  :  x  <  r0
\mvdash{}  -(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:
(Assert  (r(-1))/2  <  -(x)  BY
              (RWO  "-1"  0  THEN  Auto  THEN  UseWitness  \mkleeneopen{}8\mkleeneclose{}\mcdot{}  THEN  Auto))

---

Home Index