Hi Adem,indeed * is defined for complex numbers. The way to have it back (for natural arguments) as a natural number is via Mizar functor clusters (functor registrations). See http://mmlquery.mizar.org/mml/4.100.1011/nat_1.html#FC2 it "registers" the result of multiplication to be natural for natural arguments. You have to include the article (NAT_1) with the required cluster into your "registrations" environmental directive, otherwise it will not work.
It is quite a black art to find the right clusters, most people just grep the Mizar abstracts, MMLQuery (http://mmlquery.mizar.org/mmlquery/three.html) is very useful if you learn some of its input syntax.
Josef(Giving cc to Mizar forum, it is better to ask such questions there, so that people could search for the previous answers)
On Wed, 9 Apr 2008, Ozyavas, Adem wrote:
Mr. Urban,
I have started learning and using mizar for the past one month. I got stuck with a
concept while working on a proof. If you could answer I would appreciate it:
how do you "cast" a complex number, for example, back to a natural number? I was using
"divides" predicate which (to my knowledge) requires Nat or Integer. But if the right
hand side of the computation yields a complex or real number, how do I make divides
work for that?
for n being Nat holds 2 divides n*(n+1)
* is defined for real and complex numbers the way I searched the MML. Again, I really
appreciate that.
Adem Ozyavas