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 ∈ ℂ
2		ax-1cn	⊢ 1 ∈ ℂ
3		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
4		divsubdir	⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 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 )