We want to prove the square root of 2 is irrational.
By the definition of rational number, we will show that there are no numbers
N
and
M
such that
2 * M * M = N * N
and
gcd(M, N) = 1
.
We want to prove
not (
( M
N
: NzNat
)
(2 * M) * M = N * N
and
gcd(M , N) = 1
)
.
We take the following steps:
-
We assume
| |
(M
N
: NzNat
)
(2 * M) * M = N * N
and
gcd(M , N) = 1
,
|
and try to get contradiction.
-
By skolemization,
we can get
| |
(2 * n1) * n1 = n2 * n2
and
gcd(n1 , n2) = 1
|
from the following hypothesis
| |
(M
N
: NzNat
)
(2 * M) * M = N * N
and
gcd(M , N) = 1
.
|
-
Then we decompose the hypothesis
| |
(2 * n1) * n1 = n2 * n2
and
gcd(n1 , n2) = 1
.
|
into the following
2 hypothese:
-
| |
(2 * n1) * n1 = n2 * n2
.
|
-
-
We introduce the lemma
| |
(  M
N
: Nat
)
(2 * M) * M = N * N
implies
(K
: Nat
)
N = 2 * K.
|
Click here to see its proof.
-
By modus ponens ,
we get
| |
(K
: Nat
)
n2 = 2 * K
|
from
| |
( M
N
: Nat
)
(2 * M) * M = N * N
implies
(K
: Nat
)
N = 2 * K
|
and
| |
(2 * n1) * n1 = n2 * n2
.
|
-
By skolemization,
we can get
from the following hypothesis
| |
(K
: Nat
)
n2 = 2 * K
.
|
-
Then we apply equation
n2 = 2 * n3
to the hypothesis
| |
(2 * n1) * n1 = n2 * n2
,
|
and get
| |
(2 * n1) * n1 = ((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3))
,
|
-
We reverse the equation
(2 * n1) * n1 = ((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3))
,
and get
((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3)) = (2 * n1) * n1
,
-
We introduce the lemma
| |
( M
N
: Nat
)
2 * M = 2 * N
implies
M = N.
|
Click here to see its proof.
-
By modus ponens ,
we get
| |
(n3 * n3) + (n3 * n3) = n1 * n1
|
from
| |
( M
N
: Nat
)
2 * M = 2 * N
implies
M = N
|
and
| |
((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3)) = (2 * n1) * n1
.
|
-
By modus ponens ,
we get
| |
(K
: Nat
)
n1 = 2 * K
|
from
| |
( M
N
: Nat
)
(2 * M) * M = N * N
implies
(K
: Nat
)
N = 2 * K
|
and
| |
(n3 * n3) + (n3 * n3) = n1 * n1
.
|
-
By skolemization,
we can get
from the following hypothesis
| |
(K
: Nat
)
n1 = 2 * K
.
|
-
Then we apply equation
n2 = 2 * n3
to the hypothesis
and get
-
Then we apply equation
n1 = 2 * n4
to the hypothesis
and get
| |
gcd(n4 + n4 , n3 + n3) = 1
,
|
-
We introduce the lemma
| |
( M
N
: NzNat
)
gcd(M + M , N + N) > (s 0).
|
Click here to see its proof.
-
In the following hypothesis
| |
( M
N
: NzNat
)
gcd(M + M , N + N) > (s 0)
,
|
let
M
=
n4
and
N
=
n3
, we get
| |
gcd(n4 + n4 , n3 + n3) > (s 0)
,
|
-
Then we apply equation
gcd(n4 + n4 , n3 + n3) = 1
to the hypothesis
| |
gcd(n4 + n4 , n3 + n3) > (s 0)
,
|
and get
And thus the main goal is proved.
|
