---

Step * of Lemma arctan_wf1

∀[x:ℝ]. (arctan(x) ∈ {y:ℝ| y = arctangent(x)} )
BY
{ ((Assert ∀x:ℝ. (r0 < (r1 + x^2)) BY
          (Auto THEN (Assert r0 ≤ x^2 BY EAuto 1) THEN RWO "-1<" 0 THEN Auto))
   THEN Auto
   THEN (InstLemma `approx-arg_wf` [⌜λ2x.full-arctan(x)⌝;⌜λ2x.(r1/r1 + x^2)⌝;⌜1⌝;⌜x⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. ∀x:ℝ. (r0 < (r1 + x^2))
2. x : ℝ
⊢ d(full-arctan(x))/dx = λx.(r1/r1 + x^2) on (-∞, ∞)

2
1. ∀x:ℝ. (r0 < (r1 + x^2))
2. x : ℝ
3. x1 : ℝ
⊢ |(r1/r1 + x1^2)| ≤ r1

3
1. ∀x:ℝ. (r0 < (r1 + x^2))
2. x : ℝ
3. approx-arg(λ2x.full-arctan(x);1;x) ∈ {y:ℝ| y = full-arctan(x)} 
⊢ arctan(x) ∈ {y:ℝ| y = arctangent(x)} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (arctan(x)  \mmember{}  \{y:\mBbbR{}|  y  =  arctangent(x)\}  )


By

---

Latex:
((Assert  \mforall{}x:\mBbbR{}.  (r0  <  (r1  +  x\^{}2))  BY
                (Auto  THEN  (Assert  r0  \mleq{}  x\^{}2  BY  EAuto  1)  THEN  RWO  "-1<"  0  THEN  Auto))
  THEN  Auto
  THEN  (InstLemma  `approx-arg\_wf`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.full-arctan(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/r1  +  x\^{}2)\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index