Theorem bhmafibid2

Description: The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
2	1	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
3	2	sqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
4		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℝ )
5	4	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
6	5	sqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
7	3 6	addcomd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) )
8	7	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) ) )
9		bhmafibid1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) )
10	9	ancom2s	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) )
11		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
12	11	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
13	12 5	mulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
14		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
15	14	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
16	15 2	mulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
17	13 16	subcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ∈ ℂ )
18	17	sqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ∈ ℂ )
19	12 2	mulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
20	15 5	mulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
21	19 20	addcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
22	21	sqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℂ )
23	18 22	addcomd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
24	8 10 23	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )