Step
*
2
of Lemma
fun_exp_add_sq
.....upcase..... 
1. n : ℤ
2. 0 < n
3. ∀[m:ℕ]. ∀[f,i:Top].  (f^(n - 1) + m i ~ f^n - 1 (f^m i))
⊢ ∀[m:ℕ]. ∀[f,i:Top].  (f^n + m i ~ f^n (f^m i))
BY
{ (UnivCD THENA Auto) }
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 + m i ~ f^n (f^m i)
Latex:
Latex:
.....upcase..... 
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))
\mvdash{}  \mforall{}[m:\mBbbN{}].  \mforall{}[f,i:Top].    (f\^{}n  +  m  i  \msim{}  f\^{}n  (f\^{}m  i))
By
Latex:
(UnivCD  THENA  Auto)
Home
Index