There's a problem in your translation. Let's forget about the quantifiers for the bit, and ask how to translate 'if a is negative and b is negative then a x b is positive'.
You have something like:
Na & Nb & Tab → ¬Nc
But where does c come from? We want to say that c is the result of multiplying a and b, and Tab doesn't tell us this.
Instead, we need a ternary relation to say 'a x b is c', let's call that 'Tabc'.
Then, we get as the translation of 'if a is negative and b is negative then a x b is positive' the following:
∀x(Na & Nb & Tabx → ¬Nx)
(Why do we need the quantifier? Because, for all we've said about T, it might be that more than one number is the result of multiplying a and b. Ideally, we'd want to write down some more sentences which tell us that there's always exactly one answer.)
Then to translate that the product of any negative numbers is positive, we do:
(1) ∀x∀y∀z(Nx & Ny & Txyz → ¬Nz)
A functional approach
Alternatively, we can consider versions of logic which feature function symbols. A n-ary function symbol f (compared with an n-ary predicate) is such that, whenever a1,...,an are terms (e.g. variables or constants) then f(a1,...,an) is a term as well.
It's then very natural to translate your sentence into a language with a function for multiplication. We let T be a binary function so that 'T(x,y)' means 'x times y' (in fact, given this, we can straightforwardly abbreviate this as x x y).
Then the translation of the sentence would be much simpler:
(2) ∀x ∀y( Nx & Ny → ¬N(T(x,y)))
Now, how would we prove either of these? The answer is, we can't, not if we're trying to do a proof in pure logic, as you are trying to. That's because the fact that (1) and (2) are true is not a matter of pure logic – that is, it is not a matter purely of the form of the sentences. Instead, it depends on the details of what 'times' and 'negative' mean. (Suppose, for example, that 'N' meant 'is negative', but 'T' meant addition. Then (1) and (2) would be false.)
In order to prove (1) and (2), we need additional facts about negativeness and multiplication, probably in the form of axioms. These will tell us what the properties of these predicates and functions are. We would then use these axioms as additional premises in the proof.
We could try to give some such axioms directly, but it probably wouldn't be very interesting. The reason is that, if we want to give some very basic principles about how these interact, the chances are that something like (1) or (2) would appear in our axioms, so the proof would be a boring one liner.
A more interesting proof – and one which is much closer to how it would actually be done – would be to select some axioms for arithmetic in general, such as the [http://en.wikipedia.org/wiki/Peano_axioms][Peano Axioms].* From these, we then define 'negative' and 'times' [but see edit below], and then prove (1) or (2) (depending on whether we've defined 'times' as a predicate or a function).
.* Actually, the Peano Axioms won't really do without a lot of additional work. The reason is that they're only about positive numbers, but we obviously want to say something about negative numbers. We could either move towards a set of axioms which also tells us about negative numbers, or we could do some tricks to define negative numbers within the positive numbers (this sounds weird, but it can be done in strange ways).
EDIT: Rereading this old-ish answer of mine, I notice I've made a mistake. In particular, in the (first-order) Peano axioms we can't define multiplication. Instead, we need to take multiplication and primitive together with some corresponding axioms. In second-order Peano arithmetic, we can, however, define multiplication as repeated addition.