Metamath Proof Explorer

Theorem 2itscplem1

Description: Lemma 1 for 2itscp . (Contributed by AV, 4-Mar-2023)

Ref Expression
Hypotheses 2itscp.a 
|- ( ph -> A e. RR )
2itscp.b 
|- ( ph -> B e. RR )
2itscp.x 
|- ( ph -> X e. RR )
2itscp.y 
|- ( ph -> Y e. RR )
2itscp.d 
|- D = ( X - A )
2itscp.e 
|- E = ( B - Y )
Assertion 2itscplem1 
|- ( ph -> ( ( ( ( E ^ 2 ) x. ( B ^ 2 ) ) + ( ( D ^ 2 ) x. ( A ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) = ( ( ( D x. A ) - ( E x. B ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 2itscp.a 
 |-  ( ph -> A e. RR )
2 2itscp.b 
 |-  ( ph -> B e. RR )
3 2itscp.x 
 |-  ( ph -> X e. RR )
4 2itscp.y 
 |-  ( ph -> Y e. RR )
5 2itscp.d 
 |-  D = ( X - A )
6 2itscp.e 
 |-  E = ( B - Y )
7 2 recnd 
 |-  ( ph -> B e. CC )
8 4 recnd 
 |-  ( ph -> Y e. CC )
9 7 8 subcld 
 |-  ( ph -> ( B - Y ) e. CC )
10 6 9 eqeltrid 
 |-  ( ph -> E e. CC )
11 10 sqcld 
 |-  ( ph -> ( E ^ 2 ) e. CC )
12 7 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
13 11 12 mulcld 
 |-  ( ph -> ( ( E ^ 2 ) x. ( B ^ 2 ) ) e. CC )
14 3 recnd 
 |-  ( ph -> X e. CC )
15 1 recnd 
 |-  ( ph -> A e. CC )
16 14 15 subcld 
 |-  ( ph -> ( X - A ) e. CC )
17 5 16 eqeltrid 
 |-  ( ph -> D e. CC )
18 17 sqcld 
 |-  ( ph -> ( D ^ 2 ) e. CC )
19 15 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
20 18 19 mulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( A ^ 2 ) ) e. CC )
21 2cnd 
 |-  ( ph -> 2 e. CC )
22 17 15 mulcld 
 |-  ( ph -> ( D x. A ) e. CC )
23 10 7 mulcld 
 |-  ( ph -> ( E x. B ) e. CC )
24 22 23 mulcld 
 |-  ( ph -> ( ( D x. A ) x. ( E x. B ) ) e. CC )
25 21 24 mulcld 
 |-  ( ph -> ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) e. CC )
26 13 20 25 addsubassd 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( B ^ 2 ) ) + ( ( D ^ 2 ) x. ( A ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) = ( ( ( E ^ 2 ) x. ( B ^ 2 ) ) + ( ( ( D ^ 2 ) x. ( A ^ 2 ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) ) )
27 20 25 subcld 
 |-  ( ph -> ( ( ( D ^ 2 ) x. ( A ^ 2 ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) e. CC )
28 13 27 addcomd 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( B ^ 2 ) ) + ( ( ( D ^ 2 ) x. ( A ^ 2 ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) ) = ( ( ( ( D ^ 2 ) x. ( A ^ 2 ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( B ^ 2 ) ) ) )
29 17 15 sqmuld 
 |-  ( ph -> ( ( D x. A ) ^ 2 ) = ( ( D ^ 2 ) x. ( A ^ 2 ) ) )
30 29 eqcomd 
 |-  ( ph -> ( ( D ^ 2 ) x. ( A ^ 2 ) ) = ( ( D x. A ) ^ 2 ) )
31 30 oveq1d 
 |-  ( ph -> ( ( ( D ^ 2 ) x. ( A ^ 2 ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) = ( ( ( D x. A ) ^ 2 ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )
32 10 7 sqmuld 
 |-  ( ph -> ( ( E x. B ) ^ 2 ) = ( ( E ^ 2 ) x. ( B ^ 2 ) ) )
33 32 eqcomd 
 |-  ( ph -> ( ( E ^ 2 ) x. ( B ^ 2 ) ) = ( ( E x. B ) ^ 2 ) )
34 31 33 oveq12d 
 |-  ( ph -> ( ( ( ( D ^ 2 ) x. ( A ^ 2 ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( B ^ 2 ) ) ) = ( ( ( ( D x. A ) ^ 2 ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E x. B ) ^ 2 ) ) )
35 26 28 34 3eqtrd 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( B ^ 2 ) ) + ( ( D ^ 2 ) x. ( A ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) = ( ( ( ( D x. A ) ^ 2 ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E x. B ) ^ 2 ) ) )
36 binom2sub 
 |-  ( ( ( D x. A ) e. CC /\ ( E x. B ) e. CC ) -> ( ( ( D x. A ) - ( E x. B ) ) ^ 2 ) = ( ( ( ( D x. A ) ^ 2 ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E x. B ) ^ 2 ) ) )
37 22 23 36 syl2anc 
 |-  ( ph -> ( ( ( D x. A ) - ( E x. B ) ) ^ 2 ) = ( ( ( ( D x. A ) ^ 2 ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E x. B ) ^ 2 ) ) )
38 35 37 eqtr4d 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( B ^ 2 ) ) + ( ( D ^ 2 ) x. ( A ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) = ( ( ( D x. A ) - ( E x. B ) ) ^ 2 ) )