let D be Nat; ( not D is square implies ex x, y being Nat st
( (x ^2) - (D * (y ^2)) = 1 & y <> 0 ) )
assume
not D is square
; ex x, y being Nat st
( (x ^2) - (D * (y ^2)) = 1 & y <> 0 )
then consider k, a, b, c, d being Integer such that
A1:
0 <> k
and
A2:
( (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) )
and
A3:
a,c are_congruent_mod k
and
A4:
b,d are_congruent_mod k
and
A5:
( |.a.| <> |.c.| or |.b.| <> |.d.| )
by Th13;
consider t being Integer such that
A6:
a - c = k * t
by A3, INT_1:def 5;
consider v being Integer such that
A7:
b - d = k * v
by A4, INT_1:def 5;
reconsider x = |.((1 + (c * t)) - ((D * d) * v)).|, y = |.((d * t) - (c * v)).| as Nat by TARSKI:1;
take
x
; ex y being Nat st
( (x ^2) - (D * (y ^2)) = 1 & y <> 0 )
take
y
; ( (x ^2) - (D * (y ^2)) = 1 & y <> 0 )
A8:
( a = c + (k * t) & b = d + (k * v) )
by A6, A7;
A9: (a * c) - ((D * b) * d) =
((c + (k * t)) * c) - ((D * (d + (k * v))) * d)
by A6, A7
.=
((c ^2) - (D * (d ^2))) + (k * ((c * t) - ((D * d) * v)))
.=
k * ((1 + (c * t)) - ((D * d) * v))
by A2
;
A10: (((a * c) - ((D * b) * d)) ^2) - (D * (((a * d) - (c * b)) ^2)) =
(((a * c) - ((D * b) * d)) ^2) - (D * ((((c + (k * t)) * d) - ((d + (k * v)) * c)) ^2))
by A6, A7
.=
((k * ((1 + (c * t)) - ((D * d) * v))) ^2) - (D * ((k * ((d * t) - (c * v))) ^2))
by A9
;
( x ^2 = ((1 + (c * t)) - ((D * d) * v)) ^2 & y ^2 = ((d * t) - (c * v)) ^2 )
by COMPLEX1:75;
hence A11: (x ^2) - (D * (y ^2)) =
(((((1 + (c * t)) - ((D * d) * v)) ^2) * (k ^2)) - ((D * (((d * t) - (c * v)) ^2)) * (k ^2))) / (k ^2)
by A1, XCMPLX_1:129
.=
(((a ^2) - (D * (b ^2))) * ((c ^2) - (D * (d ^2)))) / (k ^2)
by A10
.=
1
by A2, A1, XCMPLX_1:60
;
y <> 0
assume A12:
y = 0
; contradiction
A13: ((1 + (c * t)) - ((D * d) * v)) * c =
(c + ((c * t) * c)) - ((D * d) * (0 + (v * c)))
.=
(c + ((c * t) * c)) - ((D * d) * (((d * t) - (c * v)) + (v * c)))
by A12, ABSVALUE:2
.=
c + (((c ^2) - (D * (d ^2))) * t)
;
A14: ((1 + (c * t)) - ((D * d) * v)) * d =
((1 * d) + (c * ((t * d) - 0))) - (((D * d) * v) * d)
.=
((1 * d) + (c * ((t * d) - ((d * t) - (c * v))))) - (((D * d) * v) * d)
by A12, ABSVALUE:2
.=
d + (((c ^2) - (D * (d ^2))) * v)
;
A15:
x = 1
by A11, A12, SQUARE_1:18, SQUARE_1:22;