Metamath Proof Explorer

Theorem halfaddsub

Description: Sum and difference of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007)

Ref Expression
Assertion halfaddsub 
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) = A /\ ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) = B ) )

Proof

Step Hyp Ref Expression
1 ppncan 
 |-  ( ( A e. CC /\ B e. CC /\ A e. CC ) -> ( ( A + B ) + ( A - B ) ) = ( A + A ) )
2 1 3anidm13 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + ( A - B ) ) = ( A + A ) )
3 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
4 3 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. A ) = ( A + A ) )
5 2 4 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + ( A - B ) ) = ( 2 x. A ) )
6 5 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) + ( A - B ) ) / 2 ) = ( ( 2 x. A ) / 2 ) )
7 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
8 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
9 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
10 divdir 
 |-  ( ( ( A + B ) e. CC /\ ( A - B ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( A + B ) + ( A - B ) ) / 2 ) = ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) )
11 9 10 mp3an3 
 |-  ( ( ( A + B ) e. CC /\ ( A - B ) e. CC ) -> ( ( ( A + B ) + ( A - B ) ) / 2 ) = ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) )
12 7 8 11 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) + ( A - B ) ) / 2 ) = ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) )
13 2cn 
 |-  2 e. CC
14 2ne0 
 |-  2 =/= 0
15 divcan3 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. A ) / 2 ) = A )
16 13 14 15 mp3an23 
 |-  ( A e. CC -> ( ( 2 x. A ) / 2 ) = A )
17 16 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. A ) / 2 ) = A )
18 6 12 17 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) = A )
19 pnncan 
 |-  ( ( A e. CC /\ B e. CC /\ B e. CC ) -> ( ( A + B ) - ( A - B ) ) = ( B + B ) )
20 19 3anidm23 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - ( A - B ) ) = ( B + B ) )
21 2times 
 |-  ( B e. CC -> ( 2 x. B ) = ( B + B ) )
22 21 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. B ) = ( B + B ) )
23 20 22 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - ( A - B ) ) = ( 2 x. B ) )
24 23 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) - ( A - B ) ) / 2 ) = ( ( 2 x. B ) / 2 ) )
25 divsubdir 
 |-  ( ( ( A + B ) e. CC /\ ( A - B ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( A + B ) - ( A - B ) ) / 2 ) = ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) )
26 9 25 mp3an3 
 |-  ( ( ( A + B ) e. CC /\ ( A - B ) e. CC ) -> ( ( ( A + B ) - ( A - B ) ) / 2 ) = ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) )
27 7 8 26 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) - ( A - B ) ) / 2 ) = ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) )
28 divcan3 
 |-  ( ( B e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. B ) / 2 ) = B )
29 13 14 28 mp3an23 
 |-  ( B e. CC -> ( ( 2 x. B ) / 2 ) = B )
30 29 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. B ) / 2 ) = B )
31 24 27 30 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) = B )
32 18 31 jca 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) = A /\ ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) = B ) )