let z be Element of Gauss_INT_Ring; :: thesis: for zz being G_INTEG st zz = z holds
( z is unital iff zz is g_int_unit )
let zz be G_INTEG; :: thesis: ( zz = z implies ( z is unital iff zz is g_int_unit ) )
assume A1: zz = z ; :: thesis: ( z is unital iff zz is g_int_unit )
hereby :: thesis: ( zz is g_int_unit implies z is unital )
assume A2: z is unital ; :: thesis: zz is g_int_unit
consider x being Element of Gauss_INT_Ring such that
A3: 1. Gauss_INT_Ring = z * x by A2, GCD_1:def 1, GCD_1:def 20;
reconsider xx = x as G_INTEG by Th2;
A4: z * x = zz * xx by A1, Th6;
reconsider gintone = In (1,G_INT_SET) as G_INTEG ;
(Norm zz) * (Norm xx) = Norm gintone by A3, A4, Th34
.= 1 by COMPLEX1:30 ;
hence zz is g_int_unit by NAT_1:15; :: thesis: verum
end;
assume A5: zz is g_int_unit ; :: thesis: z is unital
ex w being Element of Gauss_INT_Ring st 1. Gauss_INT_Ring = z * w
proof
per cases ( z = 1 or z = - 1 or z = <i> or z = - <i> ) by A5, A1, Th35;
suppose A6: z = 1 ; :: thesis: ex w being Element of Gauss_INT_Ring st 1. Gauss_INT_Ring = z * w
take w = z; :: thesis: 1. Gauss_INT_Ring = z * w
thus 1. Gauss_INT_Ring = 1 * 1
.= z * w by A6, Th6 ; :: thesis: verum
end;
suppose A7: z = - 1 ; :: thesis: ex w being Element of Gauss_INT_Ring st 1. Gauss_INT_Ring = z * w
take w = z; :: thesis: 1. Gauss_INT_Ring = z * w
thus 1. Gauss_INT_Ring = (- 1) * (- 1)
.= z * w by A7, Th6 ; :: thesis: verum
end;
suppose A8: z = <i> ; :: thesis: ex w being Element of Gauss_INT_Ring st 1. Gauss_INT_Ring = z * w
reconsider w = - <i> as Element of Gauss_INT_Ring by Th3;
take w ; :: thesis: 1. Gauss_INT_Ring = z * w
thus 1. Gauss_INT_Ring = <i> * (- <i>)
.= z * w by A8, Th6 ; :: thesis: verum
end;
suppose A9: z = - <i> ; :: thesis: ex w being Element of Gauss_INT_Ring st 1. Gauss_INT_Ring = z * w
reconsider w = <i> as Element of Gauss_INT_Ring by Lm2;
take w ; :: thesis: 1. Gauss_INT_Ring = z * w
thus 1. Gauss_INT_Ring = (- <i>) * <i>
.= z * w by A9, Th6 ; :: thesis: verum
end;
end;
end;
hence z is unital by GCD_1:def 2; :: thesis: verum