Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Formal Proof Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

 Messages: [ Previous | Next ]
 Joshua Cranmer Posts: 487 Registered: 8/20/08
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 27, 2009 11:09 PM

Andrew Tomazos wrote:
> Isn't q just the GCD of (c + a) and (c - a) ?
>
> It's clear that b*b = (c+a) * (c-a).
>
> It is also clear that the exponents of the prime factorization of
> (b*b) must all be even.
>
> I am not sure how you conclude from this that ((c+a)/q) and ((c-a)/q)
> must be perfect squares? Can you express this step formally?

If we let p1, ..., pn be the prime factorization of b, then we obviously
have that b*b = p1^2 * ... * pn^2. Since b*b = (c+a) * (c-a), it
obviously stands (c+a) and (c-a) each get some subset of these prime
factors.

For each factor p_i^2, it stands to reason that there are three ways it
can end up in the product (c+a) * (c-a). It can be a factor of only
(c+a), a factor of only (c-a), or p_i could be a factor of each.

The GCD q will be made up only of the p_i^2 factors that were split
between the two quantities; if we divide q from both of the quantities,
we are therefore left with the product of numerous perfect squares,
which must itself be a perfect square.

Another way to think about it is to look at the exponents of prime
factors of b*b, c + a, and c - a. Since b*b's prime factorization must
have all even exponents, the corresponding prime must have either both
odd or both even exponents in c + a and c - a. If you divide those
quantities by their GCD, you will either be subtracting even exponents
by an even exponent (producing an even) or odd exponents by an odd
exponent (producing an even), leaving you with only even exponents.

--
Beware of bugs in the above code; I have only proved it correct, not
tried it. -- Donald E. Knuth

Date Subject Author
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/24/09 Andrew Tomazos
6/25/09 MeAmI.org
6/25/09 Jan Burse
6/26/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Joshua Cranmer
6/27/09 Andrew Tomazos
6/21/09 Marshall
6/21/09 Spiros Bousbouras
6/24/09 Tim Smith
6/21/09 Charlie-Boo
6/21/09 William Elliot
6/22/09 MeAmI.org
6/22/09 MeAmI.org
6/23/09 Slawomir
6/24/09 David Bernier
6/24/09 MeAmI.org
6/24/09 MeAmI.org
6/24/09 Andrew Tomazos
6/24/09 Andrew Tomazos
6/25/09 Slawomir