---

Step * of Lemma Machin-lemma

(π/r(4)) = ((r(4) * arctangent((r1/r(5)))) - arctangent((r1/r(239))))
BY
{ ((Assert rtan(arctangent((r1/r(5)))) = (r1/r(5)) BY
          Auto)
   THEN (Assert arctangent((r1/r(5))) ≤ (r1/r(5)) BY
               (BLemma `arctangent-rleq` THEN Auto))
   THEN (Assert arctangent(r0) < arctangent((r1/r(5))) BY
               (BLemma `arctangent_functionality_wrt_rless` THEN Auto))
   THEN (RWO "arctangent0" (-1) THENA Auto)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN (GenConcl ⌜arctangent((r1/r(5))) = a ∈ {a:ℝ| a ∈ (-(π/2), π/2)} ⌝⋅
         THENA (Auto THEN InstLemma `arctangent-bounds` [⌜(r1/r(5))⌝]⋅ THEN Auto)
         )
   THEN Auto) }

1
1. a : {a:ℝ| a ∈ (-(π/2), π/2)} 
2. arctangent((r1/r(5))) = a ∈ {a:ℝ| a ∈ (-(π/2), π/2)} 
3. rtan(a) = (r1/r(5))
4. a ≤ (r1/r(5))
5. r0 < a
⊢ (π/r(4)) = ((r(4) * a) - arctangent((r1/r(239))))

---

Latex:

---

Latex:
(\mpi{}/r(4))  =  ((r(4)  *  arctangent((r1/r(5))))  -  arctangent((r1/r(239))))


By

---

Latex:
((Assert  rtan(arctangent((r1/r(5))))  =  (r1/r(5))  BY
                Auto)
  THEN  (Assert  arctangent((r1/r(5)))  \mleq{}  (r1/r(5))  BY
                          (BLemma  `arctangent-rleq`  THEN  Auto))
  THEN  (Assert  arctangent(r0)  <  arctangent((r1/r(5)))  BY
                          (BLemma  `arctangent\_functionality\_wrt\_rless`  THEN  Auto))
  THEN  (RWO  "arctangent0"  (-1)  THENA  Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}arctangent((r1/r(5)))  =  a\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  InstLemma  `arctangent-bounds`  [\mkleeneopen{}(r1/r(5))\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  Auto)

---

Home Index