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 A23: + (* x,x),(* y,y) = 0 ; :: thesis: contradiction
A24: ( x = 0 & y = 0 ) by A23, ARYTM_0:19;
thus contradiction by A2, A19, A24, ARYTM_0:def 7; :: thesis: verum

end;

A25: * 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 ;
A26: + (* x,(* (opp y),(inv (+ (* x,x),(* y,y))))),(* y,(* x,(inv (+ (* x,x),(* y,y))))) = 0 by A25, ARYTM_0:def 4;
A27: [*(+ (* 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 A26, 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 ;
thus z * z9 = 1 by A2, A27, Def5; :: thesis: verum

end;

assume A28: z = 0 ; :: thesis: ex b₁ being complex number st b₁ = 0
thus ex b₁ being complex number st b₁ = 0 by A28; :: thesis: verum