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

Metamath Proof Explorer

Theorem crre

Description: The real part of a complex number representation. Definition 10-3.1 of Gleason p. 132. (Contributed by NM, 12-May-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion crre 
|- ( ( A e. RR /\ B e. RR ) -> ( Re ` ( A + ( _i x. B ) ) ) = A )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 ax-icn 
 |-  _i e. CC
3 recn 
 |-  ( B e. RR -> B e. CC )
4 mulcl 
 |-  ( ( _i e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
5 2 3 4 sylancr 
 |-  ( B e. RR -> ( _i x. B ) e. CC )
6 addcl 
 |-  ( ( A e. CC /\ ( _i x. B ) e. CC ) -> ( A + ( _i x. B ) ) e. CC )
7 1 5 6 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + ( _i x. B ) ) e. CC )
8 reval 
 |-  ( ( A + ( _i x. B ) ) e. CC -> ( Re ` ( A + ( _i x. B ) ) ) = ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) )
9 7 8 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( Re ` ( A + ( _i x. B ) ) ) = ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) )
10 cjcl 
 |-  ( ( A + ( _i x. B ) ) e. CC -> ( * ` ( A + ( _i x. B ) ) ) e. CC )
11 7 10 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( * ` ( A + ( _i x. B ) ) ) e. CC )
12 7 11 addcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) e. CC )
13 12 halfcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) e. CC )
14 1 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. CC )
15 recl 
 |-  ( ( A + ( _i x. B ) ) e. CC -> ( Re ` ( A + ( _i x. B ) ) ) e. RR )
16 7 15 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( Re ` ( A + ( _i x. B ) ) ) e. RR )
17 9 16 eqeltrrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) e. RR )
18 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
19 17 18 resubcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) e. RR )
20 2 a1i 
 |-  ( ( A e. RR /\ B e. RR ) -> _i e. CC )
21 3 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
22 2 21 4 sylancr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( _i x. B ) e. CC )
23 7 11 subcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) e. CC )
24 23 halfcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) e. CC )
25 20 22 24 subdid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( _i x. ( ( _i x. B ) - ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) ) = ( ( _i x. ( _i x. B ) ) - ( _i x. ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) ) )
26 14 22 14 pnpcand 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) - ( A + A ) ) = ( ( _i x. B ) - A ) )
27 22 14 22 pnpcan2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( _i x. B ) + ( _i x. B ) ) - ( A + ( _i x. B ) ) ) = ( ( _i x. B ) - A ) )
28 26 27 eqtr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) - ( A + A ) ) = ( ( ( _i x. B ) + ( _i x. B ) ) - ( A + ( _i x. B ) ) ) )
29 28 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) - ( A + A ) ) + ( * ` ( A + ( _i x. B ) ) ) ) = ( ( ( ( _i x. B ) + ( _i x. B ) ) - ( A + ( _i x. B ) ) ) + ( * ` ( A + ( _i x. B ) ) ) ) )
30 14 14 addcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + A ) e. CC )
31 7 11 30 addsubd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) - ( A + A ) ) = ( ( ( A + ( _i x. B ) ) - ( A + A ) ) + ( * ` ( A + ( _i x. B ) ) ) ) )
32 22 22 addcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( _i x. B ) + ( _i x. B ) ) e. CC )
33 32 7 11 subsubd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( _i x. B ) + ( _i x. B ) ) - ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) = ( ( ( ( _i x. B ) + ( _i x. B ) ) - ( A + ( _i x. B ) ) ) + ( * ` ( A + ( _i x. B ) ) ) ) )
34 29 31 33 3eqtr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) - ( A + A ) ) = ( ( ( _i x. B ) + ( _i x. B ) ) - ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) )
35 14 2timesd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2 x. A ) = ( A + A ) )
36 35 oveq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) - ( 2 x. A ) ) = ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) - ( A + A ) ) )
37 22 2timesd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2 x. ( _i x. B ) ) = ( ( _i x. B ) + ( _i x. B ) ) )
38 37 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 2 x. ( _i x. B ) ) - ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) = ( ( ( _i x. B ) + ( _i x. B ) ) - ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) )
39 34 36 38 3eqtr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) - ( 2 x. A ) ) = ( ( 2 x. ( _i x. B ) ) - ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) )
40 39 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) - ( 2 x. A ) ) / 2 ) = ( ( ( 2 x. ( _i x. B ) ) - ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) / 2 ) )
41 2cn 
 |-  2 e. CC
42 mulcl 
 |-  ( ( 2 e. CC /\ A e. CC ) -> ( 2 x. A ) e. CC )
43 41 14 42 sylancr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2 x. A ) e. CC )
44 41 a1i 
 |-  ( ( A e. RR /\ B e. RR ) -> 2 e. CC )
45 2ne0 
 |-  2 =/= 0
46 45 a1i 
 |-  ( ( A e. RR /\ B e. RR ) -> 2 =/= 0 )
47 12 43 44 46 divsubdird 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) - ( 2 x. A ) ) / 2 ) = ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - ( ( 2 x. A ) / 2 ) ) )
48 mulcl 
 |-  ( ( 2 e. CC /\ ( _i x. B ) e. CC ) -> ( 2 x. ( _i x. B ) ) e. CC )
49 41 22 48 sylancr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2 x. ( _i x. B ) ) e. CC )
50 49 23 44 46 divsubdird 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( 2 x. ( _i x. B ) ) - ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) / 2 ) = ( ( ( 2 x. ( _i x. B ) ) / 2 ) - ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) )
51 40 47 50 3eqtr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - ( ( 2 x. A ) / 2 ) ) = ( ( ( 2 x. ( _i x. B ) ) / 2 ) - ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) )
52 14 44 46 divcan3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 2 x. A ) / 2 ) = A )
53 52 oveq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - ( ( 2 x. A ) / 2 ) ) = ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) )
54 22 44 46 divcan3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 2 x. ( _i x. B ) ) / 2 ) = ( _i x. B ) )
55 54 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( 2 x. ( _i x. B ) ) / 2 ) - ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) = ( ( _i x. B ) - ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) )
56 51 53 55 3eqtr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) = ( ( _i x. B ) - ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) )
57 56 oveq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( _i x. ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) ) = ( _i x. ( ( _i x. B ) - ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) ) )
58 20 20 21 mulassd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( _i x. _i ) x. B ) = ( _i x. ( _i x. B ) ) )
59 20 23 44 46 divassd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) / 2 ) = ( _i x. ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) )
60 58 59 oveq12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( _i x. _i ) x. B ) - ( ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) / 2 ) ) = ( ( _i x. ( _i x. B ) ) - ( _i x. ( ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) ) ) )
61 25 57 60 3eqtr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( _i x. ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) ) = ( ( ( _i x. _i ) x. B ) - ( ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) / 2 ) ) )
62 ixi 
 |-  ( _i x. _i ) = -u 1
63 neg1rr 
 |-  -u 1 e. RR
64 62 63 eqeltri 
 |-  ( _i x. _i ) e. RR
65 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
66 remulcl 
 |-  ( ( ( _i x. _i ) e. RR /\ B e. RR ) -> ( ( _i x. _i ) x. B ) e. RR )
67 64 65 66 sylancr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( _i x. _i ) x. B ) e. RR )
68 cjth 
 |-  ( ( A + ( _i x. B ) ) e. CC -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) e. RR /\ ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) e. RR ) )
69 68 simprd 
 |-  ( ( A + ( _i x. B ) ) e. CC -> ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) e. RR )
70 7 69 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) e. RR )
71 70 rehalfcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) / 2 ) e. RR )
72 67 71 resubcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( _i x. _i ) x. B ) - ( ( _i x. ( ( A + ( _i x. B ) ) - ( * ` ( A + ( _i x. B ) ) ) ) ) / 2 ) ) e. RR )
73 61 72 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( _i x. ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) ) e. RR )
74 rimul 
 |-  ( ( ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) e. RR /\ ( _i x. ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) ) e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) = 0 )
75 19 73 74 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) - A ) = 0 )
76 13 14 75 subeq0d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + ( _i x. B ) ) + ( * ` ( A + ( _i x. B ) ) ) ) / 2 ) = A )
77 9 76 eqtrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( Re ` ( A + ( _i x. B ) ) ) = A )