Metamath Proof Explorer

Theorem 2itscplem2

Description: Lemma 2 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 )
2itscp.c 
|- C = ( ( D x. B ) + ( E x. A ) )
Assertion 2itscplem2 
|- ( ph -> ( C ^ 2 ) = ( ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( A ^ 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 2itscp.c 
 |-  C = ( ( D x. B ) + ( E x. A ) )
8 7 oveq1i 
 |-  ( C ^ 2 ) = ( ( ( D x. B ) + ( E x. A ) ) ^ 2 )
9 8 a1i 
 |-  ( ph -> ( C ^ 2 ) = ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) )
10 3 recnd 
 |-  ( ph -> X e. CC )
11 1 recnd 
 |-  ( ph -> A e. CC )
12 10 11 subcld 
 |-  ( ph -> ( X - A ) e. CC )
13 5 12 eqeltrid 
 |-  ( ph -> D e. CC )
14 2 recnd 
 |-  ( ph -> B e. CC )
15 13 14 mulcld 
 |-  ( ph -> ( D x. B ) e. CC )
16 4 recnd 
 |-  ( ph -> Y e. CC )
17 14 16 subcld 
 |-  ( ph -> ( B - Y ) e. CC )
18 6 17 eqeltrid 
 |-  ( ph -> E e. CC )
19 18 11 mulcld 
 |-  ( ph -> ( E x. A ) e. CC )
20 binom2 
 |-  ( ( ( D x. B ) e. CC /\ ( E x. A ) e. CC ) -> ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) = ( ( ( ( D x. B ) ^ 2 ) + ( 2 x. ( ( D x. B ) x. ( E x. A ) ) ) ) + ( ( E x. A ) ^ 2 ) ) )
21 15 19 20 syl2anc 
 |-  ( ph -> ( ( ( D x. B ) + ( E x. A ) ) ^ 2 ) = ( ( ( ( D x. B ) ^ 2 ) + ( 2 x. ( ( D x. B ) x. ( E x. A ) ) ) ) + ( ( E x. A ) ^ 2 ) ) )
22 13 14 sqmuld 
 |-  ( ph -> ( ( D x. B ) ^ 2 ) = ( ( D ^ 2 ) x. ( B ^ 2 ) ) )
23 mul4r 
 |-  ( ( ( D e. CC /\ B e. CC ) /\ ( E e. CC /\ A e. CC ) ) -> ( ( D x. B ) x. ( E x. A ) ) = ( ( D x. A ) x. ( E x. B ) ) )
24 13 14 18 11 23 syl22anc 
 |-  ( ph -> ( ( D x. B ) x. ( E x. A ) ) = ( ( D x. A ) x. ( E x. B ) ) )
25 24 oveq2d 
 |-  ( ph -> ( 2 x. ( ( D x. B ) x. ( E x. A ) ) ) = ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) )
26 22 25 oveq12d 
 |-  ( ph -> ( ( ( D x. B ) ^ 2 ) + ( 2 x. ( ( D x. B ) x. ( E x. A ) ) ) ) = ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )
27 18 11 sqmuld 
 |-  ( ph -> ( ( E x. A ) ^ 2 ) = ( ( E ^ 2 ) x. ( A ^ 2 ) ) )
28 26 27 oveq12d 
 |-  ( ph -> ( ( ( ( D x. B ) ^ 2 ) + ( 2 x. ( ( D x. B ) x. ( E x. A ) ) ) ) + ( ( E x. A ) ^ 2 ) ) = ( ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) )
29 9 21 28 3eqtrd 
 |-  ( ph -> ( C ^ 2 ) = ( ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) )