---

Step * of Lemma fun_exp-rem

∀[T:Type]. ∀[f:T ⟶ T]. ∀[x:T]. ∀[n:ℕ+].  ∀[k:ℕ]. ((f^k x) = (f^k rem n x) ∈ T) supposing (f^n x) = x ∈ T
BY
{ (Auto THEN (InstLemma `div_rem_sum` [⌜k⌝;⌜n⌝]⋅ THENA Auto)) }

1
1. T : Type
2. f : T ⟶ T
3. x : T
4. n : ℕ+
5. (f^n x) = x ∈ T
6. k : ℕ
7. k = (((k ÷ n) * n) + (k rem n)) ∈ ℤ
⊢ (f^k x) = (f^k rem n x) ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[x:T].  \mforall{}[n:\mBbbN{}\msupplus{}].    \mforall{}[k:\mBbbN{}].  ((f\^{}k  x)  =  (f\^{}k  rem  n  x))  supposing  (f\^{}n  x)  =  x


By

---

Latex:
(Auto  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index