This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2halves

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

Ref Expression
Assertion 2halves ( 𝐴 ∈ ℂ → ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 2times ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
2 1 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · 𝐴 ) / 2 ) = ( ( 𝐴 + 𝐴 ) / 2 ) )
3 2cn ⊢ 2 ∈ ℂ
4 2ne0 ⊢ 2 ≠ 0
5 divcan3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
6 3 4 5 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
7 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
8 divdir ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝐴 + 𝐴 ) / 2 ) = ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) )
9 7 8 mp3an3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 + 𝐴 ) / 2 ) = ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) )
10 9 anidms ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + 𝐴 ) / 2 ) = ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) )
11 2 6 10 3eqtr3rd ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / 2 ) + ( 𝐴 / 2 ) ) = 𝐴 )