---

Step * 1 1 of Lemma full-arctan_wf


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)} 
BY
{ ((RWO "int-rdiv-req" (-1) THENA Auto)
   THEN (Assert r0 < x BY
               (RWO "-1<" 0 THEN Auto))
   THEN GenConclTerms Auto [⌜rless-case(r(2);r(3);4;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. (r1/r(3)) < x
5. r0 < x
6. x1 : r(2) < x
⊢ 2 * MachinPi4() - atan-small((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. (r1/r(3)) < x
5. r0 < x
6. y : x < r(3)
⊢ MachinPi4() + atan-small((x - r1/r1 + 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.  x  :  \mBbbR{}
3.  (r(-1))/2  <  x
4.  x1  :  (r1)/3  <  x
\mvdash{}  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))  \mmember{}  \{y:\mBbbR{}|  y  =  arctangent(x)\} 


By

---

Latex:
((RWO  "int-rdiv-req"  (-1)  THENA  Auto)
  THEN  (Assert  r0  <  x  BY
                          (RWO  "-1<"  0  THEN  Auto))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rless-case(r(2);r(3);4;x)\mkleeneclose{}]\mcdot{}
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index