---

Step * 2 1 of Lemma fun_exp_add_sq


1. n : ℤ
2. 0 < n
3. ∀[m:ℕ]. ∀[f,i:Top].  (f^(n - 1) + m i ~ f^n - 1 (f^m i))
4. m : ℕ
5. f : Top
6. i : Top
⊢ f^n + m i ~ f^n (f^m i)
BY
{ (((Subst ⌜n ~ (n - 1) + 1⌝ 0⋅ THENL [Auto; Id]) THEN Subst ⌜((n - 1) + 1) + m ~ ((n - 1) + m) + 1⌝ 0⋅)
   THENL [Auto; Id]
) }

1
1. n : ℤ
2. 0 < n
3. ∀[m:ℕ]. ∀[f,i:Top].  (f^(n - 1) + m i ~ f^n - 1 (f^m i))
4. m : ℕ
5. f : Top
6. i : Top
⊢ f^((n - 1) + m) + 1 i ~ f^(n - 1) + 1 (f^m i)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[m:\mBbbN{}].  \mforall{}[f,i:Top].    (f\^{}(n  -  1)  +  m  i  \msim{}  f\^{}n  -  1  (f\^{}m  i))
4.  m  :  \mBbbN{}
5.  f  :  Top
6.  i  :  Top
\mvdash{}  f\^{}n  +  m  i  \msim{}  f\^{}n  (f\^{}m  i)


By

---

Latex:
(((Subst  \mkleeneopen{}n  \msim{}  (n  -  1)  +  1\mkleeneclose{}  0\mcdot{}  THENL  [Auto;  Id])
    THEN  Subst  \mkleeneopen{}((n  -  1)  +  1)  +  m  \msim{}  ((n  -  1)  +  m)  +  1\mkleeneclose{}  0\mcdot{}
    )
  THENL  [Auto;  Id]
)

---

Home Index