Step |
Hyp |
Ref |
Expression |
1 |
|
simprl |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR ) |
2 |
1
|
recnd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. CC ) |
3 |
2
|
sqcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C ^ 2 ) e. CC ) |
4 |
|
simprr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR ) |
5 |
4
|
recnd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. CC ) |
6 |
5
|
sqcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( D ^ 2 ) e. CC ) |
7 |
3 6
|
addcomd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( C ^ 2 ) + ( D ^ 2 ) ) = ( ( D ^ 2 ) + ( C ^ 2 ) ) ) |
8 |
7
|
oveq2d |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( D ^ 2 ) + ( C ^ 2 ) ) ) ) |
9 |
|
bhmafibid1 |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( D e. RR /\ C e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( D ^ 2 ) + ( C ^ 2 ) ) ) = ( ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) + ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) ) ) |
10 |
9
|
ancom2s |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( D ^ 2 ) + ( C ^ 2 ) ) ) = ( ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) + ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) ) ) |
11 |
|
simpll |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR ) |
12 |
11
|
recnd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. CC ) |
13 |
12 5
|
mulcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. D ) e. CC ) |
14 |
|
simplr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. RR ) |
15 |
14
|
recnd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. CC ) |
16 |
15 2
|
mulcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. C ) e. CC ) |
17 |
13 16
|
subcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A x. D ) - ( B x. C ) ) e. CC ) |
18 |
17
|
sqcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) e. CC ) |
19 |
12 2
|
mulcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. C ) e. CC ) |
20 |
15 5
|
mulcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. D ) e. CC ) |
21 |
19 20
|
addcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A x. C ) + ( B x. D ) ) e. CC ) |
22 |
21
|
sqcld |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) e. CC ) |
23 |
18 22
|
addcomd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) + ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) ) = ( ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) ) ) |
24 |
8 10 23
|
3eqtrd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( ( A x. C ) + ( B x. D ) ) ^ 2 ) + ( ( ( A x. D ) - ( B x. C ) ) ^ 2 ) ) ) |