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

Metamath Proof Explorer

Theorem binom2subadd

Description: The difference of the squares of the sum and difference of two complex numbers A and B . (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Hypotheses binom2subadd.1 
|- ( ph -> A e. CC )
binom2subadd.2 
|- ( ph -> B e. CC )
Assertion binom2subadd 
|- ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) )

Proof

Step Hyp Ref Expression
1 binom2subadd.1 
 |-  ( ph -> A e. CC )
2 binom2subadd.2 
 |-  ( ph -> B e. CC )
3 1 2 addcld 
 |-  ( ph -> ( A + B ) e. CC )
4 1 2 subcld 
 |-  ( ph -> ( A - B ) e. CC )
5 subsq 
 |-  ( ( ( A + B ) e. CC /\ ( A - B ) e. CC ) -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( ( ( A + B ) + ( A - B ) ) x. ( ( A + B ) - ( A - B ) ) ) )
6 3 4 5 syl2anc 
 |-  ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( ( ( A + B ) + ( A - B ) ) x. ( ( A + B ) - ( A - B ) ) ) )
7 1 2 1 ppncand 
 |-  ( ph -> ( ( A + B ) + ( A - B ) ) = ( A + A ) )
8 1 2timesd 
 |-  ( ph -> ( 2 x. A ) = ( A + A ) )
9 7 8 eqtr4d 
 |-  ( ph -> ( ( A + B ) + ( A - B ) ) = ( 2 x. A ) )
10 1 2 2 pnncand 
 |-  ( ph -> ( ( A + B ) - ( A - B ) ) = ( B + B ) )
11 2 2timesd 
 |-  ( ph -> ( 2 x. B ) = ( B + B ) )
12 10 11 eqtr4d 
 |-  ( ph -> ( ( A + B ) - ( A - B ) ) = ( 2 x. B ) )
13 9 12 oveq12d 
 |-  ( ph -> ( ( ( A + B ) + ( A - B ) ) x. ( ( A + B ) - ( A - B ) ) ) = ( ( 2 x. A ) x. ( 2 x. B ) ) )
14 2cnd 
 |-  ( ph -> 2 e. CC )
15 14 1 14 2 mul4d 
 |-  ( ph -> ( ( 2 x. A ) x. ( 2 x. B ) ) = ( ( 2 x. 2 ) x. ( A x. B ) ) )
16 6 13 15 3eqtrd 
 |-  ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( ( 2 x. 2 ) x. ( A x. B ) ) )
17 2t2e4 
 |-  ( 2 x. 2 ) = 4
18 17 oveq1i 
 |-  ( ( 2 x. 2 ) x. ( A x. B ) ) = ( 4 x. ( A x. B ) )
19 16 18 eqtrdi 
 |-  ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) )