Metamath Proof Explorer

Theorem 2halves

Description: Two halves make a whole. (Contributed by NM, 11-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
2 1 oveq1d 
 |-  ( A e. CC -> ( ( 2 x. A ) / 2 ) = ( ( A + A ) / 2 ) )
3 2cn 
 |-  2 e. CC
4 2ne0 
 |-  2 =/= 0
5 divcan3 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. A ) / 2 ) = A )
6 3 4 5 mp3an23 
 |-  ( A e. CC -> ( ( 2 x. A ) / 2 ) = A )
7 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
8 divdir 
 |-  ( ( A e. CC /\ A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( A + A ) / 2 ) = ( ( A / 2 ) + ( A / 2 ) ) )
9 7 8 mp3an3 
 |-  ( ( A e. CC /\ A e. CC ) -> ( ( A + A ) / 2 ) = ( ( A / 2 ) + ( A / 2 ) ) )
10 9 anidms 
 |-  ( A e. CC -> ( ( A + A ) / 2 ) = ( ( A / 2 ) + ( A / 2 ) ) )
11 2 6 10 3eqtr3rd 
 |-  ( A e. CC -> ( ( A / 2 ) + ( A / 2 ) ) = A )