Metamath Proof Explorer

Theorem bhmafibid1

Description: The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. Remark: The proof uses a different approach than the proof of bhmafibid1cn , and is a little bit shorter. (Contributed by Thierry Arnoux, 1-Feb-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bhmafibid1 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
2 1 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
3 ax-icn ⊢ i ∈ ℂ
4 3 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → i ∈ ℂ )
5 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
6 5 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
7 4 6 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( i · 𝐵 ) ∈ ℂ )
8 2 7 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
9 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
10 9 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
11 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℝ )
12 11 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
13 4 12 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( i · 𝐷 ) ∈ ℂ )
14 10 13 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℂ )
15 8 14 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℂ )
16 15 replimd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) = ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) + ( i · ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ) ) )
17 8 14 remuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) − ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ) )
18 1 5 crred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )
19 9 11 crred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐶 )
20 18 19 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( 𝐴 · 𝐶 ) )
21 1 5 crimd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 )
22 9 11 crimd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐷 )
23 21 22 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( 𝐵 · 𝐷 ) )
24 20 23 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) − ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) )
25 17 24 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) )
26 8 14 immuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ) )
27 18 22 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( 𝐴 · 𝐷 ) )
28 21 19 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( 𝐵 · 𝐶 ) )
29 27 28 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
30 26 29 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
31 30 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( i · ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ) = ( i · ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ) )
32 25 31 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) + ( i · ( ℑ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) + ( i · ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ) ) )
33 16 32 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) + ( i · ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ) ) )
34 33 fveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( abs ‘ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) + ( i · ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ) ) ) )
35 34 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( abs ‘ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) + ( i · ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ) ) ) ↑ 2 ) )
36 8 14 absmuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) = ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) )
37 36 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) )
38 8 abscld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
39 38 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℂ )
40 14 abscld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℝ )
41 40 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ∈ ℂ )
42 39 41 sqmuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) · ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) · ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) )
43 absreimsq ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
44 absreimsq ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
45 43 44 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) · ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
46 37 42 45 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( abs ‘ ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐶 + ( i · 𝐷 ) ) ) ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
47 1 9 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
48 5 11 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐷 ) ∈ ℝ )
49 47 48 resubcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℝ )
50 1 11 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 · 𝐷 ) ∈ ℝ )
51 5 9 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
52 50 51 readdcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ∈ ℝ )
53 absreimsq ⊢ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℝ ∧ ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ∈ ℝ ) → ( ( abs ‘ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) + ( i · ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
54 49 52 53 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( abs ‘ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) + ( i · ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ) ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
55 35 46 54 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )