---

Step * 1 1 1 1 of Lemma Machin-lemma

.....aux..... 
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)
⊢ (r1 - (r1/r(5))^2) = (r(24)/r(25))
BY
{ ((RWO "rnexp-rdiv<" 0 THENA Auto) THEN RWO "rnexp-int" 0 THEN Auto THEN Try ((RWO "rnexp-int" 0 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
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)
⊢ (r1 - (r(1^2)/r(5^2))) = (r(24)/r(25))

---

Latex:

---

Latex:
.....aux..... 
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(2)  *  rtan(a)/r1  -  rtan(a)\^{}2)
\mvdash{}  (r1  -  (r1/r(5))\^{}2)  =  (r(24)/r(25))


By

---

Latex:
((RWO  "rnexp-rdiv<"  0  THENA  Auto)
  THEN  RWO  "rnexp-int"  0
  THEN  Auto
  THEN  Try  ((RWO  "rnexp-int"  0  THEN  Auto)))

---

Home Index