Metamath Proof Explorer

Theorem 1mhlfehlf

Description: Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler, 4-Jan-2017)

Ref Expression
Assertion 1mhlfehlf 
|- ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 ax-1cn 
 |-  1 e. CC
3 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
4 divsubdir 
 |-  ( ( 2 e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 - 1 ) / 2 ) = ( ( 2 / 2 ) - ( 1 / 2 ) ) )
5 1 2 3 4 mp3an 
 |-  ( ( 2 - 1 ) / 2 ) = ( ( 2 / 2 ) - ( 1 / 2 ) )
6 2m1e1 
 |-  ( 2 - 1 ) = 1
7 6 oveq1i 
 |-  ( ( 2 - 1 ) / 2 ) = ( 1 / 2 )
8 2div2e1 
 |-  ( 2 / 2 ) = 1
9 8 oveq1i 
 |-  ( ( 2 / 2 ) - ( 1 / 2 ) ) = ( 1 - ( 1 / 2 ) )
10 5 7 9 3eqtr3ri 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )