> I imagine that one could also prove that √−1 is not rational
I feel like this was a marvellous joke but I can’t prove it.
I feel like this was a marvellous joke but I can’t prove it.
* sqrt(-1) = a/b
* a^2 = -1 * b^2
Then either a^2 or b^2 are negative but a square can't be negative, so contradiction and sqrt(-1) is not rational.
The main "problem" with this proof (and the original with sqrt(2)) is "how to prove that a^2 >= 0" (or that "if a^2 is even, then a is even")
The first one is easy to prove:
* a^2 = sign(a)^2 * abs(a)^2
* abs(a) >= 0 for any a
* sign(a) = 1 or -1 for any a so sign(a)^2 = 1 (either 1*1 or -1*-1)
* so a^2 >= 0
The second one may be proved:
* Assume a is even, then a=2n, then a^2=4n^2=2*(2n^2) so a is even => a^2 is even
* Assume a is odd, then a=2n+1, then a^2=4n^2+4n+1=2*(2n^2+2n)+1, then a^2 is odd
* a is either even or odd
* So the only possibility for a^2 to be even is for a to be even
And both sign and abs are not defined. So you say abs(a) >= 0 and sign(a) \in {-1, 1}. Why? For instance, what is sign(0)?
Are you assuming a construction of integers from the natural numbers such that for any n < 0, there is an integer abs(n) and n = -1 * abs(n)? If so, don't you need to include that (or at least reference it)?
Later you assume that all integers are even or odd. Why?
These are niggling details that don't matter when you have chalk in hand, but do matter when speaking to a system like lean4.
* abs(x) is usually defined as "x if x >=0 and -x if x < 0"
* sign(x) is usually defined as "1 if x >=0 and -1 if x < 0"
* with these definitions, it follows that for any x, x = sign(x) * abs(x) (by definition applied for each cases >=0 and <0, assuming that all integer are either >=0 or <0)
Showing that any integer is either even or odd seem less obvious
https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur...
btw, that book is a lot of fun to work through.
i tends to pop out as a construction so I suspect you can probably prove it is both rational and irrational or neither, depending on the fine print.
Here's a discussion: https://math.stackexchange.com/questions/823970/is-i-irratio...