---

Step * 2 of Lemma full-arctan_wf


1. (8 ∈ (r(-1))/2 < r0) ∧ (16 ∈ (r1)/3 < (r1)/2) ∧ (4 ∈ r(2) < r(3))
2. ∀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)} ))
⊢ ∀[x:ℝ]. (full-arctan(x) ∈ {y:ℝ| y = arctangent(x)} )
BY
{ (Auto
   THEN Unfold `full-arctan` 0
   THEN GenConclTerms Auto [⌜rless-case((r(-1))/2;r0;8;x)⌝]⋅
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0) }

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. x1 : (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)} 

2
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)} 

---

Latex:

---

Latex:

1.  (8  \mmember{}  (r(-1))/2  <  r0)  \mwedge{}  (16  \mmember{}  (r1)/3  <  (r1)/2)  \mwedge{}  (4  \mmember{}  r(2)  <  r(3))
2.  \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)\}  ))
\mvdash{}  \mforall{}[x:\mBbbR{}].  (full-arctan(x)  \mmember{}  \{y:\mBbbR{}|  y  =  arctangent(x)\}  )


By

---

Latex:
(Auto
  THEN  Unfold  `full-arctan`  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rless-case((r(-1))/2;r0;8;x)\mkleeneclose{}]\mcdot{}
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index