This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem creui

Description: The imaginary part of a complex number is unique. Proposition 10-1.3 of Gleason p. 130. (Contributed by NM, 9-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion creui 
|- ( A e. CC -> E! y e. RR E. x e. RR A = ( x + ( _i x. y ) ) )

Proof

Step Hyp Ref Expression
1 cnre 
 |-  ( A e. CC -> E. z e. RR E. w e. RR A = ( z + ( _i x. w ) ) )
2 simpr 
 |-  ( ( z e. RR /\ w e. RR ) -> w e. RR )
3 eqcom 
 |-  ( ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> ( x + ( _i x. y ) ) = ( z + ( _i x. w ) ) )
4 cru 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( z e. RR /\ w e. RR ) ) -> ( ( x + ( _i x. y ) ) = ( z + ( _i x. w ) ) <-> ( x = z /\ y = w ) ) )
5 4 ancoms 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ ( x e. RR /\ y e. RR ) ) -> ( ( x + ( _i x. y ) ) = ( z + ( _i x. w ) ) <-> ( x = z /\ y = w ) ) )
6 3 5 bitrid 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ ( x e. RR /\ y e. RR ) ) -> ( ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> ( x = z /\ y = w ) ) )
7 6 anass1rs 
 |-  ( ( ( ( z e. RR /\ w e. RR ) /\ y e. RR ) /\ x e. RR ) -> ( ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> ( x = z /\ y = w ) ) )
8 7 rexbidva 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ y e. RR ) -> ( E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> E. x e. RR ( x = z /\ y = w ) ) )
9 biidd 
 |-  ( x = z -> ( y = w <-> y = w ) )
10 9 ceqsrexv 
 |-  ( z e. RR -> ( E. x e. RR ( x = z /\ y = w ) <-> y = w ) )
11 10 ad2antrr 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ y e. RR ) -> ( E. x e. RR ( x = z /\ y = w ) <-> y = w ) )
12 8 11 bitrd 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ y e. RR ) -> ( E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> y = w ) )
13 12 ralrimiva 
 |-  ( ( z e. RR /\ w e. RR ) -> A. y e. RR ( E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> y = w ) )
14 reu6i 
 |-  ( ( w e. RR /\ A. y e. RR ( E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> y = w ) ) -> E! y e. RR E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) )
15 2 13 14 syl2anc 
 |-  ( ( z e. RR /\ w e. RR ) -> E! y e. RR E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) )
16 eqeq1 
 |-  ( A = ( z + ( _i x. w ) ) -> ( A = ( x + ( _i x. y ) ) <-> ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) ) )
17 16 rexbidv 
 |-  ( A = ( z + ( _i x. w ) ) -> ( E. x e. RR A = ( x + ( _i x. y ) ) <-> E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) ) )
18 17 reubidv 
 |-  ( A = ( z + ( _i x. w ) ) -> ( E! y e. RR E. x e. RR A = ( x + ( _i x. y ) ) <-> E! y e. RR E. x e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) ) )
19 15 18 syl5ibrcom 
 |-  ( ( z e. RR /\ w e. RR ) -> ( A = ( z + ( _i x. w ) ) -> E! y e. RR E. x e. RR A = ( x + ( _i x. y ) ) ) )
20 19 rexlimivv 
 |-  ( E. z e. RR E. w e. RR A = ( z + ( _i x. w ) ) -> E! y e. RR E. x e. RR A = ( x + ( _i x. y ) ) )
21 1 20 syl 
 |-  ( A e. CC -> E! y e. RR E. x e. RR A = ( x + ( _i x. y ) ) )