---

Step * 1 1 of Lemma Machin-lemma


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
6. (r(2) * a) ≤ (r(2)/r(5))
7. r0 < (r(2) * a)
⊢ (π/r(4)) = ((r(4) * a) - arctangent((r1/r(239))))
BY
{ ((Assert r(2) * a ∈ (-(π/2), π/2) BY
          (Reduce 0
           THEN (D 0
                 THENL [((RWO "-1<" 0 THEN Auto) THEN UseWitness ⌜2⌝⋅ THEN Auto)
                       ; ((RWO "-2" 0 THEN Auto) THEN UseWitness ⌜2⌝⋅ THEN Auto)]
                )
           ))
   THEN (InstLemma `rtan-double` [⌜a⌝]⋅ THENA 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
6. (r(2) * a) ≤ (r(2)/r(5))
7. r0 < (r(2) * a)
8. r(2) * a ∈ (-(π/2), π/2)
9. rtan(r(2) * a) = (r(2) * rtan(a)/r1 - rtan(a)^2)
⊢ (π/r(4)) = ((r(4) * a) - arctangent((r1/r(239))))

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  a  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\} 
2.  arctangent((r1/r(5)))  =  a
3.  rtan(a)  =  (r1/r(5))
4.  a  \mleq{}  (r1/r(5))
5.  r0  <  a
6.  (r(2)  *  a)  \mleq{}  (r(2)/r(5))
7.  r0  <  (r(2)  *  a)
\mvdash{}  (\mpi{}/r(4))  =  ((r(4)  *  a)  -  arctangent((r1/r(239))))


By

---

Latex:
((Assert  r(2)  *  a  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)  BY
                (Reduce  0
                  THEN  (D  0
                              THENL  [((RWO  "-1<"  0  THEN  Auto)  THEN  UseWitness  \mkleeneopen{}2\mkleeneclose{}\mcdot{}  THEN  Auto)
                                          ;  ((RWO  "-2"  0  THEN  Auto)  THEN  UseWitness  \mkleeneopen{}2\mkleeneclose{}\mcdot{}  THEN  Auto)]
                            )
                  ))
  THEN  (InstLemma  `rtan-double`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index