thus ( z <> 0 implies ex z9 being Complex st z * z9 = 1 ) :: thesis: ( not z <> 0 implies ex b₁ being Complex 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 by Def2;
assume A15: z <> 0 ; :: thesis: ex z9 being Complex st z * z9 = 1
take z9 ; :: thesis: z * z9 = 1
A16: opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))) = opp (* (y,(opp (* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:15
.= opp (opp (* (y,(* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:15
.= * ((* (y,y)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:13 ;
A17: * (x,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((* (x,x)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:13;

A18: now :: thesis: not + ((* (x,x)),(* (y,y))) = 0

assume + ((* (x,x)),(* (y,y))) = 0 ; :: thesis: contradiction
then ( x = 0 & y = 0 ) by ARYTM_0:17;
hence contradiction by A1, A15, ARYTM_0:def 5; :: thesis: verum

end;

* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((opp y),(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) by ARYTM_0:13
.= opp (* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))) by ARYTM_0:15 ;
then + ((* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))),(* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))))) = 0 by ARYTM_0:def 3;
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 5
.= * ((+ ((* (x,x)),(* (y,y)))),(inv (+ ((* (x,x)),(* (y,y)))))) by A16, A17, ARYTM_0:14
.= 1 by A18, ARYTM_0:def 4 ;
hence z * z9 = 1 by A1, Def4; :: thesis: verum

end;

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