---

Step * 2 of Lemma atan-log_wf


1. a : {2...}
2. M : ℤ
3. 2 ≤ a^2
⊢ atan-log(a;M) ∈ {k:ℕ| M ≤ (((2 * k) + 3) * a^((2 * k) + 3))} 
BY
{ (Unfold `atan-log` 0 THEN (DoSubsume THEN Auto) THEN (D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \{2...\}
2.  M  :  \mBbbZ{}
3.  2  \mleq{}  a\^{}2
\mvdash{}  atan-log(a;M)  \mmember{}  \{k:\mBbbN{}|  M  \mleq{}  (((2  *  k)  +  3)  *  a\^{}((2  *  k)  +  3))\} 


By

---

Latex:
(Unfold  `atan-log`  0
  THEN  (DoSubsume  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index