Metamath Proof Explorer

Theorem 2halves

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

Ref Expression
Assertion 2halves ⊢ A ∈ ℂ → A 2 + A 2 = A

Proof

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