let z2, z1 be Element of ; :: thesis: ( z2 <> 0. F_Complex implies ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) ) )
assume A1: z2 <> 0. F_Complex ; :: thesis: ( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )
then A2: - z2 <> 0. F_Complex by VECTSP_1:86;
reconsider z1' = z1, z2' = z2 as Element of COMPLEX by Def1;
A3: - z1 = - z1' by Th4;
z1 / z2 = z1' / z2' by A1, Th8;
hence - (z1 / z2) = - (z1' / z2') by Th4
.= (- z1') / z2' by XCMPLX_1:188
.= (- z1) / z2 by A3, A1, Th8 ;
:: thesis: - (z1 / z2) = z1 / (- z2)
A4: - z2 = - z2' by Th4;
z1 / z2 = z1' / z2' by A1, Th8;
hence - (z1 / z2) = - (z1' / z2') by Th4
.= z1' / (- z2') by XCMPLX_1:189
.= z1 / (- z2) by A4, A2, Th8 ;
:: thesis: verum