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