Metamath Proof Explorer

Theorem creur

Description: The real 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 creur 
|- ( A e. CC -> E! x e. RR E. y 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 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 ) ) )
3 2 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 ) ) )
4 eqcom 
 |-  ( ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> ( x + ( _i x. y ) ) = ( z + ( _i x. w ) ) )
5 ancom 
 |-  ( ( y = w /\ x = z ) <-> ( x = z /\ y = w ) )
6 3 4 5 3bitr4g 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ ( x e. RR /\ y e. RR ) ) -> ( ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> ( y = w /\ x = z ) ) )
7 6 anassrs 
 |-  ( ( ( ( z e. RR /\ w e. RR ) /\ x e. RR ) /\ y e. RR ) -> ( ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> ( y = w /\ x = z ) ) )
8 7 rexbidva 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ x e. RR ) -> ( E. y e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> E. y e. RR ( y = w /\ x = z ) ) )
9 biidd 
 |-  ( y = w -> ( x = z <-> x = z ) )
10 9 ceqsrexv 
 |-  ( w e. RR -> ( E. y e. RR ( y = w /\ x = z ) <-> x = z ) )
11 10 ad2antlr 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ x e. RR ) -> ( E. y e. RR ( y = w /\ x = z ) <-> x = z ) )
12 8 11 bitrd 
 |-  ( ( ( z e. RR /\ w e. RR ) /\ x e. RR ) -> ( E. y e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> x = z ) )
13 12 ralrimiva 
 |-  ( ( z e. RR /\ w e. RR ) -> A. x e. RR ( E. y e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> x = z ) )
14 reu6i 
 |-  ( ( z e. RR /\ A. x e. RR ( E. y e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) <-> x = z ) ) -> E! x e. RR E. y e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) )
15 13 14 syldan 
 |-  ( ( z e. RR /\ w e. RR ) -> E! x e. RR E. y 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. y e. RR A = ( x + ( _i x. y ) ) <-> E. y e. RR ( z + ( _i x. w ) ) = ( x + ( _i x. y ) ) ) )
18 17 reubidv 
 |-  ( A = ( z + ( _i x. w ) ) -> ( E! x e. RR E. y e. RR A = ( x + ( _i x. y ) ) <-> E! x e. RR E. y 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! x e. RR E. y e. RR A = ( x + ( _i x. y ) ) ) )
20 19 rexlimivv 
 |-  ( E. z e. RR E. w e. RR A = ( z + ( _i x. w ) ) -> E! x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
21 1 20 syl 
 |-  ( A e. CC -> E! x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )