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

Metamath Proof Explorer

Theorem subsq2

Description: Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008)

Ref Expression
Assertion subsq2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( ( 𝐴 − 𝐵 ) ↑ 2 ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 2cn ⊢ 2 ∈ ℂ
2 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) ∈ ℂ )
3 1 2 mpan ⊢ ( 𝐵 ∈ ℂ → ( 2 · 𝐵 ) ∈ ℂ )
4 3 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) ∈ ℂ )
5 subadd23 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 2 · 𝐵 ) ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) = ( 𝐴 + ( ( 2 · 𝐵 ) − 𝐵 ) ) )
6 4 5 mpd3an3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) = ( 𝐴 + ( ( 2 · 𝐵 ) − 𝐵 ) ) )
7 2txmxeqx ⊢ ( 𝐵 ∈ ℂ → ( ( 2 · 𝐵 ) − 𝐵 ) = 𝐵 )
8 7 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · 𝐵 ) − 𝐵 ) = 𝐵 )
9 8 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + ( ( 2 · 𝐵 ) − 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
10 6 9 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
11 10 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
12 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
13 12 4 12 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )
14 11 13 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )
15 subsq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
16 sqval ⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( 𝐴 − 𝐵 ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
17 12 16 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
18 17 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) ↑ 2 ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) = ( ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )
19 14 15 18 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( ( 𝐴 − 𝐵 ) ↑ 2 ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )