[bumbledraven]

> It is "obvious" in the real numbers that if you multiply two numbers and get 0 then one of them must be zero. I doubt you could prove this.

Theorem: If x & y are reals and xy=0, then at least one of x and y is zero.

To see this, assume x and y are both nonzero. Divide both sides of xy=0 by x (this is valid because x is nonzero). Then y=0; contradiction. Therefore, at least one of x and y is zero.

[yequalsx]

First you'd need that the integers are an integral domain and then build up to the fact that the reals are a field. At least that's how I'd go about it. Maybe one can start with the reals themselves. Here's the proof that the integers have no zero divisors:

https://proofwiki.org/wiki/Ring_of_Integers_has_no_Zero_Divi...

[eru]

Are you sure that the assumptions that your proof relies on are more fundamental than than what you are trying to prove?

(Eg if memory serves right, you might use the property you are trying to prove to justify why you can even divide by non-zero x on both sides.)

[JadeNB]

> Are you sure that the assumptions that your proof relies on are more fundamental than than what you are trying to prove?

Yes, at least to the extent that "fundamental-ness" can be defined. It is a well, and probably universally, established convention that the field axioms allowing division by non-0 elements (that is to say, allowing multiplication by arbitrary elements, and multiplicative inversion of non-0 elements) is taken as part of the definition of a field, and the fact that the set of non-0 elements in a field is closed under multiplication as a theorem about fields.

[yequalsx]

I believe the point the person you were responding to was getting at is that the person's proof assumes that the reals are a field. It's not a convention that cancellation holds for fields. It's a theorem one proves about integral domains. That a field is closed under multiplication is not a theorem; it's part of the definition of being a ring.

[JadeNB]

> It's not a convention that cancellation holds for fields. It's a theorem one proves about integral domains. That a field is closed under multiplication is not a theorem; it's part of the definition of being a ring.

Yes, that's what I said. My point was that, between

(A) making an axiom the right to divide in a field by non-0 numbers, and proving the closure of non-0 numbers in a field under multiplication,

and

(B) just making an axiom the closure of non-0 numbers in a field under multiplication,

it is only convention (rooted in the deeper convention of not making an additional axiom out of something we could prove from existing ones) that we choose (A) instead of (B). (Also notice that I was talking about the closure under multiplication of the set of non-0 numbers, which is (usually) not part of the definition, rather than of the entire set, which is indeed always part of the definition.)