let a be non zero square Nat; :: thesis: for p being prime Nat st a + p is square holds
p = (2 * (sqrt a)) + 1
let p be prime Nat; :: thesis: ( a + p is square implies p = (2 * (sqrt a)) + 1 )
assume a + p is square ; :: thesis: p = (2 * (sqrt a)) + 1
then consider m being Nat such that
B2: a + p = m ^2 by PYTHTRIP:def 3;
consider n being Nat such that
B3: a = n ^2 by PYTHTRIP:def 3;
B4: p = (m ^2) - (n ^2) by B2, B3
.= (m - n) * (m + n) by NEWTON01:1 ;
m - n > 0 by B4;
then reconsider l = m - n as Element of NAT by INT_1:3;
( m - n divides p & m + n divides p ) by B4;
then B5: ( ( m + n = p or m + n = 1 ) & ( l = p or l = 1 ) ) by INT_2:def 4;
( n >= - n & not p is trivial ) ;
then ( n + m >= (- n) + m & p > 1 ) by XREAL_1:6;
then p = (2 * n) + 1 by B4, B5;
hence p = (2 * (sqrt a)) + 1 by B3, SQUARE_1:def 2; :: thesis: verum