let D be Nat; :: thesis: ( not D is square implies ex x, y being Nat st
( (x ^2) - (D * (y ^2)) = 1 & y <> 0 ) )
assume not D is square ; :: thesis: 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 ; :: thesis: ex y being Nat st
( (x ^2) - (D * (y ^2)) = 1 & y <> 0 )
take y ; :: thesis: ( (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 ;
:: thesis: y <> 0
assume A12: y = 0 ; :: thesis: 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;

per cases ( (1 + (c * t)) - ((D * d) * v) = 1 or - ((1 + (c * t)) - ((D * d) * v)) = 1 ) by A15, ABSVALUE:def 1;

suppose (1 + (c * t)) - ((D * d) * v) = 1 ; :: thesis: contradiction

hence contradiction by A5, A2, A8, A13, A14; :: thesis: verum

end;

suppose - ((1 + (c * t)) - ((D * d) * v)) = 1 ; :: thesis: contradiction

then ( (- 1) * c = c + (((c ^2) - (D * (d ^2))) * t) & (- 1) * d = d + (((c ^2) - (D * (d ^2))) * v) ) by A13, A14;
then ( - c = c + (((c ^2) - (D * (d ^2))) * t) & - d = d + (((c ^2) - (D * (d ^2))) * v) ) ;
hence contradiction by A5, A2, Lm2, A8; :: thesis: verum

end;

end;