MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  replim Unicode version

Theorem replim 11442
Description: Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
Assertion
Ref Expression
replim  |-  ( A  e.  CC  ->  A  =  ( ( Re
`  A )  +  ( _i  x.  (
Im `  A )
) ) )

Proof of Theorem replim
StepHypRef Expression
1 ax-cnre 8687 . 2  |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
2 crre 11440 . . . . . 6  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( Re `  (
x  +  ( _i  x.  y ) ) )  =  x )
3 crim 11441 . . . . . . 7  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( Im `  (
x  +  ( _i  x.  y ) ) )  =  y )
43oveq2d 5723 . . . . . 6  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( _i  x.  (
Im `  ( x  +  ( _i  x.  y ) ) ) )  =  ( _i  x.  y ) )
52, 4oveq12d 5725 . . . . 5  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( Re `  ( x  +  (
_i  x.  y )
) )  +  ( _i  x.  ( Im
`  ( x  +  ( _i  x.  y
) ) ) ) )  =  ( x  +  ( _i  x.  y ) ) )
65eqcomd 2258 . . . 4  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  +  ( _i  x.  y ) )  =  ( ( Re `  ( x  +  ( _i  x.  y ) ) )  +  ( _i  x.  ( Im `  ( x  +  ( _i  x.  y ) ) ) ) ) )
7 id 21 . . . . 5  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  A  =  ( x  +  ( _i  x.  y
) ) )
8 fveq2 5374 . . . . . 6  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
Re `  A )  =  ( Re `  ( x  +  (
_i  x.  y )
) ) )
9 fveq2 5374 . . . . . . 7  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
Im `  A )  =  ( Im `  ( x  +  (
_i  x.  y )
) ) )
109oveq2d 5723 . . . . . 6  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
_i  x.  ( Im `  A ) )  =  ( _i  x.  (
Im `  ( x  +  ( _i  x.  y ) ) ) ) )
118, 10oveq12d 5725 . . . . 5  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
( Re `  A
)  +  ( _i  x.  ( Im `  A ) ) )  =  ( ( Re
`  ( x  +  ( _i  x.  y
) ) )  +  ( _i  x.  (
Im `  ( x  +  ( _i  x.  y ) ) ) ) ) )
127, 11eqeq12d 2267 . . . 4  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  ( A  =  ( (
Re `  A )  +  ( _i  x.  ( Im `  A ) ) )  <->  ( x  +  ( _i  x.  y ) )  =  ( ( Re `  ( x  +  (
_i  x.  y )
) )  +  ( _i  x.  ( Im
`  ( x  +  ( _i  x.  y
) ) ) ) ) ) )
136, 12syl5ibrcom 215 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( A  =  ( x  +  ( _i  x.  y ) )  ->  A  =  ( ( Re `  A
)  +  ( _i  x.  ( Im `  A ) ) ) ) )
1413rexlimivv 2632 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) )  ->  A  =  ( ( Re
`  A )  +  ( _i  x.  (
Im `  A )
) ) )
151, 14syl 17 1  |-  ( A  e.  CC  ->  A  =  ( ( Re
`  A )  +  ( _i  x.  (
Im `  A )
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621   E.wrex 2508   ` cfv 4589  (class class class)co 5707   CCcc 8612   RRcr 8613   _ici 8616    + caddc 8617    x. cmul 8619   Recre 11423   Imcim 11424
This theorem is referenced by:  remim  11443  reim0b  11445  rereb  11446  mulre  11447  cjreb  11449  reneg  11451  readd  11452  remullem  11454  imneg  11459  imadd  11460  cjcj  11466  imval2  11477  cnrecnv  11491  replimi  11496  replimd  11523  recan  11659  efeul  12278  absef  12313  absefib  12314  efieq1re  12315  cnsubrg  16226  itgconst  18967  tanregt0  19691  tanarg  19754
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4035  ax-nul 4043  ax-pow 4079  ax-pr 4105  ax-un 4400  ax-resscn 8671  ax-1cn 8672  ax-icn 8673  ax-addcl 8674  ax-addrcl 8675  ax-mulcl 8676  ax-mulrcl 8677  ax-mulcom 8678  ax-addass 8679  ax-mulass 8680  ax-distr 8681  ax-i2m1 8682  ax-1ne0 8683  ax-1rid 8684  ax-rnegex 8685  ax-rrecex 8686  ax-cnre 8687  ax-pre-lttri 8688  ax-pre-lttrn 8689  ax-pre-ltadd 8690  ax-pre-mulgt0 8691
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-nel 2415  df-ral 2511  df-rex 2512  df-reu 2513  df-rab 2514  df-v 2727  df-sbc 2920  df-csb 3007  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-pw 3529  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-mpt 3973  df-id 4199  df-po 4204  df-so 4205  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fun 4599  df-fn 4600  df-f 4601  df-f1 4602  df-fo 4603  df-f1o 4604  df-fv 4605  df-ov 5710  df-oprab 5711  df-mpt2 5712  df-iota 6140  df-riota 6187  df-er 6543  df-en 6747  df-dom 6748  df-sdom 6749  df-pnf 8746  df-mnf 8747  df-xr 8748  df-ltxr 8749  df-le 8750  df-sub 8911  df-neg 8912  df-div 9280  df-2 9652  df-cj 11425  df-re 11426  df-im 11427
  Copyright terms: Public domain W3C validator