let x, y, p, q be Real; :: thesis: for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2 ) - (4 * q) >= 0 & p > 0 & q > 0 & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) & not ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) & not ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) & not ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) holds
( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) )
let n be Element of NAT ; :: thesis: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2 ) - (4 * q) >= 0 & p > 0 & q > 0 & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) & not ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) & not ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) & not ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) & not ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) implies ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) )
assume A1:
( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q )
; :: thesis: ( not (p ^2 ) - (4 * q) >= 0 or not p > 0 or not q > 0 or for m being Element of NAT holds
( not n = 2 * m or not m >= 1 ) or ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) )
assume A2:
( (p ^2 ) - (4 * q) >= 0 & p > 0 & q > 0 & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) )
; :: thesis: ( ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) )
A3: delta 1,(- p),q =
((- p) ^2 ) - ((4 * 1) * q)
by QUIN_1:def 1
.=
(p ^2 ) - (4 * q)
;
then
0 <= sqrt (delta 1,(- p),q)
by A2, SQUARE_1:82, SQUARE_1:94;
then A4:
(- (- p)) + (sqrt (delta 1,(- p),q)) > 0 + 0
by A2, XREAL_1:10;
- (- (4 * q)) > 0
by A2, XREAL_1:131;
then
- (4 * q) < 0
;
then
(p ^2 ) + (- (4 * q)) < (p ^2 ) + 0
by XREAL_1:10;
then
sqrt ((p ^2 ) - (4 * q)) < sqrt (p ^2 )
by A2, SQUARE_1:95;
then
sqrt ((p ^2 ) - (4 * q)) < p
by A2, SQUARE_1:89;
then
- (sqrt ((p ^2 ) - (4 * q))) > - p
by XREAL_1:26;
then
(- (sqrt ((p ^2 ) - (4 * q)))) + p > ((- p) + 0 ) + p
by XREAL_1:10;
then A5:
( ((0 + p) + (sqrt ((p ^2 ) - (4 * q)))) / 2 > 0 & ((0 + p) - (sqrt ((p ^2 ) - (4 * q)))) / 2 > 0 )
by A3, A4, XREAL_1:141;
hence
( ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2 ) - (4 * q)))) / 2)) ) )
; :: thesis: verum