let r be real number ; :: thesis: for b₁ being complex number st r = sqrt (((Re b₁) ^2) + ((Im b₁) ^2)) holds
r = sqrt (((Re r) ^2) + ((Im r) ^2))
let z be complex number ; :: thesis: ( r = sqrt (((Re z) ^2) + ((Im z) ^2)) implies r = sqrt (((Re r) ^2) + ((Im r) ^2)) )
assume A1: r = sqrt (((Re z) ^2) + ((Im z) ^2)) ; :: thesis: r = sqrt (((Re r) ^2) + ((Im r) ^2))
then A2: Im r = 0 by Def2;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63;
then r >= 0 by A1, SQUARE_1:def 2;
then A3: Re r >= 0 by A1, Def1;
thus r = Re r by A1, Def1
.= sqrt (((Re r) ^2) + ((Im r) ^2)) by A3, A2, SQUARE_1:22 ; :: thesis: verum