let a be non zero Real; :: thesis: for b, c, d being Real st (a ^2) + (c ^2) = b ^2 & 1 < b ^2 holds
not (((((b ^2) ^2) / (a ^2)) - ((2 * (((b ^2) * c) / (a * a))) * d)) + (((c ^2) / (a ^2)) * (d ^2))) + (d ^2) = 1
let b, c, d be Real; :: thesis: ( (a ^2) + (c ^2) = b ^2 & 1 < b ^2 implies not (((((b ^2) ^2) / (a ^2)) - ((2 * (((b ^2) * c) / (a * a))) * d)) + (((c ^2) / (a ^2)) * (d ^2))) + (d ^2) = 1 )
assume that
A1: (a ^2) + (c ^2) = b ^2 and
A2: 1 < b ^2 ; :: thesis: not (((((b ^2) ^2) / (a ^2)) - ((2 * (((b ^2) * c) / (a * a))) * d)) + (((c ^2) / (a ^2)) * (d ^2))) + (d ^2) = 1
assume A5: (((((b ^2) ^2) / (a ^2)) - ((2 * (((b ^2) * c) / (a * a))) * d)) + (((c ^2) / (a ^2)) * (d ^2))) + (d ^2) = 1 ; :: thesis: contradiction
((c ^2) / (a ^2)) + 1 = ((c ^2) / (a ^2)) + ((a ^2) / (a ^2)) by XCMPLX_1:60
.= (b ^2) / (a ^2) by A1 ;
then A6: (a ^2) * (((c ^2) / (a ^2)) + 1) = ((a ^2) * (b ^2)) / (a ^2) by XCMPLX_1:74
.= b ^2 by XCMPLX_1:89 ;
A7: (a ^2) * (2 * (((b ^2) * c) / (a * a))) = 2 * (((a ^2) * ((b ^2) * c)) / (a * a))
.= 2 * ((b ^2) * c) by XCMPLX_1:89 ;
A8: ((a ^2) * (((b ^2) ^2) / (a ^2))) - ((a ^2) * 1) = (((a ^2) * ((b ^2) ^2)) / (a ^2)) - ((a ^2) * 1)
.= ((b ^2) ^2) - (a ^2) by XCMPLX_1:89 ;
(a ^2) * 0 = (a ^2) * (((((((c ^2) / (a ^2)) + 1) * (d ^2)) - ((2 * (((b ^2) * c) / (a * a))) * d)) + (((b ^2) ^2) / (a ^2))) - 1) by A5;
then A9: 0 = (((((a ^2) * (((c ^2) / (a ^2)) + 1)) * (d ^2)) - ((((a ^2) * 2) * (((b ^2) * c) / (a * a))) * d)) + ((a ^2) * (((b ^2) ^2) / (a ^2)))) - ((a ^2) * 1) ;
A11: b <> 0 by A6;
A12: 0 = (((((b ^2) * (d ^2)) - ((2 * ((b ^2) * c)) * d)) + ((b ^2) ^2)) - (a ^2)) / (b ^2) by A9, A6, A7, A8
.= (((((d ^2) * (b ^2)) / (b ^2)) - (((2 * ((b ^2) * c)) * d) / (b ^2))) + (((b ^2) ^2) / (b ^2))) - ((a ^2) / (b ^2))
.= (((d ^2) - (((2 * ((b ^2) * c)) * d) / (b ^2))) + (((b ^2) ^2) / (b ^2))) - ((a ^2) / (b ^2)) by A6, XCMPLX_1:89
.= (((d ^2) - ((2 * c) * d)) + (((b ^2) ^2) / (b ^2))) - ((a ^2) / (b ^2)) by A11, Th05
.= (((d ^2) + ((- (2 * c)) * d)) + (b ^2)) - ((a ^2) / (b ^2)) by A6, XCMPLX_1:89
.= ((1 * (d ^2)) + ((- (2 * c)) * d)) + ((b ^2) - ((a ^2) / (b ^2))) ;
reconsider c1 = 1, c2 = - (2 * c), c3 = (b ^2) - ((a ^2) / (b ^2)) as Real ;
A13: ((a ^2) / (b ^2)) - (a ^2) < 0 by A2, Th08;
delta (c1,c2,c3) < 0 hence contradiction by A12, QUIN_1:3; :: thesis: verum