Step * of Lemma mon_nat_op_op

[g:IAbMonoid]. ∀[n:ℕ]. ∀[a,b:|g|].  ((n ⋅ (a b)) ((n ⋅ a) (n ⋅ b)) ∈ |g|)
BY
THENM THENM NatInd (-1) 
THEN Auto }

1
1. IAbMonoid
2. : ℤ
3. |g|
4. |g|
⊢ (0 ⋅ (a b)) ((0 ⋅ a) (0 ⋅ b)) ∈ |g|

2
1. IAbMonoid
2. : ℤ
3. 0 < n
4. ∀[a,b:|g|].  (((n 1) ⋅ (a b)) (((n 1) ⋅ a) ((n 1) ⋅ b)) ∈ |g|)
5. |g|
6. |g|
⊢ (n ⋅ (a b)) ((n ⋅ a) (n ⋅ b)) ∈ |g|


Latex:


Latex:
\mforall{}[g:IAbMonoid].  \mforall{}[n:\mBbbN{}].  \mforall{}[a,b:|g|].    ((n  \mcdot{}  (a  *  b))  =  ((n  \mcdot{}  a)  *  (n  \mcdot{}  b)))


By


Latex:
D  0  THENM  D  0  THENM  NatInd  (-1) 
THEN  Auto




Home Index