Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


Math Forum » Discussions » sci.math.* » sci.math

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   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
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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
Read Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/26/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Joshua Cranmer
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Marshall
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Spiros Bousbouras
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Tim Smith
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Charlie-Boo
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
William Elliot
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/23/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
David Bernier
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.