let x, y be Real; :: thesis: for z being Complex

for v being Element of (REAL-NS 2) st z = x + (y * <i>) & v = <*x,y*> holds

|.z.| = ||.v.||

let z be Complex; :: thesis: for v being Element of (REAL-NS 2) st z = x + (y * <i>) & v = <*x,y*> holds

|.z.| = ||.v.||

let v be Element of (REAL-NS 2); :: thesis: ( z = x + (y * <i>) & v = <*x,y*> implies |.z.| = ||.v.|| )

assume that

A1: z = x + (y * <i>) and

A2: v = <*x,y*> ; :: thesis: |.z.| = ||.v.||

A3: Im z = y by A1, COMPLEX1:12;

( x in REAL & y in REAL ) by XREAL_0:def 1;

then reconsider xx = <*x,y*> as Element of REAL 2 by FINSEQ_2:101;

A4: ( |.xx.| = ||.v.|| & Re z = x ) by A1, A2, COMPLEX1:12, REAL_NS1:1;

reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22;

xx1 `2 = y by FINSEQ_1:44;

then A5: (sqr xx) . 2 = y ^2 by VALUED_1:11;

xx1 `1 = x by FINSEQ_1:44;

then ( len (sqr xx) = 2 & (sqr xx) . 1 = x ^2 ) by CARD_1:def 7, VALUED_1:11;

then sqr xx = <*(x ^2),(y ^2)*> by A5, FINSEQ_1:44;

hence |.z.| = ||.v.|| by A4, A3, RVSUM_1:77; :: thesis: verum

for v being Element of (REAL-NS 2) st z = x + (y * <i>) & v = <*x,y*> holds

|.z.| = ||.v.||

let z be Complex; :: thesis: for v being Element of (REAL-NS 2) st z = x + (y * <i>) & v = <*x,y*> holds

|.z.| = ||.v.||

let v be Element of (REAL-NS 2); :: thesis: ( z = x + (y * <i>) & v = <*x,y*> implies |.z.| = ||.v.|| )

assume that

A1: z = x + (y * <i>) and

A2: v = <*x,y*> ; :: thesis: |.z.| = ||.v.||

A3: Im z = y by A1, COMPLEX1:12;

( x in REAL & y in REAL ) by XREAL_0:def 1;

then reconsider xx = <*x,y*> as Element of REAL 2 by FINSEQ_2:101;

A4: ( |.xx.| = ||.v.|| & Re z = x ) by A1, A2, COMPLEX1:12, REAL_NS1:1;

reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22;

xx1 `2 = y by FINSEQ_1:44;

then A5: (sqr xx) . 2 = y ^2 by VALUED_1:11;

xx1 `1 = x by FINSEQ_1:44;

then ( len (sqr xx) = 2 & (sqr xx) . 1 = x ^2 ) by CARD_1:def 7, VALUED_1:11;

then sqr xx = <*(x ^2),(y ^2)*> by A5, FINSEQ_1:44;

hence |.z.| = ||.v.|| by A4, A3, RVSUM_1:77; :: thesis: verum