Metamath Proof Explorer

Theorem itsclc0yqsollem1

Description: Lemma 1 for itsclc0yqsol . (Contributed by AV, 6-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itscnhlc0yqe.t 
|- T = -u ( 2 x. ( B x. C ) )
itscnhlc0yqe.u 
|- U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
itsclc0yqsollem1.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion itsclc0yqsollem1 
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) = ( ( 4 x. ( A ^ 2 ) ) x. D ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2 itscnhlc0yqe.t 
 |-  T = -u ( 2 x. ( B x. C ) )
3 itscnhlc0yqe.u 
 |-  U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
4 itsclc0yqsollem1.d 
 |-  D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
5 2 oveq1i 
 |-  ( T ^ 2 ) = ( -u ( 2 x. ( B x. C ) ) ^ 2 )
6 2cnd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> 2 e. CC )
7 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> B e. CC )
8 simpl3 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> C e. CC )
9 7 8 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( B x. C ) e. CC )
10 6 9 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( 2 x. ( B x. C ) ) e. CC )
11 sqneg 
 |-  ( ( 2 x. ( B x. C ) ) e. CC -> ( -u ( 2 x. ( B x. C ) ) ^ 2 ) = ( ( 2 x. ( B x. C ) ) ^ 2 ) )
12 10 11 syl 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( -u ( 2 x. ( B x. C ) ) ^ 2 ) = ( ( 2 x. ( B x. C ) ) ^ 2 ) )
13 6 9 sqmuld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( 2 x. ( B x. C ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( B x. C ) ^ 2 ) ) )
14 sq2 
 |-  ( 2 ^ 2 ) = 4
15 14 a1i 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( 2 ^ 2 ) = 4 )
16 7 8 sqmuld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( B x. C ) ^ 2 ) = ( ( B ^ 2 ) x. ( C ^ 2 ) ) )
17 15 16 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( 2 ^ 2 ) x. ( ( B x. C ) ^ 2 ) ) = ( 4 x. ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
18 12 13 17 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( -u ( 2 x. ( B x. C ) ) ^ 2 ) = ( 4 x. ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
19 5 18 eqtrid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( T ^ 2 ) = ( 4 x. ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
20 1 3 oveq12i 
 |-  ( Q x. U ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) )
21 simpl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> A e. CC )
22 21 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( A ^ 2 ) e. CC )
23 7 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( B ^ 2 ) e. CC )
24 22 23 addcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. CC )
25 8 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( C ^ 2 ) e. CC )
26 simpr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> R e. CC )
27 26 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( R ^ 2 ) e. CC )
28 22 27 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( R ^ 2 ) ) e. CC )
29 24 25 28 subdid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
30 22 23 25 adddird 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( C ^ 2 ) ) = ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
31 22 23 28 adddird 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( B ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
32 30 31 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( B ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) )
33 23 25 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( B ^ 2 ) x. ( C ^ 2 ) ) e. CC )
34 22 25 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( C ^ 2 ) ) e. CC )
35 22 28 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) e. CC )
36 23 27 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( B ^ 2 ) x. ( R ^ 2 ) ) e. CC )
37 22 36 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) e. CC )
38 35 37 addcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) e. CC )
39 34 33 addcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) = ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) )
40 23 22 27 mul12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( B ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) )
41 40 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( B ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) )
42 39 41 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( B ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) )
43 33 34 38 42 assraddsubd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( B ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
44 29 32 43 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
45 20 44 eqtrid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( Q x. U ) = ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
46 45 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( 4 x. ( Q x. U ) ) = ( 4 x. ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) )
47 19 46 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) = ( ( 4 x. ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( 4 x. ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) )
48 4cn 
 |-  4 e. CC
49 48 a1i 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> 4 e. CC )
50 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
51 50 sqcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A ^ 2 ) e. CC )
52 51 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( A ^ 2 ) e. CC )
53 1 24 eqeltrid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> Q e. CC )
54 27 53 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( R ^ 2 ) x. Q ) e. CC )
55 54 25 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) e. CC )
56 4 55 eqeltrid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> D e. CC )
57 49 52 56 mulassd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( 4 x. ( A ^ 2 ) ) x. D ) = ( 4 x. ( ( A ^ 2 ) x. D ) ) )
58 34 38 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) e. CC )
59 33 33 58 subsub4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) )
60 33 subidd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) = 0 )
61 60 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( 0 - ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
62 0cnd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> 0 e. CC )
63 62 34 38 subsub2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( 0 - ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( 0 + ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) ) )
64 38 34 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) e. CC )
65 64 addlidd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( 0 + ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) )
66 61 63 65 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) )
67 59 66 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) = ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) )
68 22 28 36 adddid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( ( ( A ^ 2 ) x. ( R ^ 2 ) ) + ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) )
69 22 23 27 adddird 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) = ( ( ( A ^ 2 ) x. ( R ^ 2 ) ) + ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) )
70 69 eqcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) x. ( R ^ 2 ) ) + ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) )
71 70 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( ( ( A ^ 2 ) x. ( R ^ 2 ) ) + ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( A ^ 2 ) x. ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) ) )
72 68 71 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( A ^ 2 ) x. ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) ) )
73 72 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) = ( ( ( A ^ 2 ) x. ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) )
74 24 27 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) e. CC )
75 22 74 25 subdid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) ) = ( ( ( A ^ 2 ) x. ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) )
76 73 75 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( A ^ 2 ) x. ( C ^ 2 ) ) ) = ( ( A ^ 2 ) x. ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) ) )
77 1 a1i 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> Q = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
78 77 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( R ^ 2 ) x. Q ) = ( ( R ^ 2 ) x. ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
79 27 24 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( R ^ 2 ) x. ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) )
80 78 79 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( R ^ 2 ) x. Q ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) )
81 80 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) )
82 4 81 eqtrid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> D = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) )
83 82 eqcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) = D )
84 83 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( A ^ 2 ) x. ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) ) = ( ( A ^ 2 ) x. D ) )
85 67 76 84 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) = ( ( A ^ 2 ) x. D ) )
86 85 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( 4 x. ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) = ( 4 x. ( ( A ^ 2 ) x. D ) ) )
87 33 58 addcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) e. CC )
88 49 33 87 subdid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( 4 x. ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) = ( ( 4 x. ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( 4 x. ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) )
89 57 86 88 3eqtr2rd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( 4 x. ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) - ( 4 x. ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( A ^ 2 ) x. ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( ( B ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) = ( ( 4 x. ( A ^ 2 ) ) x. D ) )
90 47 89 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) = ( ( 4 x. ( A ^ 2 ) ) x. D ) )