Metamath Proof Explorer

Theorem axcnre

Description: A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of Gleason p. 130. Axiom 17 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre . (Contributed by NM, 13-May-1996) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-c 
 |-  CC = ( R. X. R. )
2 eqeq1 
 |-  ( <. z , w >. = A -> ( <. z , w >. = ( x + ( _i x. y ) ) <-> A = ( x + ( _i x. y ) ) ) )
3 2 2rexbidv 
 |-  ( <. z , w >. = A -> ( E. x e. RR E. y e. RR <. z , w >. = ( x + ( _i x. y ) ) <-> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) ) )
4 opelreal 
 |-  ( <. z , 0R >. e. RR <-> z e. R. )
5 opelreal 
 |-  ( <. w , 0R >. e. RR <-> w e. R. )
6 4 5 anbi12i 
 |-  ( ( <. z , 0R >. e. RR /\ <. w , 0R >. e. RR ) <-> ( z e. R. /\ w e. R. ) )
7 6 biimpri 
 |-  ( ( z e. R. /\ w e. R. ) -> ( <. z , 0R >. e. RR /\ <. w , 0R >. e. RR ) )
8 df-i 
 |-  _i = <. 0R , 1R >.
9 8 oveq1i 
 |-  ( _i x. <. w , 0R >. ) = ( <. 0R , 1R >. x. <. w , 0R >. )
10 0r 
 |-  0R e. R.
11 1sr 
 |-  1R e. R.
12 mulcnsr 
 |-  ( ( ( 0R e. R. /\ 1R e. R. ) /\ ( w e. R. /\ 0R e. R. ) ) -> ( <. 0R , 1R >. x. <. w , 0R >. ) = <. ( ( 0R .R w ) +R ( -1R .R ( 1R .R 0R ) ) ) , ( ( 1R .R w ) +R ( 0R .R 0R ) ) >. )
13 10 11 12 mpanl12 
 |-  ( ( w e. R. /\ 0R e. R. ) -> ( <. 0R , 1R >. x. <. w , 0R >. ) = <. ( ( 0R .R w ) +R ( -1R .R ( 1R .R 0R ) ) ) , ( ( 1R .R w ) +R ( 0R .R 0R ) ) >. )
14 10 13 mpan2 
 |-  ( w e. R. -> ( <. 0R , 1R >. x. <. w , 0R >. ) = <. ( ( 0R .R w ) +R ( -1R .R ( 1R .R 0R ) ) ) , ( ( 1R .R w ) +R ( 0R .R 0R ) ) >. )
15 mulcomsr 
 |-  ( 0R .R w ) = ( w .R 0R )
16 00sr 
 |-  ( w e. R. -> ( w .R 0R ) = 0R )
17 15 16 eqtrid 
 |-  ( w e. R. -> ( 0R .R w ) = 0R )
18 17 oveq1d 
 |-  ( w e. R. -> ( ( 0R .R w ) +R ( -1R .R ( 1R .R 0R ) ) ) = ( 0R +R ( -1R .R ( 1R .R 0R ) ) ) )
19 00sr 
 |-  ( 1R e. R. -> ( 1R .R 0R ) = 0R )
20 11 19 ax-mp 
 |-  ( 1R .R 0R ) = 0R
21 20 oveq2i 
 |-  ( -1R .R ( 1R .R 0R ) ) = ( -1R .R 0R )
22 m1r 
 |-  -1R e. R.
23 00sr 
 |-  ( -1R e. R. -> ( -1R .R 0R ) = 0R )
24 22 23 ax-mp 
 |-  ( -1R .R 0R ) = 0R
25 21 24 eqtri 
 |-  ( -1R .R ( 1R .R 0R ) ) = 0R
26 25 oveq2i 
 |-  ( 0R +R ( -1R .R ( 1R .R 0R ) ) ) = ( 0R +R 0R )
27 0idsr 
 |-  ( 0R e. R. -> ( 0R +R 0R ) = 0R )
28 10 27 ax-mp 
 |-  ( 0R +R 0R ) = 0R
29 26 28 eqtri 
 |-  ( 0R +R ( -1R .R ( 1R .R 0R ) ) ) = 0R
30 18 29 eqtrdi 
 |-  ( w e. R. -> ( ( 0R .R w ) +R ( -1R .R ( 1R .R 0R ) ) ) = 0R )
31 mulcomsr 
 |-  ( 1R .R w ) = ( w .R 1R )
32 1idsr 
 |-  ( w e. R. -> ( w .R 1R ) = w )
33 31 32 eqtrid 
 |-  ( w e. R. -> ( 1R .R w ) = w )
34 33 oveq1d 
 |-  ( w e. R. -> ( ( 1R .R w ) +R ( 0R .R 0R ) ) = ( w +R ( 0R .R 0R ) ) )
35 00sr 
 |-  ( 0R e. R. -> ( 0R .R 0R ) = 0R )
36 10 35 ax-mp 
 |-  ( 0R .R 0R ) = 0R
37 36 oveq2i 
 |-  ( w +R ( 0R .R 0R ) ) = ( w +R 0R )
38 0idsr 
 |-  ( w e. R. -> ( w +R 0R ) = w )
39 37 38 eqtrid 
 |-  ( w e. R. -> ( w +R ( 0R .R 0R ) ) = w )
40 34 39 eqtrd 
 |-  ( w e. R. -> ( ( 1R .R w ) +R ( 0R .R 0R ) ) = w )
41 30 40 opeq12d 
 |-  ( w e. R. -> <. ( ( 0R .R w ) +R ( -1R .R ( 1R .R 0R ) ) ) , ( ( 1R .R w ) +R ( 0R .R 0R ) ) >. = <. 0R , w >. )
42 14 41 eqtrd 
 |-  ( w e. R. -> ( <. 0R , 1R >. x. <. w , 0R >. ) = <. 0R , w >. )
43 9 42 eqtrid 
 |-  ( w e. R. -> ( _i x. <. w , 0R >. ) = <. 0R , w >. )
44 43 oveq2d 
 |-  ( w e. R. -> ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) = ( <. z , 0R >. + <. 0R , w >. ) )
45 44 adantl 
 |-  ( ( z e. R. /\ w e. R. ) -> ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) = ( <. z , 0R >. + <. 0R , w >. ) )
46 addcnsr 
 |-  ( ( ( z e. R. /\ 0R e. R. ) /\ ( 0R e. R. /\ w e. R. ) ) -> ( <. z , 0R >. + <. 0R , w >. ) = <. ( z +R 0R ) , ( 0R +R w ) >. )
47 10 46 mpanl2 
 |-  ( ( z e. R. /\ ( 0R e. R. /\ w e. R. ) ) -> ( <. z , 0R >. + <. 0R , w >. ) = <. ( z +R 0R ) , ( 0R +R w ) >. )
48 10 47 mpanr1 
 |-  ( ( z e. R. /\ w e. R. ) -> ( <. z , 0R >. + <. 0R , w >. ) = <. ( z +R 0R ) , ( 0R +R w ) >. )
49 0idsr 
 |-  ( z e. R. -> ( z +R 0R ) = z )
50 addcomsr 
 |-  ( 0R +R w ) = ( w +R 0R )
51 50 38 eqtrid 
 |-  ( w e. R. -> ( 0R +R w ) = w )
52 opeq12 
 |-  ( ( ( z +R 0R ) = z /\ ( 0R +R w ) = w ) -> <. ( z +R 0R ) , ( 0R +R w ) >. = <. z , w >. )
53 49 51 52 syl2an 
 |-  ( ( z e. R. /\ w e. R. ) -> <. ( z +R 0R ) , ( 0R +R w ) >. = <. z , w >. )
54 45 48 53 3eqtrrd 
 |-  ( ( z e. R. /\ w e. R. ) -> <. z , w >. = ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) )
55 opex 
 |-  <. z , 0R >. e. _V
56 opex 
 |-  <. w , 0R >. e. _V
57 eleq1 
 |-  ( x = <. z , 0R >. -> ( x e. RR <-> <. z , 0R >. e. RR ) )
58 eleq1 
 |-  ( y = <. w , 0R >. -> ( y e. RR <-> <. w , 0R >. e. RR ) )
59 57 58 bi2anan9 
 |-  ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) -> ( ( x e. RR /\ y e. RR ) <-> ( <. z , 0R >. e. RR /\ <. w , 0R >. e. RR ) ) )
60 oveq1 
 |-  ( x = <. z , 0R >. -> ( x + ( _i x. y ) ) = ( <. z , 0R >. + ( _i x. y ) ) )
61 oveq2 
 |-  ( y = <. w , 0R >. -> ( _i x. y ) = ( _i x. <. w , 0R >. ) )
62 61 oveq2d 
 |-  ( y = <. w , 0R >. -> ( <. z , 0R >. + ( _i x. y ) ) = ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) )
63 60 62 sylan9eq 
 |-  ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) -> ( x + ( _i x. y ) ) = ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) )
64 63 eqeq2d 
 |-  ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) -> ( <. z , w >. = ( x + ( _i x. y ) ) <-> <. z , w >. = ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) ) )
65 59 64 anbi12d 
 |-  ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) -> ( ( ( x e. RR /\ y e. RR ) /\ <. z , w >. = ( x + ( _i x. y ) ) ) <-> ( ( <. z , 0R >. e. RR /\ <. w , 0R >. e. RR ) /\ <. z , w >. = ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) ) ) )
66 55 56 65 spc2ev 
 |-  ( ( ( <. z , 0R >. e. RR /\ <. w , 0R >. e. RR ) /\ <. z , w >. = ( <. z , 0R >. + ( _i x. <. w , 0R >. ) ) ) -> E. x E. y ( ( x e. RR /\ y e. RR ) /\ <. z , w >. = ( x + ( _i x. y ) ) ) )
67 7 54 66 syl2anc 
 |-  ( ( z e. R. /\ w e. R. ) -> E. x E. y ( ( x e. RR /\ y e. RR ) /\ <. z , w >. = ( x + ( _i x. y ) ) ) )
68 r2ex 
 |-  ( E. x e. RR E. y e. RR <. z , w >. = ( x + ( _i x. y ) ) <-> E. x E. y ( ( x e. RR /\ y e. RR ) /\ <. z , w >. = ( x + ( _i x. y ) ) ) )
69 67 68 sylibr 
 |-  ( ( z e. R. /\ w e. R. ) -> E. x e. RR E. y e. RR <. z , w >. = ( x + ( _i x. y ) ) )
70 1 3 69 optocl 
 |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )