thus ( z <> 0 implies ex z9 being complex number st z * z9 = 1 ) :: thesis: ( not z <> 0 implies ex b₁ being complex number st b₁ = 0 )

proof

set y1 = * (x,(inv (+ ((* (x,x)),(* (y,y))))));
set y2 = * ((opp y),(inv (+ ((* (x,x)),(* (y,y))))));
set z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*];
reconsider z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] as complex number by Def2;
assume A19: z <> 0 ; :: thesis: ex z9 being complex number st z * z9 = 1
take z9 ; :: thesis: z * z9 = 1
A20: opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))) = opp (* (y,(opp (* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:17
.= opp (opp (* (y,(* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:17
.= * ((* (y,y)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:15 ;
A21: * (x,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((* (x,x)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:15;

A22: now

assume + ((* (x,x)),(* (y,y))) = 0 ; :: thesis: contradiction
then ( x = 0 & y = 0 ) by ARYTM_0:19;
hence contradiction by A2, A19, ARYTM_0:def 7; :: thesis: verum

end;

* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((opp y),(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) by ARYTM_0:15
.= opp (* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))) by ARYTM_0:17 ;
then + ((* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))),(* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))))) = 0 by ARYTM_0:def 4;
then [*(+ ((* (x,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))),(opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))))))),(+ ((* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))),(* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))))))*] = + ((* (x,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))),(opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))))) by ARYTM_0:def 7
.= * ((+ ((* (x,x)),(* (y,y)))),(inv (+ ((* (x,x)),(* (y,y)))))) by A20, A21, ARYTM_0:16
.= 1 by A22, ARYTM_0:def 5 ;
hence z * z9 = 1 by A2, Def5; :: thesis: verum

end;

assume z = 0 ; :: thesis: ex b₁ being complex number st b₁ = 0
hence ex b₁ being complex number st b₁ = 0 ; :: thesis: verum