---

Step * 1 1 1 2 3 1 1 1 2 2 1 1 1 1 1 1 2 2 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)
8. r(2) * a ∈ (-(π/2), π/2)
9. rtan(r(2) * a) = (r(5)/r(12))
10. (r(4) * a) ≤ (r(4)/r(5))
11. r0 < (r(4) * a)
12. r(4) * a ∈ (-(π/2), π/2)
13. rtan(r(2) * r(2) * a) = (r(120)/r(119))
14. (r1 - rtan(r(2) * a)^2) = (r(119)/r(144))
15. r1 - rtan(r(2) * a)^2 ≠ r0
16. r(2) * r(2) * a ∈ {x:ℝ| (-(π/2) < x) ∧ (x < π/2)} 
17. (r(2) * rtan(r(2) * a)/(r(119)/r(144))) = (r(120)/r(119))
18. rtan(r(4) * a) = (r(120)/r(119))
19. (r(4) * a) - (π/r(4)) ∈ {x:ℝ| x ∈ (-(π/2), π/2)} 
20. rtan((r(4) * a) - (π/r(4))) = (r1/r(239))
⊢ arctangent((r1/r(239))) = ((r(4) * a) - (π/r(4)))
BY
{ (RWO "-1<" 0 THEN Auto) }

---

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)
8.  r(2)  *  a  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)
9.  rtan(r(2)  *  a)  =  (r(5)/r(12))
10.  (r(4)  *  a)  \mleq{}  (r(4)/r(5))
11.  r0  <  (r(4)  *  a)
12.  r(4)  *  a  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)
13.  rtan(r(2)  *  r(2)  *  a)  =  (r(120)/r(119))
14.  (r1  -  rtan(r(2)  *  a)\^{}2)  =  (r(119)/r(144))
15.  r1  -  rtan(r(2)  *  a)\^{}2  \mneq{}  r0
16.  r(2)  *  r(2)  *  a  \mmember{}  \{x:\mBbbR{}|  (-(\mpi{}/2)  <  x)  \mwedge{}  (x  <  \mpi{}/2)\} 
17.  (r(2)  *  rtan(r(2)  *  a)/(r(119)/r(144)))  =  (r(120)/r(119))
18.  rtan(r(4)  *  a)  =  (r(120)/r(119))
19.  (r(4)  *  a)  -  (\mpi{}/r(4))  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\} 
20.  rtan((r(4)  *  a)  -  (\mpi{}/r(4)))  =  (r1/r(239))
\mvdash{}  arctangent((r1/r(239)))  =  ((r(4)  *  a)  -  (\mpi{}/r(4)))


By

---

Latex:
(RWO  "-1<"  0  THEN  Auto)

---

Home Index