let z, a2, a1, a0, x, a3, q, r, p be complex number ; :: thesis: ( z = x - (a3 / 4) & p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 implies ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r) = 0 ) )
assume A1: z = x - (a3 / 4) ; :: thesis: ( not p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 or not q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 or not r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 or ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r) = 0 ) )
assume A2: ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 ) ; :: thesis: ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r) = 0 )
A3: 4 * z = (4 * x) - a3 by A1;
A4: (4 * x) |^ 4 = (4 |^ 4) * (x |^ 4) by NEWTON:12
.= (((4 * 4) * 4) * 4) * (x |^ 4) by Th3
.= 256 * (x |^ 4) ;
A5: (4 * x) |^ 3 = (4 |^ 3) * (x |^ 3) by NEWTON:12
.= ((4 * 4) * 4) * (x |^ 3) by Th2
.= 64 * (x |^ 3) ;
A6: (4 * x) |^ 2 = (4 |^ 2) * (x |^ 2) by NEWTON:12
.= (4 * 4) * (x |^ 2) by Th1
.= 16 * (x |^ 2) ;
A7: 256 * (z |^ 4) = (((4 * 4) * 4) * 4) * (z |^ 4)
.= (4 |^ 4) * (z |^ 4) by Th3
.= ((4 * x) - a3) |^ 4 by A3, NEWTON:12
.= ((((256 * (x |^ 4)) - ((4 * (64 * (x |^ 3))) * a3)) + ((6 * (16 * (x |^ 2))) * (a3 |^ 2))) - ((4 * (a3 |^ 3)) * (4 * x))) + (a3 |^ 4) by A5, A6, A4, Th7
.= ((((256 * (x |^ 4)) - ((256 * (x |^ 3)) * a3)) + ((96 * (x |^ 2)) * (a3 |^ 2))) - ((16 * (a3 |^ 3)) * x)) + (a3 |^ 4) ;
A8: (4 * a3) * (64 * (z |^ 3)) = (4 * a3) * (((4 * 4) * 4) * (z |^ 3))
.= (4 * a3) * ((4 |^ 3) * (z |^ 3)) by Th2
.= (4 * a3) * (((4 * x) - a3) |^ 3) by A3, NEWTON:12
.= (4 * a3) * ((((64 * (x |^ 3)) - ((3 * (16 * (x |^ 2))) * a3)) + ((3 * (a3 |^ 2)) * (4 * x))) - (a3 |^ 3)) by A5, A6, Th6
.= ((((256 * a3) * (x |^ 3)) - ((192 * (a3 * a3)) * (x |^ 2))) + ((48 * ((a3 |^ 2) * a3)) * x)) - (4 * ((a3 |^ 3) * a3))
.= ((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * ((a3 |^ 2) * a3)) * x)) - (4 * ((a3 |^ 3) * a3)) by Th1
.= ((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ (2 + 1))) * x)) - (4 * ((a3 |^ 3) * a3)) by NEWTON:11
.= ((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ 3)) * x)) - (4 * (a3 |^ (3 + 1))) by NEWTON:11
.= ((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ 3)) * x)) - (4 * (a3 |^ 4)) ;
A9: 16 * (z |^ 2) = (4 * 4) * (z |^ 2)
.= (4 |^ 2) * (z |^ 2) by Th1
.= (4 * z) |^ 2 by NEWTON:12
.= (((4 * x) |^ 2) - ((2 * (4 * x)) * a3)) + (a3 |^ 2) by A3, Th5
.= (((4 * x) * (4 * x)) - ((2 * (4 * x)) * a3)) + (a3 |^ 2) by Th1
.= ((16 * (x * x)) - ((8 * x) * a3)) + (a3 |^ 2)
.= ((16 * (x |^ 2)) - ((8 * x) * a3)) + (a3 |^ 2) by Th1 ;
256 * (((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0) = ((((256 * (z |^ 4)) + ((4 * a3) * (64 * (z |^ 3)))) + ((16 * a2) * (16 * (z |^ 2)))) + ((64 * a1) * (4 * z))) + (256 * a0)
.= ((((((((256 * (x |^ 4)) - ((256 * (x |^ 3)) * a3)) + ((96 * (x |^ 2)) * (a3 |^ 2))) - ((16 * (a3 |^ 3)) * x)) + (a3 |^ 4)) + (((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ 3)) * x)) - (4 * (a3 |^ 4)))) + ((16 * a2) * (((16 * (x |^ 2)) - ((8 * x) * a3)) + (a3 |^ 2)))) + ((64 * a1) * ((4 * x) - a3))) + (256 * a0) by A1, A9, A8, A7
.= 256 * ((((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r)) by A2 ;
hence ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r) = 0 ) ; :: thesis: verum