Metamath Proof Explorer

Theorem resub

Description: Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005)

Ref Expression
Assertion resub 
|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A - B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 readd 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( Re ` ( A + -u B ) ) = ( ( Re ` A ) + ( Re ` -u B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + -u B ) ) = ( ( Re ` A ) + ( Re ` -u B ) ) )
4 reneg 
 |-  ( B e. CC -> ( Re ` -u B ) = -u ( Re ` B ) )
5 4 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` -u B ) = -u ( Re ` B ) )
6 5 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) + ( Re ` -u B ) ) = ( ( Re ` A ) + -u ( Re ` B ) ) )
7 3 6 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + -u B ) ) = ( ( Re ` A ) + -u ( Re ` B ) ) )
8 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
9 8 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + -u B ) ) = ( Re ` ( A - B ) ) )
10 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
11 10 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
12 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
13 12 recnd 
 |-  ( B e. CC -> ( Re ` B ) e. CC )
14 negsub 
 |-  ( ( ( Re ` A ) e. CC /\ ( Re ` B ) e. CC ) -> ( ( Re ` A ) + -u ( Re ` B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )
15 11 13 14 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) + -u ( Re ` B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )
16 7 9 15 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A - B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )