---

Step * of Lemma arctangent-reduction-1

∀x:{x:ℝ| r(-1) < x} . (arctangent(x) = (MachinPi4() + arctangent((x - r1/r1 + x))))
BY
{ (Auto THEN (InstLemma `arctangent-reduction` [⌜r1⌝;⌜x⌝]⋅ THENA Auto)) }

1
.....wf..... 
1. x : {x:ℝ| r(-1) < x} 
⊢ x ∈ {x:ℝ| (r(-1)/r1) < x} 

2
1. x : {x:ℝ| r(-1) < x} 
2. arctangent(x) = (arctangent(r1) + arctangent((x - r1/r1 + (x * r1))))
⊢ arctangent(x) = (MachinPi4() + arctangent((x - r1/r1 + x)))

---

Latex:

---

Latex:
\mforall{}x:\{x:\mBbbR{}|  r(-1)  <  x\}  .  (arctangent(x)  =  (MachinPi4()  +  arctangent((x  -  r1/r1  +  x))))


By

---

Latex:
(Auto  THEN  (InstLemma  `arctangent-reduction`  [\mkleeneopen{}r1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index