---

Step * of Lemma atan-log_wf

∀[a:{2...}]. ∀[M:ℤ].  (atan-log(a;M) ∈ {k:ℕ| M ≤ (((2 * k) + 3) * a^((2 * k) + 3))} )
BY
{ (Auto THEN Assert  ⌜2 ≤ a^2⌝⋅) }

1
.....assertion..... 
1. a : {2...}
2. M : ℤ
⊢ 2 ≤ a^2

2
1. a : {2...}
2. M : ℤ
3. 2 ≤ a^2
⊢ atan-log(a;M) ∈ {k:ℕ| M ≤ (((2 * k) + 3) * a^((2 * k) + 3))} 

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Assert    \mkleeneopen{}2  \mleq{}  a\^{}2\mkleeneclose{}\mcdot{})

---

Home Index