Metamath Proof Explorer

Theorem 2itscplem3

Description: Lemma D 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 ) )
2itscp.r 
|- ( ph -> R e. RR )
2itscplem3.q 
|- Q = ( ( E ^ 2 ) + ( D ^ 2 ) )
2itscplem3.s 
|- S = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion 2itscplem3 
|- ( ph -> S = ( ( ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )

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 2itscp.r 
 |-  ( ph -> R e. RR )
9 2itscplem3.q 
 |-  Q = ( ( E ^ 2 ) + ( D ^ 2 ) )
10 2itscplem3.s 
 |-  S = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
11 10 a1i 
 |-  ( ph -> S = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) )
12 9 a1i 
 |-  ( ph -> Q = ( ( E ^ 2 ) + ( D ^ 2 ) ) )
13 12 oveq2d 
 |-  ( ph -> ( ( R ^ 2 ) x. Q ) = ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) )
14 8 recnd 
 |-  ( ph -> R e. CC )
15 14 sqcld 
 |-  ( ph -> ( R ^ 2 ) e. CC )
16 2 recnd 
 |-  ( ph -> B e. CC )
17 4 recnd 
 |-  ( ph -> Y e. CC )
18 16 17 subcld 
 |-  ( ph -> ( B - Y ) e. CC )
19 6 18 eqeltrid 
 |-  ( ph -> E e. CC )
20 19 sqcld 
 |-  ( ph -> ( E ^ 2 ) e. CC )
21 3 recnd 
 |-  ( ph -> X e. CC )
22 1 recnd 
 |-  ( ph -> A e. CC )
23 21 22 subcld 
 |-  ( ph -> ( X - A ) e. CC )
24 5 23 eqeltrid 
 |-  ( ph -> D e. CC )
25 24 sqcld 
 |-  ( ph -> ( D ^ 2 ) e. CC )
26 20 25 addcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( D ^ 2 ) ) e. CC )
27 15 26 mulcomd 
 |-  ( ph -> ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( R ^ 2 ) ) )
28 20 25 15 adddird 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( R ^ 2 ) ) = ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) )
29 13 27 28 3eqtrd 
 |-  ( ph -> ( ( R ^ 2 ) x. Q ) = ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) )
30 1 2 3 4 5 6 7 2itscplem2 
 |-  ( ph -> ( C ^ 2 ) = ( ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) )
31 29 30 oveq12d 
 |-  ( ph -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) = ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) ) )
32 20 15 mulcld 
 |-  ( ph -> ( ( E ^ 2 ) x. ( R ^ 2 ) ) e. CC )
33 25 15 mulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( R ^ 2 ) ) e. CC )
34 32 33 addcld 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) e. CC )
35 16 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
36 25 35 mulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( B ^ 2 ) ) e. CC )
37 2cnd 
 |-  ( ph -> 2 e. CC )
38 24 22 mulcld 
 |-  ( ph -> ( D x. A ) e. CC )
39 19 16 mulcld 
 |-  ( ph -> ( E x. B ) e. CC )
40 38 39 mulcld 
 |-  ( ph -> ( ( D x. A ) x. ( E x. B ) ) e. CC )
41 37 40 mulcld 
 |-  ( ph -> ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) e. CC )
42 34 36 41 subsub4d 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) = ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) ) )
43 42 eqcomd 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) ) = ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )
44 43 oveq1d 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) )
45 34 36 subcld 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) e. CC )
46 22 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
47 20 46 mulcld 
 |-  ( ph -> ( ( E ^ 2 ) x. ( A ^ 2 ) ) e. CC )
48 45 41 47 sub32d 
 |-  ( ph -> ( ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )
49 44 48 eqtrd 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )
50 36 41 addcld 
 |-  ( ph -> ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) e. CC )
51 34 50 47 subsub4d 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) ) )
52 32 33 36 addsubassd 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) = ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( ( D ^ 2 ) x. ( R ^ 2 ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) ) )
53 25 15 35 subdid 
 |-  ( ph -> ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) = ( ( ( D ^ 2 ) x. ( R ^ 2 ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) )
54 53 eqcomd 
 |-  ( ph -> ( ( ( D ^ 2 ) x. ( R ^ 2 ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) = ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) )
55 54 oveq2d 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( ( D ^ 2 ) x. ( R ^ 2 ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) ) = ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) )
56 52 55 eqtrd 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) = ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) )
57 56 oveq1d 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) )
58 15 35 subcld 
 |-  ( ph -> ( ( R ^ 2 ) - ( B ^ 2 ) ) e. CC )
59 25 58 mulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) e. CC )
60 32 59 47 addsubd 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) )
61 20 15 46 subdid 
 |-  ( ph -> ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) = ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) )
62 61 eqcomd 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) )
63 62 oveq1d 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) = ( ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) )
64 57 60 63 3eqtrd 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) = ( ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) )
65 64 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( D ^ 2 ) x. ( B ^ 2 ) ) ) - ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) = ( ( ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )
66 49 51 65 3eqtr3d 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( ( ( ( D ^ 2 ) x. ( B ^ 2 ) ) + ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) + ( ( E ^ 2 ) x. ( A ^ 2 ) ) ) ) = ( ( ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )
67 11 31 66 3eqtrd 
 |-  ( ph -> S = ( ( ( ( E ^ 2 ) x. ( ( R ^ 2 ) - ( A ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( R ^ 2 ) - ( B ^ 2 ) ) ) ) - ( 2 x. ( ( D x. A ) x. ( E x. B ) ) ) ) )