---

Step * of Lemma full-arctan_wf

∀[x:ℝ]. (full-arctan(x) ∈ {y:ℝ| y = arctangent(x)} )
BY
{ ((Assert (8 ∈ (r(-1))/2 < r0) ∧ (16 ∈ (r1)/3 < (r1)/2) ∧ (4 ∈ r(2) < r(3)) BY
          Auto)
   THEN Assert ⌜∀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)} ))⌝⋅
   ) }

1
.....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)} ))

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

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (full-arctan(x)  \mmember{}  \{y:\mBbbR{}|  y  =  arctangent(x)\}  )


By

---

Latex:
((Assert  (8  \mmember{}  (r(-1))/2  <  r0)  \mwedge{}  (16  \mmember{}  (r1)/3  <  (r1)/2)  \mwedge{}  (4  \mmember{}  r(2)  <  r(3))  BY
                Auto)
  THEN  Assert  \mkleeneopen{}\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)\}  ))\mkleeneclose{}\mcdot{}
  )

---

Home Index