Metamath Proof Explorer

Theorem subhalfhalf

Description: Subtracting the half of a number from the number yields the half of the number. (Contributed by AV, 28-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. CC -> A e. CC )
2 2cnd 
 |-  ( A e. CC -> 2 e. CC )
3 2ne0 
 |-  2 =/= 0
4 3 a1i 
 |-  ( A e. CC -> 2 =/= 0 )
5 1 2 4 divcan1d 
 |-  ( A e. CC -> ( ( A / 2 ) x. 2 ) = A )
6 5 eqcomd 
 |-  ( A e. CC -> A = ( ( A / 2 ) x. 2 ) )
7 6 oveq1d 
 |-  ( A e. CC -> ( A - ( A / 2 ) ) = ( ( ( A / 2 ) x. 2 ) - ( A / 2 ) ) )
8 halfcl 
 |-  ( A e. CC -> ( A / 2 ) e. CC )
9 8 2 mulcomd 
 |-  ( A e. CC -> ( ( A / 2 ) x. 2 ) = ( 2 x. ( A / 2 ) ) )
10 9 oveq1d 
 |-  ( A e. CC -> ( ( ( A / 2 ) x. 2 ) - ( A / 2 ) ) = ( ( 2 x. ( A / 2 ) ) - ( A / 2 ) ) )
11 2 8 mulsubfacd 
 |-  ( A e. CC -> ( ( 2 x. ( A / 2 ) ) - ( A / 2 ) ) = ( ( 2 - 1 ) x. ( A / 2 ) ) )
12 2m1e1 
 |-  ( 2 - 1 ) = 1
13 12 a1i 
 |-  ( A e. CC -> ( 2 - 1 ) = 1 )
14 13 oveq1d 
 |-  ( A e. CC -> ( ( 2 - 1 ) x. ( A / 2 ) ) = ( 1 x. ( A / 2 ) ) )
15 8 mulid2d 
 |-  ( A e. CC -> ( 1 x. ( A / 2 ) ) = ( A / 2 ) )
16 11 14 15 3eqtrd 
 |-  ( A e. CC -> ( ( 2 x. ( A / 2 ) ) - ( A / 2 ) ) = ( A / 2 ) )
17 7 10 16 3eqtrd 
 |-  ( A e. CC -> ( A - ( A / 2 ) ) = ( A / 2 ) )