Metamath Proof Explorer

Theorem 1mhlfehlf

Description: Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler, 4-Jan-2017) (Proof shortened by SN, 22-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 halfcn 
 |-  ( 1 / 2 ) e. CC
3 2halves 
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
4 1 3 ax-mp 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
5 1 2 2 4 subaddrii 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )