---

Step * 1 of Lemma MachinPi4_wf


4 * atan(5;(r1)/5) - atan(239;(r1)/239) ∈ {x:ℝ| x = (π/r(4))} 
BY
{ ((GenConclTerm ⌜atan(5;(r1)/5)⌝⋅
    THENA (Auto THEN (RWO "int-rdiv-req" 0 THEN Auto) THEN RWO "rabs-of-nonneg" 0 THEN Auto)
    )
   THEN (GenConclTerm ⌜atan(239;(r1)/239)⌝⋅
         THENA (Auto THEN (RWO "int-rdiv-req" 0 THEN Auto) THEN RWO "rabs-of-nonneg" 0 THEN Auto)
         )
   THEN DSetVars
   THEN MemTypeCD
   THEN Auto) }

1
.....set predicate..... 
1. v : ℝ
2. arctangent((r1)/5) = v
3. atan(5;(r1)/5) = v ∈ {y:ℝ| arctangent((r1)/5) = y} 
4. v1 : ℝ
5. arctangent((r1)/239) = v1
6. atan(239;(r1)/239) = v1 ∈ {y:ℝ| arctangent((r1)/239) = y} 
⊢ (4 * v - v1) = (π/r(4))

---

Latex:

---

Latex:

4  *  atan(5;(r1)/5)  -  atan(239;(r1)/239)  \mmember{}  \{x:\mBbbR{}|  x  =  (\mpi{}/r(4))\} 


By

---

Latex:
((GenConclTerm  \mkleeneopen{}atan(5;(r1)/5)\mkleeneclose{}\mcdot{}
    THENA  (Auto  THEN  (RWO  "int-rdiv-req"  0  THEN  Auto)  THEN  RWO  "rabs-of-nonneg"  0  THEN  Auto)
    )
  THEN  (GenConclTerm  \mkleeneopen{}atan(239;(r1)/239)\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  (RWO  "int-rdiv-req"  0  THEN  Auto)  THEN  RWO  "rabs-of-nonneg"  0  THEN  Auto)
              )
  THEN  DSetVars
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index